theorem
proved
phi_unique_self_similar
show as:
view math explainer →
Self-similar closure forces the golden ratio: r² = r + 1.
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.PhiForcing on GitHub at line 186.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
183 nlinarith [sq_nonneg (r - φ), sq_nonneg (r + φ - 1), phi_pos, hsq5]
184
185/-- The golden constraint characterizes φ among positive reals. -/
186theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r) (hr_eq : satisfies_golden_constraint r) :
187 r = φ :=
188 golden_constraint_unique hr_pos hr_eq
189
190/-! ## Discrete Ledger with Self-Similarity -/
191
192/-- A discrete ledger structure (from LedgerForcing). -/
193structure DiscreteLedger where
194 /-- The ledger structure -/
195 ledger : LedgerForcing.Ledger
196 /-- A concrete discrete configuration space witnessing finite step structure. -/
197 discrete_space : DiscretenessForcing.DiscreteConfigSpace
198
199/-- Self-similarity property for a discrete ledger. -/
200def is_self_similar (_L : DiscreteLedger) (r : ℝ) : Prop :=
201 ∃ S : SelfSimilar, S.ratio = r
202
203/-! ## Phi Forcing Theorem -/
204
205/-- **PHI FORCING THEOREM**: In a self-similar discrete ledger, the scale ratio is φ.
206
207If:
2081. L is a discrete ledger (from DiscretenessForcing + LedgerForcing)
2092. L is self-similar with scale ratio r
2103. r satisfies the compositional constraint r² = r + 1
211
212Then: r = φ = (1 + √5)/2 -/
213theorem phi_forced (L : DiscreteLedger) (r : ℝ) (hr : is_self_similar L r) : r = φ := by
214 rcases hr with ⟨S, rfl⟩
215 exact golden_constraint_unique S.ratio_pos (self_similar_forces_golden_constraint S)
216
papers checked against this theorem (showing 3 of 3)
-
Gravity as a broken gauge symmetry, with no Big Bang singularity
"the SSB of the vacuum state in the Wilczek theory is realised when the Higgs-like field acquires a nonzero vacuum expectation value along one of the five directions of the internal space"
-
A 38 TeV gauge operator could seed the universe's matter excess
"For the value of g² and λ at finite temperatures, we use g²|_{T≠0} ≃ 0.39 and λ/g²|_{T≠0} ≃ 0.22 obtained by extrapolating from the three-dimensional effective field theory"
-
A Noble-Gas-Centered Coordinate for Within-Period Atomic Property Trends
"φ = (1+√5)/2 is presently a modeling ansatz, not a derived chemical constant. ... a first-principles derivation of φ in this chemical context is left to future work."