phiInvSq_eq_two_minus_phi
plain-language theorem explainer
The equality one over the square of the golden ratio equals two minus the golden ratio holds exactly. Cross-domain researchers in Recognition Science cite it when unifying decay rates, target ratios, and mixing angles around the inverse golden ratio attractor. The proof substitutes the squared and cubed identities for phi into the product expression and applies linear arithmetic to recover the division form.
Claim. For the golden ratio $phi$ satisfying $phi^2 = phi + 1$, it holds that $1/phi^2 = 2 - phi$.
background
The module establishes cross-domain invariants for quantities scaling as one over phi, the inverse golden ratio, which serves as the canonical attractor for negative-rung quantities including decay rates, dampings, and target ratios. Key supporting definitions include the golden ratio phi obeying the quadratic equation whose positive root yields phi squared equals phi plus one, and the derived cubic identity phi cubed equals two phi plus one. These are drawn from upstream results such as the lemma stating 'Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0)' and the corresponding cubic expansion 'Key identity: φ³ = 2φ + 1 (Fibonacci recurrence)'.
proof idea
The tactic proof begins by confirming phi squared is nonzero from positivity. It retrieves phi squared equals phi plus one from the squared identity lemma and phi cubed equals two phi plus one from the cubed identity lemma. Nonlinear arithmetic then verifies that phi squared multiplied by two minus phi equals one. The target equality follows by commuting the equation and applying the division equivalence, then linear arithmetic.
why it matters
This result is assembled into the PhiInverseInvariantsCert which packages the full set of inverse-phi properties for use in domain-specific claims. It directly supports the structural claim in the C22 wave that one over phi unifies senolytic target ratios, Gini ceilings, and Cabibbo-angle factors. Within the Recognition framework it confirms the self-similar fixed point of phi arising from the forcing chain without additional assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.