CosmologicalEpoch
plain-language theorem explainer
The inductive type enumerates the five canonical cosmological epochs as distinct constructors. Recognition Science cosmologists cite it when establishing that configDim equals five and when certifying depth via cardinality. The definition is a direct inductive enumeration that derives decidable equality, representation, boolean equality, and finite type instances automatically.
Claim. The set of cosmological epochs is the inductive type consisting of the five constructors inflation, radiation-dominated, matter-dominated, dark-energy-dominated, and future de Sitter.
background
In the Cosmology Depth from RS module the five epochs are identified with configDim D = 5. Each epoch corresponds to a distinct J-cost regime in the recognition field: inflation has J approaching zero at reheating, radiation has thermal J-cost, and dark energy has J locked yielding Lambda_RS = 8 phi^5 / 45 approximately 1.91. The module states that Lean realizes this as exactly five epochs with zero sorry or axiom.
proof idea
The declaration is a direct inductive type with five constructors, from which the instances DecidableEq, Repr, BEq, and Fintype are derived via the deriving clause.
why it matters
This definition supplies the finite set whose cardinality is established as five by the downstream theorem cosmologicalEpochCount and is embedded in the CosmologyDepthCert structure. It realizes the A2/B12 claim that five epochs match configDim D = 5, connecting to the forcing chain landmarks T7 eight-tick octave and T8 D = 3. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.