ReionizationCert
plain-language theorem explainer
ReionizationCert records that reionization proceeds through exactly five epochs whose boundary redshifts form a geometric sequence with common ratio phi. Cosmologists embedding reionization inside Recognition Science would cite the certificate to fix the timeline to the phi-ladder. The structure is a direct packaging of three properties: the epoch type has cardinality five, successive boundaries satisfy the constant ratio, and all boundaries remain positive.
Claim. The structure ReionizationCert asserts that the finite type of reionization epochs has cardinality five, that the boundary redshifts satisfy $z_{k+1}/z_k = phi$ for every natural number $k$, and that every boundary redshift is strictly positive.
background
The module treats reionization as five canonical epochs whose boundaries lie on a geometric ladder. ReionizationEpoch is the inductive type with constructors darkAges, firstStars, galaxyFormation, bulkReionization and saturation. boundaryRedshift is defined by boundaryRedshift k := phi ^ k, where phi is the golden-ratio fixed point imported from Constants. The module states that each boundary redshift sits one rung on this ladder and that the construction carries zero sorry or axiom.
proof idea
This is a structure definition that directly encodes the three required properties. The fields are later supplied by the downstream definition reionizationCert, which applies the lemmas reionizationEpoch_count for the cardinality, redshift_ratio for the constant phi ratio, and redshift_pos for positivity.
why it matters
ReionizationCert supplies the concrete certificate that the reionization timeline consists of five epochs on the phi-ladder, realizing the five-epoch division required by the cosmology module. It is instantiated by reionizationCert and thereby feeds any later result that needs the certified boundary sequence. In the Recognition Science framework it aligns the reionization history with the self-similar fixed point and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.