ReionizationCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive numerical redshift values from the forcing chain.
- Does not prove the physical identification of each epoch name with observed intervals.
- Does not establish the transition dynamics between successive epochs.
- Does not address consistency with the spatial dimension D = 3.
formal statement (Lean)
42structure ReionizationCert where
43 five_epochs : Fintype.card ReionizationEpoch = 5
44 phi_ratio : ∀ k, boundaryRedshift (k + 1) / boundaryRedshift k = phi
45 boundary_always_pos : ∀ k, 0 < boundaryRedshift k
46