Pith. sign in
module module high

IndisputableMonolith.Foundation.PhiForcing

show as:
view Lean formalization →

PhiForcing establishes that the golden ratio φ satisfies φ² = φ + 1 as the self-similar fixed point forced by discrete scale sequences and additive ledger composition. Constant derivations and cosmology modules cite it to anchor the φ-ladder in the J-cost landscape. The module aggregates upstream forcing results from DiscretenessForcing and LedgerForcing without new proofs.

claim$\phi^2 = \phi + 1$, where $\phi > 1$ is the unique positive solution to the quadratic arising from closure of the geometric scale sequence under additive ledger composition.

background

The module sits inside the Foundation layer after LawOfExistence (x exists iff defect(x) = 0) and LedgerForcing (J-symmetry forces double-entry structure). It imports the J-cost J(x) = ½(x + x⁻¹) - 1 from Cost and the discreteness argument that J has a unique minimum at x = 1. PhiForcingDerived supplies the three axioms: discrete scales form {1, r, r², …}, ledger composition is additive, and the resulting fixed-point equation is r² = r + 1.

proof idea

This is a definition module, no proofs. It imports PhiForcingDerived to obtain the equation and re-exports the basic inequalities and inverse properties of φ listed among its siblings.

why it matters in Recognition Science

The module supplies the golden-ratio relation required by downstream constant derivations (ElectronMass C-007, FineStructureConstant C-001, GravitationalConstant C-002, PlanckScaleMatching) and by cosmology modules (FlatnessProblem, DarkMatter). It completes the T5–T6 segment of the forcing chain that produces the self-similar fixed point used for the eight-tick octave and D = 3.

scope and limits

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (24)