structure
definition
SelfSimilarity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.MetaPrinciple on GitHub at line 108.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
105The claim is that recognition structures are invariant under rescaling
106by a specific factor.
107-/
108structure SelfSimilarity (X : Type*) where
109 /-- The scaling factor. -/
110 factor : ℝ
111 /-- Positive factor. -/
112 factor_pos : 0 < factor
113 /-- The scaling map. -/
114 scale : X → X
115
116/-- The golden ratio φ = (1 + √5) / 2. -/
117noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
118
119/-- φ > 0. -/
120theorem phi_pos : 0 < phi := by
121 unfold phi
122 have h : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (0:ℝ) < 5)
123 linarith
124
125/-- φ² = φ + 1 (the defining property). -/
126theorem phi_sq : phi ^ 2 = phi + 1 := by
127 unfold phi
128 have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5)
129 ring_nf
130 rw [h5]
131 ring
132
133/-- Self-similar + ledger closure forces φ.
134
135This is a THEOREM: the only positive solution to x² = x + 1 is φ.
136-/
137theorem self_similarity_forces_phi (x : ℝ) (hpos : 0 < x) (hsq : x ^ 2 = x + 1) :
138 x = phi := by