standardInflation
plain-language theorem explainer
Standard inflation parameters are instantiated with 65 e-folds, GUT-scale Hubble rate, and 10^{-32} s duration. Cosmologists comparing horizon-problem resolutions cite this record to benchmark the conventional exponential-expansion account against the 8-tick ledger synchronization. The definition assembles the structure by direct field assignment and applies norm_num to confirm the e-folds exceed 60.
Claim. The standard inflation parameters consist of $N=65$ e-foldings, Hubble rate $H=10^{13}×1.602×10^{-10}/ℏ$ at the GUT scale, duration $10^{-32}$ s, and the verified condition $N>60$.
background
InflationParameters is the structure that records the number of e-foldings, the Hubble expansion rate during inflation, the duration in seconds, and the proof obligation that the number of e-foldings exceeds 60. The module COS-004 states the horizon problem as the observed CMB uniformity to 1 part in 10^5 despite regions that remain causally disconnected in the standard Big Bang timeline. The conventional solution invokes early exponential expansion that stretches one small causally connected patch across the observable universe. Upstream constants supply ℏ as the reduced Planck constant in RS-native units (φ^{-5}) and the fundamental tick as the time quantum of 1.
proof idea
The definition constructs the InflationParameters record by direct assignment of the three numerical fields. The remaining field is discharged by the norm_num tactic, which reduces the inequality 65 > 60 to a decidable numerical comparison.
why it matters
This definition supplies the conventional inflationary benchmark inside the COS-004 module, enabling explicit comparison with the Recognition Science account that treats the eight-tick octave as a universal ledger property rather than a local causal process. It therefore sits at the interface between the standard T7 eight-tick construction and the J-cost minimization that enforces homogeneity as a consistency condition. The module doc-comment notes that the ledger structure itself provides the required synchronization without light-speed communication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.