build mathematics from puzzles!-logic puzzles, code puzzles, category theory
H2 : « Explorer la logique à travers des énigmes » #
#MVP
build mathematics from puzzles!
+espansos
def 真 : Prop := true
def 偽 : Prop := false
def 謎 (p q : Prop) : Prop :=
(p ∧ q) → p
#check 謎 真 偽 -- What is the truth value?
#check 謎 偽 偽 -- What about here?
#awesome
def 命題 : Prop := true
#check 命題 -- What is its truth value?
def 命題2 : Prop := false
#check 命題2 -- What about this one?
f⁻¹ pulls sets,
f* pulls props`
logic mirrors set inverse images
preimage in limits
pulling ε-neighborhoods back via f⁻¹
— logic meets topology
ε-balls surround outputs—
δ pulls back to x around any a
δ is the pullback of an ε-neighborhood around f(a)
reverse-map (f(x)∈(f(a)±ε)) to find x-range → ∣x−a∣<δ
δ ⬅️ ε via f⁻¹ — like logical preimage
limits ↔ pullbacks
ε–δ ↔ inverse images
category theory in disguise!
f^∗ = pullback of props: logic-level (truth over B pulled to A) 🌰
i_b = inclusion: ε-hood in codomain ⛺️
f^∗ ∘ i_b = pull truth sets back via f! 🎞️
def 🧿 (🍅 🥏 : ℚ) : Prop :=
🍅 > 0 ∧ (∀ 🐞 : ℚ, abs (🐞 - 1) < 🍅 → abs (🐞*🐞 - 1) < 🥏)
#eval 🧿 (1/3) (1/9)
#eval 🧿 (1/20) (1/400)
def 𝔽 : ℚ → ℚ := λ x => x*x
def 𝑖𝔟 (ε : ℚ) : Set ℚ := { y | abs (y - 1) < ε }
def 𝑓* (δ : ℚ) : Set ℚ := { x | abs (x - 1) < δ }
def 輪 (δ ε : ℚ) : Prop :=
∀ x, x ∈ 𝑓* δ → 𝔽 x ∈ 𝑖𝔟 ε
#eval 輪 (1/3) (1/9)
#eval 輪 (1/10) (1/100)