ReionizationEpoch
plain-language theorem explainer
ReionizationEpoch enumerates the five stages of cosmic reionization as an inductive type with constructors for dark ages, first stars, galaxy formation, bulk reionization, and saturation. Cosmologists working in the Recognition Science framework cite this enumeration when building certificates that enforce a geometric ladder of boundary redshifts. The definition is a direct listing of the five cases together with automatic derivation of Fintype, DecidableEq, Repr, and BEq instances.
Claim. The inductive type of reionization epochs consists of five constructors: dark ages, first stars, galaxy formation, bulk reionization, and saturation.
background
The Reionization History from RS module partitions reionization into five epochs that realize configDim D = 5. These comprise the cosmic dark ages (z > 20), first stars (z ~ 20), galaxy formation (z ~ 15), bulk reionization (z ~ 7-10), and saturation (z < 6). Each boundary redshift is required to sit one rung on a geometric ladder scaled by the golden ratio phi.
proof idea
The declaration is a direct inductive definition that lists the five constructors and invokes the deriving clause for DecidableEq, Repr, BEq, and Fintype.
why it matters
This definition supplies the finite set of epochs that ReionizationCert uses to assert Fintype.card = 5 together with the phi-ratio property on consecutive boundary redshifts. It directly implements the five-epoch partition stated in the module documentation and aligns with the Recognition Science requirement that reionization history follows the geometric ladder with D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.