reionizationCert
plain-language theorem explainer
The reionizationCert definition supplies a concrete certificate asserting exactly five reionization epochs whose boundary redshifts form a geometric progression with common ratio phi and remain strictly positive. Cosmologists modeling early universe structure formation within the Recognition Science framework would cite this certificate when invoking the five-epoch ladder. The definition is assembled directly from three prior results: the cardinality theorem for ReionizationEpoch, the ratio theorem for consecutive boundaries, and the positivity
Claim. Define a certificate structure requiring that the number of reionization epochs equals five, that consecutive boundary redshifts satisfy $z_{k+1}/z_k = phi$ for all $k$, and that every boundary redshift satisfies $0 < z_k$. Populate the structure by assigning the epoch count from the cardinality result, the ratio property from the geometric progression theorem, and the positivity property from the power positivity theorem.
background
The module sets out a reionization history of five epochs (= configDim D = 5): cosmic dark ages (z > 20), first stars (z ~ 20), galaxy formation (z ~ 15), bulk reionization (z ~ 7-10), saturation (z < 6). Each boundary redshift occupies one rung on a geometric ladder. The ReionizationCert structure packages three properties: Fintype.card ReionizationEpoch = 5, the constant ratio phi between consecutive boundaries, and strict positivity of all boundaries. Upstream, phi_ratio originates from the quasicrystal definition as 1/phi; the redshift theorems prove the ratio via unfolding and ring simplification and prove positivity via pow_pos.
proof idea
The definition constructs the ReionizationCert instance by direct field assignment: five_epochs receives the reionizationEpoch_count theorem, phi_ratio receives the redshift_ratio theorem, and boundary_always_pos receives the redshift_pos theorem. No additional reasoning steps are performed.
why it matters
This definition supplies the canonical certificate for the five-epoch reionization ladder in Recognition Science cosmology. It realizes the geometric progression of boundary redshifts required by the phi-ladder and closes the local module by providing a single reference object for the entire history. It connects to the framework through the use of phi as the self-similar fixed point and the five-epoch count matching configDim D = 5. No open questions are addressed; the construction is complete within the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.