inflation_ends_at_threshold
plain-language theorem explainer
The result establishes that the J-cost function vanishes at argument one, which marks the reheating threshold where inflation terminates in the Recognition Science model. Cosmologists working with J-cost dynamics for the inflaton would cite this when certifying the end of slow-roll expansion. The proof is a direct one-line wrapper that applies the established evaluation of J at unity.
Claim. $J(1) = 0$, where $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
In the Recognition Science treatment of cosmology the inflaton is treated as a recognition ratio whose J-cost controls the expansion. For field values much larger than one the cost is large and drives inflation; as the field approaches one the cost drops to zero and inflation ends. The module states that reheating is fixed at this canonical J-cost threshold, with five inflation models corresponding to configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the J_one lemma from the CanonicalJBand module (or its counterpart in ActivationEnergy).
why it matters
This supplies the reheating_condition inside the cosmicInflationCert definition, which assembles the full model certification together with the count of five models. It connects the J-uniqueness property (T5) directly to the observable termination of inflation, consistent with the eight-tick octave and D = 3 in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.