pith. sign in
theorem

phi_forced

proved
show as:
module
IndisputableMonolith.Foundation.PhiForcing
domain
Foundation
line
213 · github
papers citing
8 papers (below)

plain-language theorem explainer

A self-similar discrete ledger forces its scale ratio to equal the golden ratio φ. Researchers deriving the Recognition Science forcing chain from T0 to T8 cite this result to establish the unique fixed point of self-similarity. The proof is a one-line term that extracts the ratio from the self-similarity witness and applies the uniqueness theorem for the golden constraint.

Claim. Let $L$ be a discrete ledger and let $r > 0$ satisfy the self-similarity condition on $L$. Then $r = φ$, where $φ = (1 + √5)/2$ is the unique positive root of $x^2 = x + 1$.

background

A DiscreteLedger packages a LedgerForcing.Ledger with a DiscretenessForcing.DiscreteConfigSpace to enforce finite-step structure. The module establishes that self-similarity on such a ledger, combined with the J-cost function, requires the scale ratio to obey the compositional identity $r^2 = r + 1$. Upstream, golden_constraint_unique states that any positive real satisfying the golden constraint equals φ, while self_similar_forces_golden_constraint shows that the self-similarity hypothesis on a ledger produces exactly that constraint.

proof idea

The term proof performs rcases on the self-similarity hypothesis to obtain the underlying scale structure S and a reflexivity equality. It then feeds S.ratio_pos together with the output of self_similar_forces_golden_constraint S directly into golden_constraint_unique.

why it matters

The declaration supplies the T6 step that φ is the self-similar fixed point inside the UnifiedForcingChain. It is invoked by origin_question_resolved to close the geometric-sequence closure clause and by fibonacci_char_poly_unique_pos_root to identify the unique positive root of the Fibonacci characteristic polynomial. The result therefore anchors the eight-tick octave and the subsequent derivation of D = 3.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.