InflationEfoldCert
plain-language theorem explainer
RS derives an inflation duration of 44 e-folds as gap45 minus one. The structure records this equality together with the condition that the derived spectral index lies between 0.95 and 0.96. Researchers matching Recognition Science cosmology to CMB measurements would cite the bundled certificate. It is introduced purely as a record type.
Claim. A record type whose fields certify that the e-fold count satisfies $N_e = g_{45} - 1$ and that the spectral index satisfies $0.95 < n_s < 0.96$, where $n_s = 1 - 2/N_e$.
background
The module computes the e-fold count during inflation from the Recognition Science gap parameter. Nefolds is defined as the natural number 44, corresponding to $N_e =$ gap(3) $-$ 1. The spectral index nS_RS is defined as $1 - 2$ divided by Nefolds, which evaluates to approximately 0.9545. Upstream, the result from InflationaryCosmologyFromRS states: E-folds $N_e = 44$ (baryonRung). This structure then combines the equality to gap45 $-$ 1 with the band check on nS_RS to form a compact certificate.
proof idea
The declaration introduces a structure type whose fields directly encode the e-fold equality and the spectral index band. It depends on the definitions of Nefolds as 44 and nS_RS as $1 - 2/$Nefolds, together with the sibling result establishing Nefolds = gap45 $-$ 1. No tactics are applied; the structure serves as a container for these two propositions.
why it matters
This structure supplies the type for the downstream certificate inflationEfoldCert, which is built from the equality Nefolds_gap45_minus_one and the band nS_RS_band. It realizes the RS prediction $N_e = 44$ during inflation, yielding $n_s ≈ 0.9545$ and $r ≈ 0.0062$. The module notes that $1 - 2/45 ≈ 0.956$ lies closer to Planck's 0.965, leaving open the precise matching to observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.