cert
plain-language theorem explainer
Packages the three structural facts needed for the ultra-high-energy cosmic-ray certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical GZK threshold is positive. Astrophysicists working the φ-ladder GZK cutoff cite this as the inhabited witness. The body is a pure structure assembly wiring three already-proved sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C(m,e)$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical GZK energy threshold is strictly positive.
background
The module treats the Greisen–Zatsepin–Kuzmin (GZK) cutoff in Recognition Science units: cosmic-ray energies above roughly $5\times 10^{19},\mathrm{eV}$ are attenuated, and RS writes $E_{\mathrm{GZK}}=\varphi^n E_{\mathrm{proton}}$ with rung $n\approx 110$. The structural certificate for that story is the record type UHECRCert.
That record demands three properties of the local domain cost (the J-cost specialized to mass–energy pairs on the φ-ladder): vanishing when mass equals energy (the identity recognition event), nonnegativity for positive arguments, and positivity of the canonical threshold energy. Upstream, the foundation lemma that any recognition-event cost is nonnegative (via $J\ge 0$) supplies the conceptual warrant for the middle field; the concrete proofs live in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
One-line structure constructor. The three fields of UHECRCert are filled by direct reference to the already-established sibling facts domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or algebraic reduction occurs here.
why it matters
Gives an inhabited witness that the UHECR/GZK side of the φ-ladder story is structurally well-formed (zero sorry, zero axiom in the module). Downstream consumers can assume a single UHECRCert value rather than re-proving diagonal vanishing, cost nonnegativity, and threshold positivity. Ties the astrophysics layer to the foundation cost nonnegativity result and to the T5/T6 landmarks (J-uniqueness and the self-similar fixed point φ) that underwrite the rung counting $n\approx 110$. With no current reverse edges, it is the terminal packaging step for this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.