satisfies_golden_constraint
plain-language theorem explainer
The definition states that a real number r satisfies the golden constraint when r squared equals r plus one. Researchers modeling self-similar discrete ledgers cite this algebraic condition as the scale-invariance requirement under J-cost. It is introduced as a direct definition that encodes the quadratic relation without lemmas or reductions.
Claim. A real number $r$ satisfies the golden constraint when $r^2 = r + 1$.
background
The module establishes that self-similarity in a discrete ledger equipped with J-cost forces the golden ratio. Self-similarity means the ledger references itself across scales while preserving the same cost structure, so that scaling by r composes to match the next ledger level plus the base unit. The upstream forces structure supplies single-valued comparison on carriers, while the self lemma confirms PhiClosed closure under the subfield generated by φ.
proof idea
One-line definition that directly encodes the quadratic equation r² = r + 1 as the Prop.
why it matters
This definition supplies the algebraic target used by golden_constraint_unique to isolate φ among positive reals and by self_similar_forces_golden_constraint to derive the constraint from scale invariance. It occupies the T6 step in the forcing chain where self-similar fixed points are required, feeding directly into phi_unique_self_similar and phi_satisfies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.