r_in_detectable_range
plain-language theorem explainer
The theorem confirms positivity of the tensor-to-scalar ratio at 50 and 60 e-folds in the phi-attractor inflation model. Cosmologists checking detectability windows for LiteBIRD or CMB-S4 would reference the result when verifying that r remains observable. The proof is a direct term-mode reduction that unfolds the ratio definition and applies the positivity of the alpha-attractor parameter together with standard real division rules.
Claim. Let $r(N)$ denote the tensor-to-scalar ratio at $N$ e-folds in the Recognition Science inflation model. Then $r(60) > 0$ and $r(50) > 0$.
background
The module formalizes inflationary predictions derived from the Recognition Science cost functional. The alpha-attractor parameter is fixed at $α = φ²$, yielding the explicit tensor-to-scalar ratio $r ≈ 12 φ² / N²$ for slow-roll parameters at $N$ e-folds. The function tensor_to_scalar is the ratio of tensor to scalar power spectra, defined as $A_T / A_s$ when the scalar amplitude is positive. Upstream results supply the cost function from multiplicative recognizers and the J-cost of recognition events, both of which are non-negative by construction and feed into the positivity of the attractor parameter.
proof idea
The term proof first unfolds tensor_to_scalar to expose the division of power spectra. It then splits the conjunction and applies div_pos to each component, multiplying the positive constant 12 by the positive alpha_attractor parameter in the numerator while invoking positivity on the denominator.
why it matters
The result supplies the final positivity check required to place the RS prediction $r ≈ 12 φ² / N²$ inside the LiteBIRD/CMB-S4 detection band. It completes the parameter-free inflation block that begins from the Recognition Composition Law and the self-similar fixed point φ, without introducing new hypotheses. The module as a whole supplies the spectral index and tensor ratio that follow directly from the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.