phi_satisfies
φ satisfies the algebraic constraint φ² = φ + 1 required by self-similarity in a discrete ledger with J-cost. Researchers deriving physical constants from Recognition Science would cite this when showing that scale factors in self-similar ledgers must be the golden ratio. The proof is a direct one-line application of the defining equation for φ.
claimThe golden ratio φ satisfies the equation φ² = φ + 1.
background
The Phi Forcing module shows that self-similarity in a discrete ledger with J-cost forces the scale ratio to obey a specific algebraic relation. The predicate satisfies_golden_constraint r asserts r² = r + 1, which encodes that scaling by r composes such that the next scale equals the current scale plus the base unit. This arises because J-cost self-similarity requires J(r) = J(1) = 0 for non-trivial fixed points, leading to the quadratic constraint instead of the trivial solution r = 1.
proof idea
One-line wrapper that applies the theorem phi_equation, which states φ² = φ + 1 and is proved by unfolding the definition of φ, verifying the square of the square root of 5, and closing with ring and nlinarith.
why it matters in Recognition Science
This result confirms that φ meets the golden constraint derived from self-similarity in the discrete ledger. It supports the module's main claim phi_forced that DiscreteLedger L and SelfSimilar L together imply Ratio L = φ. In the Recognition Science framework it corresponds to T6, where phi is forced as the self-similar fixed point after J-uniqueness (T5) and before the eight-tick octave (T7).
scope and limits
- Does not prove that φ is the unique positive real satisfying the constraint.
- Does not derive the numerical approximation of φ.
- Does not instantiate the constraint inside a concrete ledger model.
- Does not reference J-cost or defectDist directly.
formal statement (Lean)
159theorem phi_satisfies : satisfies_golden_constraint φ := phi_equation
proof body
Term-mode proof.
160
161/-- The golden constraint characterizes φ among positive reals. -/