pith. machine review for the scientific record. sign in
theorem proved term proof high

inflatonRegime_count

show as:
view Lean formalization →

The theorem establishes that the inductive type enumerating the structural regimes of the RS inflaton potential contains exactly five elements. Cosmologists assembling the inflatonCert object in the Recognition Science framework would cite this cardinality when confirming the completeness of the potential's phase structure. The proof is a one-line decision procedure that evaluates the Fintype instance derived from the five-constructor inductive definition.

claimThe set of canonical structural regimes for the RS inflaton potential has cardinality five, consisting of the slow-roll plateau, the slow-roll slope, the hilltop decline, reheating, and the radiation era.

background

The Inflaton Potential Structural module partitions the RS inflaton potential V(χ) into five regimes that realize configDim D = 5. These regimes are the constructors of the inductive type with cases slow-roll plateau, slow-roll slope, hilltop decline, reheating, and radiation era; the module also records the slow-roll parameters ε = 1/(2φ⁵), η = 1/φ⁵ and the e-fold count N_e = 44 drawn from the gap-45 ladder. Upstream results supply the gap function as the logarithmic residue F(Z) = ln(1 + Z/φ) / ln(φ) at the anchor scale, which fixes the gap-45 derivation used for the e-fold count.

proof idea

The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression. The tactic succeeds because the inductive type derives a Fintype instance directly from its five constructors, allowing the decision procedure to compute the cardinality as 5 without further lemmas.

why it matters in Recognition Science

This result supplies the five_regimes field of the inflatonCert definition, which collects the complete certification of the inflaton potential including e-folds, phi5 equality, and positivity of the slow-roll parameters. It realizes the structural claim in the module documentation that the potential has five regimes tied to the gap-45 ladder. Within the Recognition Science framework it extends the forcing chain to cosmological scales while preserving the phi-ladder mass formula and the eight-tick octave structure.

scope and limits

formal statement (Lean)

  31theorem inflatonRegime_count : Fintype.card InflatonRegime = 5 := by decide

proof body

Term-mode proof.

  32
  33/-- e-fold count N_e = 44 (gap-45 ladder). -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.