cert_inhabited
plain-language theorem explainer
The reionization certificate type is inhabited: a witness packs diagonal vanishing of domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Cosmology auditors cite it to discharge Nonempty goals when wiring RS redshift scaffolding. Proof is a one-constructor term handing over the prebuilt cert.
Claim. There exists a reionization certificate: a record asserting that domain cost vanishes on the diagonal for every nonzero real argument, is nonnegative whenever both arguments are positive, and that the canonical threshold is strictly positive.
background
The module places reionization redshift in Recognition Science units. Data put $z_{\mathrm{reion}}$ near 7–10; RS identifies the window $\varphi^4\approx 6.85$ through $\varphi^5\approx 11.09$ as the structural bracket, called consistent with observation. Status is structural (zero sorry, zero axiom).
A reionization certificate is a three-field record: domain cost equals zero on the diagonal for nonzero $r$; domain cost is nonnegative for positive mass and energy arguments; the canonical threshold is positive. These are the local cost axioms specialized to the reionization domain, in the same family as the J-cost $J(x)=(x+x^{-1})/2-1$.
Sibling facts supply each field (diagonal identity, nonnegativity, threshold positivity). The value cert assembles them; this theorem only records that the resulting type is nonempty.
proof idea
Pure term proof. Nonempty is introduced by its single constructor applied to the already-built structure value cert, written $\langle\mathrm{cert}\rangle$. No tactics, no lemmas beyond the existence of that witness.
why it matters
Closes the module’s structural claim by proving the certificate bundle is inhabited, so any later cosmology development can assume a reionization certificate without adding axioms. No downstream uses are recorded yet; the natural consumers are redshift-history and epoch-from-J-cost developments that share the same certificate shape.
In the broader RS chain this sits under the cost backbone (T5 J-uniqueness and the Recognition Composition Law) rather than under the forcing steps T6–T8. It does not itself compute $z_{\mathrm{reion}}$; it only certifies the cost scaffolding that the $\varphi^4$–$\varphi^5$ bracket rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.