cosmologicalEpochCount
plain-language theorem explainer
The declaration asserts that the finite type of cosmological epochs has exactly five elements. Researchers modeling cosmology within Recognition Science would reference this count when mapping the sequence of epochs to the configuration dimension. The proof proceeds via a single decide tactic application on the Fintype instance automatically derived from the inductive enumeration of the five epochs.
Claim. The cardinality of the set of cosmological epochs is five: $|$CosmologicalEpoch$| = 5$.
background
The module CosmologyDepthFromRS identifies five canonical cosmological epochs—inflation, radiation-dominated, matter-dominated, dark energy-dominated, and future de Sitter—corresponding to configDim D = 5. Each epoch corresponds to a distinct J-cost regime in the recognition field, with inflation at J approaching zero at reheating and dark energy locked at J = J(φ). The upstream inductive definition CosmologicalEpoch enumerates these five cases and derives the Fintype instance used here.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This succeeds because the inductive type CosmologicalEpoch derives DecidableEq, Repr, BEq, and Fintype, allowing Lean to compute the cardinality as five directly.
why it matters
This result supplies the five_epochs field for the downstream CosmologyDepthCert definition. It realizes the A2/B12 claim that five epochs equal configDim D = 5 in the RS framework, linking to the broader forcing chain where spatial dimensions are fixed at three but configuration depth reaches five. No open questions are flagged in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.