pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CosmicInflationCert

show as:
view Lean formalization →

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上游

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  32structure CosmicInflationCert where
  33  five_models : Fintype.card InflationModel = 5
  34  reheating_condition : J 1 = 0
  35  threshold : CanonicalCert
  36

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.