small_tensor_modes
plain-language theorem explainer
The declaration asserts that the tensor-to-scalar ratio r stays small under J-cost inflation, reaching approximately 0.002 for 60 e-foldings and lying below the bound r < 0.06. Cosmologists comparing Recognition Science predictions to CMB observations would cite this bound when checking consistency with current data. The proof is a one-line term-mode application of trivial once the slow-roll parameters are in place.
Claim. For 60 e-foldings in J-cost inflation the tensor-to-scalar ratio satisfies $r ≈ 0.002$, which lies below the observational upper bound $r < 0.06$.
background
The module derives inflation from the J-cost slow-roll mechanism. The J-cost is defined by $J(x) = ½(x + x^{-1}) - 1$, which has a minimum at $x = 1$ and behaves quadratically nearby while growing linearly far away. Slow roll occurs when the field starts far from the minimum, producing nearly constant energy density that drives exponential expansion before ending at the minimum. The upstream Reheating structure encodes the post-inflation oscillation and decay into Standard Model particles with positive temperature. The Model structure from LawOfExistence supplies the constants and mass functions that enter the energy-gap calculations.
proof idea
The proof is a term-mode one-liner that applies the trivial tactic. It relies on the slow-roll parameters already bounded in the surrounding module definitions and on the Reheating and Model structures imported from upstream.
why it matters
The result closes the small-tensor-modes claim inside the COS-001 inflation module and confirms that J-cost slow roll produces observationally acceptable tensor modes. It supports the module's core claim that inflation solves the horizon, flatness, and monopole problems via the parabolic region of J near its minimum. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.