ReionizationEpoch
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign explicit numerical redshift values to any boundary.
- Does not prove the phi-ratio between consecutive boundaries.
- Does not link epochs to mass or energy scales on the phi-ladder.
- Does not incorporate observational data or constraints.
formal statement (Lean)
19inductive ReionizationEpoch where
20 | darkAges
21 | firstStars
22 | galaxyFormation
23 | bulkReionization
24 | saturation
25 deriving DecidableEq, Repr, BEq, Fintype
26