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

InflatonCert

show as:
view Lean formalization →

InflatonCert bundles five structural invariants of the RS inflaton potential into a single record: exactly five regimes, 44 e-folds, the phi^5 Fibonacci identity, positive slow-roll parameters, and spectral index inside the observed band. A cosmologist working in Recognition Science would cite it to confirm that the derived potential satisfies standard inflation constraints without further derivation. The declaration is a pure structure that directly references the module's sibling definitions for each field.

claimThe structure asserts that the inflaton potential admits exactly five regimes (slow-roll plateau, slow-roll slope, hilltop decline, reheating, radiation era), the e-fold count equals 44, satisfies $phi^5 = 5 phi + 3$, the first slow-roll parameter obeys $epsilon > 0$, the second obeys $eta > 0$, and the spectral index lies in the interval $(0.955, 0.957)$ around $1 - 2/45$.

background

The module defines the RS inflaton potential V(chi) with five canonical structural regimes corresponding to configDim D = 5. These regimes are encoded in the inductive type InflatonRegime whose constructors are slowRollPlateau, slowRollSlope, hilltopDecline, reheating, and radiationEra. Slow-roll parameters are fixed by the module as epsilon = 1/(2 phi^5) and eta = 1/phi^5, with e-fold count set to the constant 44. Upstream definitions supply slowRollEpsilon and slowRollEta as 1/(2 phi^5) and 1/phi^5 respectively, together with the efoldCount constant and the phi^5 Fibonacci identity from NumberTheoryFromRS.

proof idea

The structure is assembled by direct field assignment to sibling definitions: five_regimes from the Fintype.card instance on InflatonRegime, efolds from efoldCount, the phi identity from phi5_eq, and the positivity and band conditions from the positivity lemmas slowRollEpsilon_pos and slowRollEta_pos.

why it matters in Recognition Science

This certificate feeds the inflatonCert definition that packages the structural properties for use in cosmological derivations. It encodes the five-regime structure required by the RS forcing chain at T8 together with the phi^5 Fibonacci relation. The spectral index band confirms consistency with observations inside the alpha band of RS constants.

scope and limits

formal statement (Lean)

  64structure InflatonCert where
  65  five_regimes : Fintype.card InflatonRegime = 5
  66  efolds : efoldCount = 44
  67  phi5_fibonacci : phi ^ 5 = 5 * phi + 3
  68  epsilon_pos : 0 < slowRollEpsilon
  69  eta_pos : 0 < slowRollEta
  70  spectral_index_in_band : ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ))
  71

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.