phi2_eq
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the tensor-to-scalar ratio formula itself.
- Does not evaluate the numerical interval without phi_gt_onePointSixOne and nlinarith.
- Does not connect the identity to the Recognition Composition Law.
formal statement (Lean)
17theorem phi2_eq : phi ^ 2 = phi + 1 := phi_sq_eq
proof body
18