pith. sign in
module module high

IndisputableMonolith.Foundation.PhiForcing

show as:
view Lean formalization →

PhiForcing module establishes that the golden ratio satisfies φ² = φ + 1 as the self-similar fixed point forced by the J-cost minimum and ledger axioms. Researchers deriving constants or cosmology results cite it for the scale factor in the phi-ladder. The argument closes via the discrete scale sequence plus additive composition imported from upstream forcing modules.

claimThe golden ratio satisfies the equation $φ^2 = φ + 1$.

background

This module belongs to the Foundation layer and imports Cost (J-cost functional J(x) = ½(x + x⁻¹) - 1), DiscretenessForcing (unique minimum at x=1, convex bowl in log coordinates), LawOfExistence (existence iff defect zero), LedgerForcing (J-symmetry forces double-entry), and PhiForcingDerived (derives r² = r + 1 from discrete geometric scales and additive ledger work). The local setting is the T0-T8 forcing chain with T6 fixing phi as the self-similar point under the Recognition Composition Law. Upstream states: 'This module derives r² = r + 1 from three stated axioms: Discrete Scale Sequence... Additive Ledger Composition...'

proof idea

The module first imports the cost and ledger forcing results, then proves auxiliary bounds (phi > 1, phi < 2, etc.) on the fixed point, and finally closes the quadratic equation by algebraic reduction from the self-similarity condition supplied by the additive ledger axiom.

why it matters in Recognition Science

This module supplies the golden ratio required by T6 in the forcing chain and the Recognition Composition Law. It feeds the parent derivations in ElectronMass (C-007), FineStructureConstant (C-001), GravitationalConstant (C-002), PlanckScaleMatching, and the cosmology modules DarkMatter and FlatnessProblem. It closes the scale-factor step that later modules use for the phi-ladder mass formula and alpha band.

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)