pith. sign in
module module high

IndisputableMonolith.Foundation.PhiForcing

show as:
view Lean formalization →

PhiForcing establishes that the self-similar fixed point satisfies the golden ratio equation phi squared equals phi plus one. Researchers deriving constants from the phi-ladder in electron mass and fine structure cite this module. The module assembles the result by importing the closure axioms from PhiForcingDerived together with discreteness, existence, and ledger forcing.

claimThe scale factor $\phi$ satisfies the equation $\phi^2 = \phi + 1$.

background

This module sits in the Foundation domain and imports the cost functional J from Cost together with the unique-minimum argument at unity from DiscretenessForcing. LawOfExistence supplies the zero-defect condition for existence while LedgerForcing derives double-entry structure from J-symmetry. PhiForcingDerived supplies the three axioms of discrete geometric scales, additive ledger composition, and closure.

From the doc-comment of PhiForcingDerived: 'This module derives r² = r + 1 from three stated axioms: 1. Discrete Scale Sequence: Scales form a geometric sequence {1, r, r², ...} 2. Additive Ledger Composition: When two recognition events combine in the ledger, their scales ADD (not multiply).'

proof idea

This is a definition module that imports the phi equation from PhiForcingDerived and records immediate consequences such as positivity, bounds near 1.618, and the inverse. No independent proofs are developed here; the argument is inherited from the upstream closure axioms.

why it matters in Recognition Science

The phi equation supplied here is the direct input to the constant derivations in ElectronMass, FineStructureConstant, GravitationalConstant, and PlanckScaleMatching. It also supports the cosmology results on dark matter and flatness. The module completes the T6 forcing step in the unified chain by identifying the self-similar fixed point with the golden ratio.

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)