cosmicInflationCert
plain-language theorem explainer
cosmicInflationCert assembles the certificate confirming that exactly five inflation models obey J-cost dynamics in Recognition Science, with reheating occurring at the J(1)=0 threshold. Cosmologists extending RS to inflationary scenarios would cite it to anchor the canonical model count and reheating condition. The definition is a direct structure constructor that records the decided cardinality and the J_one theorem.
Claim. The certificate that the cardinality of the set of inflation models equals 5, that $J(1)=0$ (reheating condition), and that the threshold equals the canonical certificate.
background
Recognition Science treats the inflaton field through the same J-cost function J(x) = (x + x^{-1})/2 - 1 that governs all recognition ratios. Slow-roll inflation corresponds to phi_inf >> 1 (large J-cost driving expansion) while reheating occurs as phi_inf approaches 1 and J-cost vanishes. The module CosmicInflationFromJCost defines the structure CosmicInflationCert requiring Fintype.card InflationModel = 5, the equality J(1)=0, and a CanonicalCert threshold.
proof idea
The definition is a direct structure constructor. It populates the five_models field by reference to inflationModelCount (which reduces to decide) and the reheating_condition field by reference to inflation_ends_at_threshold (which reduces to J_one).
why it matters
This definition supplies the terminal certificate that instantiates CosmicInflationCert inside the J-cost cosmology module. It closes the local development by wiring the upstream model-count theorem and the J(1)=0 theorem into the structure. In the Recognition framework it supports the claim that inflation follows the same forcing chain (T5 J-uniqueness through T8 D=3) that yields the phi-ladder and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.