one_sub_phi_inv_eq_phi_inv_sq
plain-language theorem explainer
The golden ratio satisfies the algebraic identity 1 - 1/φ = 1/φ². Researchers deriving the recognition band boundaries in the Unification module cite this relation when establishing the sum-to-one property of rhoBandLower and rhoBandUpper. The proof is a short term-mode calculation that invokes the quadratic equation φ² = φ + 1, applies field simplification to clear the inverse, and closes with linear arithmetic.
Claim. $1 - 1/φ = (1/φ)^2$
background
The golden ratio φ is the positive root of x² - x - 1 = 0 and satisfies the key identity φ² = φ + 1. In the RecognitionBandGeometry module this relation is used to relate the lower and upper boundaries of the recognition band, which are defined via the band operation on stable states. Upstream results supply the non-vanishing of φ and the quadratic identity itself.
proof idea
The proof obtains φ ≠ 0 from phi_ne_zero and the quadratic relation from phi_sq_eq. Field simplification clears the denominator, after which nlinarith closes the goal using positivity of φ and the quadratic identity.
why it matters
This identity supports the bandBoundaries_sum_to_one theorem in the same module and supplies an algebraic step toward the phi-ladder mass formula. It sits inside the Recognition Science derivation that forces D = 3 and the eight-tick octave from the Recognition Composition Law. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.