phi_satisfies
plain-language theorem explainer
φ 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 φ.
Claim. The 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
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).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.