CosmicInflationCert
plain-language theorem explainer
A certificate structure asserts that exactly five canonical inflation models exist under J-cost dynamics, that reheating occurs when the recognition cost vanishes at argument one, and that the threshold meets the six-clause canonical band conditions. Cosmologists modeling the inflaton via recognition ratios would cite this to tie the standard models to the phi-ladder. The declaration is a structure definition that assembles the model count from the inductive enumeration, the zero condition from band properties, and the full threshold from the上游
Claim. A certificate structure states that the set of inflation models has cardinality five, that the recognition cost function satisfies $J(1)=0$, and that the threshold obeys the six conditions of the canonical band certificate (matched zero at unity, reciprocity, positive phi value, band bounds 0.11 to 0.13, and positive recovery at $1/phi^2$).
background
The module treats the inflaton field as obeying the same J-cost dynamics as any recognition ratio: large J drives slow-roll inflation while J approaches zero at reheating. J is the recognition cost $J(x)=(x+x^{-1})/2-1$. The inductive type enumerates five models: chaotic, natural, starobinsky, higgs inflation, and axion monodromy, matching configDim equal to five. CanonicalCert supplies the six-clause threshold: matched zero at J(1)=0, reciprocity under inversion, J(phi)>0, the band 0.11<J(phi)<0.13, and positive recovery at $1/phi^2$.
proof idea
The declaration is a structure definition with no proof body. It directly bundles the cardinality claim from the Fintype instance on the five-constructor inductive type, the reheating zero from the matched_zero field of CanonicalCert, and the full threshold structure from the same upstream certificate.
why it matters
This certificate is consumed by the downstream cosmicInflationCert definition that packages the complete inflation claim. It supplies the explicit link between J-cost reheating and the five standard models predicted by the Recognition Science framework for the inflaton. The construction sits inside the forcing chain after phi is fixed as the self-similar point and before the eight-tick octave is applied to spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.