cert
plain-language theorem explainer
assembles the structural certificate for short GRB durations in the phi-ladder window phi^{-2} to phi^{-1} seconds. Anyone citing the RS astrophysics match for short bursts uses this bundle. It is a pure structure inhabitant: three already-proved field lemmas are plugged in with no extra argument.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
Module 6 of the RS astrophysics layer targets short gamma-ray burst durations. The claimed window is $\phi^{-2}$ to $\phi^{-1}$ seconds (about $0.382$–$0.618,\mathrm{s}$), which sits inside the observational band $0.1$–$2,\mathrm{s}$ and is marked MATCH.
The certificate type packages the minimal analytic hygiene for a domain cost on that ladder: diagonal vanishing, nonnegativity for positive arguments, and a positive canonical threshold. Nonnegativity ultimately traces to the global fact that every recognition-event cost is nonnegative (the $J$-cost is nonnegative for positive state).
Local siblings supply the three field proofs: equality of domain cost on equal arguments, nonnegativity of domain cost, and positivity of the canonical threshold.
proof idea
One-line structure inhabitant. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Gives a single named witness that the short-GRB duration module meets its structural obligations (zero sorry, zero axiom). Downstream consumers can require this certificate rather than re-proving diagonal vanishing, cost nonnegativity, and threshold positivity. It sits in the astrophysics layer that maps phi-ladder intervals onto observed burst timescales; the module doc records an explicit MATCH for the short-duration band. No parent theorems currently depend on it in the graph, so it is an export point for later GRB or timing arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.