pith. sign in
module module high

IndisputableMonolith.Foundation.PhiForcing

show as:
view Lean formalization →

The PhiForcing module establishes that the golden ratio φ satisfies φ² = φ + 1 from the J-cost functional together with ledger axioms. Researchers deriving physical constants from the φ-ladder cite this result. The module assembles discreteness and ledger forcing to reach the self-similar fixed point.

claimThe unique positive real φ satisfying φ² = φ + 1 is the fixed point of the recognition cost landscape under discrete scale invariance.

background

The module sits in the Foundation domain and imports LawOfExistence (existence iff defect zero), DiscretenessForcing (J(x) = ½(x + x⁻¹) - 1 has unique minimum at x = 1, or J(e^t) = cosh(t) - 1), LedgerForcing (J-symmetry forces double-entry structure), and PhiForcingDerived (derives r² = r + 1 from geometric scale sequences and additive ledger composition). Sibling declarations include phi_equation together with bounds such as phi_gt_onePointSixOneEight and phi_lt_onePointSixOneNine.

proof idea

This is a definition module, no proofs. The core equation is supplied by the imported PhiForcingDerived and specialized via the listed sibling declarations.

why it matters in Recognition Science

This module supplies the golden ratio φ that feeds constant derivations in ElectronMass, FineStructureConstant, GravitationalConstant, and PlanckScaleMatching, plus cosmological models in DarkMatter and FlatnessProblem. It fills the T6 step of the forcing chain where phi is forced as the self-similar fixed point.

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)