positive_root_unique_above_one
plain-language theorem explainer
Any real number r greater than 1 that satisfies the quadratic relation r squared equals r plus 1 must equal the golden ratio phi. Researchers modeling self-similar cascades in the phi-ladder for Navier-Stokes would cite the result to identify the unique ratio that drives the defect cost to zero. The tactic proof rewrites both the candidate equation and the defining identity for phi into monic quadratic form, then reaches a contradiction by comparing the quadratic values under the ordering supplied by one less than phi.
Claim. Let $r$ be a real number satisfying $r > 1$ and $r^2 = r + 1$. Then $r = phi$, where $phi$ is the golden ratio.
background
The declaration belongs to the module that develops a simplified variational model for the phi-ladder. In this model the defect of a ratio r greater than 1 is measured by its failure to obey the self-similar closure equation r squared equals r plus 1; the associated cost function is minimized precisely when r equals phi. The local setting therefore treats phi as the canonical fixed point of the geometric cascade. The proof draws on the upstream identity phi squared equals phi plus 1, which records the defining equation of the golden ratio, and on the fact that phi exceeds 1. Both facts are established in Constants.lean and re-exported through the PhiSupport layer.
proof idea
The proof first converts the hypothesis r squared equals r plus 1 into the monic equation r squared minus r minus 1 equals zero by nlinarith. It performs the same conversion for phi using the upstream identity phi squared equals phi plus 1. Assuming the two roots differ, it splits into the cases r less than phi and r greater than phi. In each case nlinarith together with one less than phi produces a strict inequality between the quadratic evaluations at r and at phi, contradicting the fact that both evaluations are zero.
why it matters
The result is invoked directly by the downstream theorem simplifiedCascadeCost_eq_zero_iff, which converts the uniqueness statement into the equivalence that the simplified cascade cost vanishes if and only if the ratio equals phi. This closes the identification of phi as the unique optimal ratio inside the variational model. In the broader Recognition Science framework the lemma supports the forcing of phi as the self-similar fixed point (T6) that underlies the eight-tick octave and the three-dimensional spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.