phiInvCubed_eq_two_phi_minus_three
plain-language theorem explainer
The identity 1/φ³ = 2φ - 3 supplies the Cabibbo-angle factor in Recognition Science. Cross-domain modelers cite it when mapping inverse-phi decay rates or mixing angles onto the phi-ladder. The proof is a short algebraic reduction that multiplies the target expression by φ³, invokes the Fibonacci relations φ² = φ + 1 and φ³ = 2φ + 1, and solves the resulting linear equation.
Claim. The golden ratio satisfies $1/φ^3 = 2φ - 3$.
background
In Recognition Science the golden ratio φ is defined by the quadratic φ² = φ + 1. The module C22 collects a family of 1/φ invariants that recur as decay rates, target ratios, and mixing factors across domains, with the explicit instance that the Cabibbo mixing angle equals 1/φ³. Upstream lemmas from Constants, PhiLadderLattice, and several domain modules establish the companion cubic identity φ³ = 2φ + 1 by direct expansion of the quadratic relation.
proof idea
The tactic proof first records φ³ ≠ 0 from positivity of φ. It imports φ² = φ + 1 via phi_sq_eq and φ³ = 2φ + 1 via phi_cubed_eq. A single nlinarith step then shows φ³(2φ - 3) = 1. The final rewrite converts the product equation into the desired division form.
why it matters
This identity is collected inside phiInverseInvariantsCert, which packages the full set of 1/φ relations for downstream certification. It directly supports the Cabibbo-angle claim listed in the module doc-comment. Within the forcing chain it instantiates the inverse branch of the phi-ladder arithmetic at rung -3. No open scaffolding remains for this specific equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.