alpha_attractor_pos
plain-language theorem explainer
This establishes that the α-attractor parameter α = φ² is strictly positive. Cosmologists checking inflationary predictions in Recognition Science would cite it before deriving tensor-to-scalar bounds. The proof is a one-line application of the fact that the square of any positive real remains positive.
Claim. Let α = φ² where φ is the golden ratio. Then 0 < α.
background
The Inflation from phi module formalizes RS predictions with the α-attractor parameter fixed at φ² from cost-functional self-similarity. The upstream definition states that α = φ² arises because the inflaton potential inherits the quadratic character of J(x) near x = 1, with the φ² = φ + 1 identity setting the curvature scale. This occurs inside the derivation of parameter-free quantities n_s ≈ 1 - 2/N and r ≈ 12 φ² / N².
proof idea
The proof is a one-line wrapper that invokes the general positivity-of-powers lemma on the positive golden ratio φ.
why it matters
It supplies the alpha_positive field required by the inflation_cert theorem that bundles all model checks. It also feeds the positivity steps in r_at_55_bounds and r_in_detectable_range. The result closes the positivity requirement for the α = φ² attractor that originates from the self-similar fixed point in the forcing chain, enabling concrete CMB predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.