InflationParameters
plain-language theorem explainer
InflationParameters bundles the e-fold count, Hubble rate, and duration for the inflationary phase in Recognition Science cosmology. Horizon-problem researchers cite it when contrasting exponential expansion against the universal 8-tick ledger synchronization. The declaration is a bare structure definition whose only content is the field list plus the inequality constraint e_folds > 60.
Claim. A record consisting of a real number $N$ of e-foldings satisfying $N>60$, a Hubble rate $H$, and a duration $t$ in seconds.
background
Module COS-004 frames the horizon problem: CMB uniformity to 1 part in $10^5$ despite regions that never shared a causal past in standard Big Bang evolution. The standard solution invokes early exponential expansion $a(t)∝exp(Ht)$ with $H∼10^{65}$ s$^{-1}$ at $t∼10^{-36}$ s, stretching one sub-horizon patch by a factor $e^{60}∼10^{26}$ (DOC_COMMENT). Recognition Science supplies a complementary account via the universal 8-tick clock that enforces homogeneity as a ledger consistency condition without light-speed signaling (MODULE_DOC). Upstream structures calibrate the J-cost $J(x)=(x+x^{-1})/2-1$ (LedgerFactorization) and derive the gauge and generation content that enters cosmological models (SpectralEmergence).
proof idea
The declaration is a structure definition with an empty proof body. It simply declares four fields, the last of which is the proposition e_folds_sufficient : e_folds > 60. No lemmas, tactics, or reductions are invoked.
why it matters
The structure is instantiated by the downstream definition standardInflation, which supplies concrete values (65 e-folds, GUT-scale Hubble rate, $10^{-32}$ s duration). It therefore supplies the parameter interface needed to compare the conventional inflationary account with the 8-tick synchronization mechanism highlighted in the module doc-comment. The construction touches framework landmark T7 (eight-tick octave) by providing the quantitative setting in which the ledger-based homogeneity alternative can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.