phi2_eq
plain-language theorem explainer
The golden ratio φ obeys φ² = φ + 1. Cosmologists deriving the Recognition Science bound on the tensor-to-scalar ratio r ∈ (0.015, 0.020) cite this identity to simplify the denominator 45φ². The proof is a one-line wrapper that directly invokes the phi_sq_eq lemma from the constants module.
Claim. The golden ratio φ satisfies the equation φ² = φ + 1.
background
The module TensorToScalarRatioFromRS derives the RS prediction r = 2/(45φ²) ∈ (0.015, 0.020) for the tensor-to-scalar ratio in cosmology. The golden ratio φ is the positive root of x² - x - 1 = 0 and appears throughout the phi-ladder constructions. Upstream results establish the identity in two places: Constants.phi_sq_eq states 'Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0)' and proves it by norm_num, Real.sq_sqrt, ring_nf and linear_combination; PhiLadderLattice.phi_sq_eq gives the parallel statement proved by field_simp after unfolding φ.
proof idea
The declaration is a one-line wrapper that applies the phi_sq_eq lemma imported from IndisputableMonolith.Constants.
why it matters
This identity is invoked inside r_band and r_lt_one to obtain the interval (0.015, 0.020) for the tensor-to-scalar ratio. It supplies the algebraic reduction required by the RS cosmology prediction r = 2/(45φ²) and traces to the forcing chain step T6 where φ is forced as the self-similar fixed point. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.