golden_constraint_unique
plain-language theorem explainer
Among positive real numbers the equation r² = r + 1 possesses exactly one solution, the golden ratio φ. Researchers deriving the forced scale factor in self-similar discrete ledgers cite this uniqueness result to close the argument from the golden constraint to φ. The proof rewrites the constraint as a quadratic, invokes positivity of r together with the known equation satisfied by φ, and applies algebraic closure via nlinarith to exclude the negative root.
Claim. Let $r > 0$ be a real number satisfying $r^2 = r + 1$. Then $r = φ$.
background
The PhiForcing module shows that self-similarity in a discrete ledger equipped with J-cost forces scale ratios to obey a specific algebraic relation. The predicate satisfies_golden_constraint r holds exactly when r² = r + 1; this encodes the requirement that scaling by r must be composable in the ledger sense, with the next scale equal to the current scale plus the base unit. The module doc states that the only positive solution to this relation is the golden ratio φ, which supplies the self-similar fixed point.
proof idea
The tactic proof first simplifies the definition of satisfies_golden_constraint to obtain r² = r + 1, then rewrites it as the quadratic r² - r - 1 = 0. It establishes auxiliary facts such as sqrt(5) > 2 and the square identity for sqrt(5), recalls the upstream theorem phi_equation that φ satisfies the same quadratic, and closes with nlinarith using phi_pos together with non-negativity of (r - φ)² and (r + φ - 1)².
why it matters
The result is invoked directly by phi_forced to conclude that any self-similar discrete ledger must adopt scale ratio φ, and likewise by phi_forcing_principle and phi_unique_self_similar. It supplies the uniqueness half of the T6 step in the forcing chain, confirming that φ is the unique positive self-similar fixed point compatible with the J-cost structure and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
One golden-ratio curve organizes four periodic-table trends at once
"the argument-rescaling factor φ = (1+√5)/2 is presently a modeling ansatz, not a derived chemical constant. We retain it because it produces the ratio identities ... but a first-principles derivation of φ in this chemical context is left to future work."