standardInflation
plain-language theorem explainer
This definition records the conventional numerical values for cosmic inflation parameters inside the Recognition Science treatment of the horizon problem. A cosmologist comparing the standard inflationary resolution to ledger-based 8-tick synchronization would cite these numbers. The definition is a direct record construction whose sole proof obligation is discharged by a numeric tactic on the e-folds threshold.
Claim. The standard inflation parameters are the record with $N=65$ e-foldings, Hubble rate $H=10^{13}×1.602×10^{-10}/ℏ$ at GUT scale, duration $10^{-32}$ s, and the verified condition $N>60$.
background
The module COS-004 states the horizon problem as the observed CMB uniformity to 1 part in $10^5$ despite causal disconnection in standard Big Bang cosmology. The conventional solution is cosmic inflation: exponential expansion $a(t)∝exp(Ht)$ that stretches one small causally connected patch across the observable universe. The sibling structure InflationParameters encodes exactly these requirements: e_folds : ℝ with the side condition e_folds > 60, together with hubble rate, duration in seconds, and a proof term for the inequality. Upstream constants supply the reduced Planck constant ℏ (both RS-native φ^{-5} and CODATA forms) and the fundamental tick τ₀ = 1 that appears in the duration field.
proof idea
The definition is a direct record literal that populates the four fields of InflationParameters. The single proof obligation e_folds_sufficient is discharged by the norm_num tactic on the concrete inequality 65 > 60.
why it matters
The definition supplies the benchmark numbers against which the module contrasts the Recognition Science alternative: the 8-tick clock is a universal ledger property that synchronizes all regions without light-speed communication, making homogeneity a consistency condition rather than a coincidence. It therefore sits inside the COS-004 discussion that cites the T7 eight-tick octave landmark. No downstream declarations depend on it; its role is purely to anchor the conventional account for comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.