reionizationEpoch_count
plain-language theorem explainer
The declaration establishes that the reionization epochs form a finite type with exactly five elements. Researchers modeling cosmic reionization within Recognition Science would reference this cardinality to align with the five-stage ladder. The proof proceeds by a single decision tactic that counts the constructors of the inductive definition.
Claim. The set of reionization epochs has cardinality five: $|E| = 5$, where $E$ consists of the five stages cosmic dark ages, first stars, galaxy formation, bulk reionization, and saturation.
background
The module discretizes reionization history into five epochs that match configDim D = 5. The inductive type enumerates them explicitly as darkAges, firstStars, galaxyFormation, bulkReionization, and saturation, with each boundary redshift placed on a geometric ladder. Module documentation states that these five stages cover cosmic dark ages (z > 20), first stars (z ~ 20), galaxy formation (z ~ 15), bulk reionization (z ~ 7-10), and saturation (z < 6).
proof idea
The proof is a one-line wrapper that invokes the decide tactic on Fintype.card applied to the inductive type, which enumerates the five constructors and returns the equality.
why it matters
This cardinality supplies the five_epochs component of the downstream reionizationCert definition. It directly realizes the five-epoch structure (= configDim D = 5) required by the module for the geometric redshift ladder. The result anchors the discrete epoch count used in Recognition Science cosmology calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.