RSAstro006Cert
plain-language theorem explainer
Certificate structure packing three structural facts for the short-GRB duration module: diagonal vanishing of the domain cost, nonnegativity of that cost on positive arguments, and positivity of the canonical threshold. Anyone checking the RS short-GRB timing band (φ^{-2} to φ^{-1} s) cites this interface. It is pure packaging; a separate definition inhabits it by assigning the three sibling lemmas.
Claim. A certificate with three fields: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Astrophysics RS Module 6 treats short gamma-ray burst durations. Recognition Science places the short-GRB window on the phi ladder between $\phi^{-2}$ and $\phi^{-1}$ seconds (roughly 0.382--0.618 s), inside the observational 0.1--2 s range. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom).
The domain cost is the module-local cost on pairs of positive reals (model scale versus evidence scale). Its diagonal vanishing and nonnegativity echo the global J-cost calculus. Upstream, the observer-forcing result states that the cost of any recognition event is nonnegative, via nonnegativity of $J$. The canonical threshold is the positive scale cut that marks the short-duration band in this module.
proof idea
Structure definition only: three Prop fields and no proof body. Inhabitation is not proved here. The sibling definition cert fills the fields by assigning the already-proved lemmas on diagonal vanishing of the domain cost, nonnegativity of the domain cost, and positivity of the canonical threshold. The nonempty theorem is then the trivial constructor application.
why it matters
This certificate is the formal gate for Module 6's claim that short GRB durations sit in the phi-ladder window $\phi^{-2}$--$\phi^{-1}$. Downstream, one definition builds a concrete inhabitant and a one-line theorem records that the certificate type is nonempty, closing the module as a structural theorem. The packaging ties the astrophysics layer to the same cost nonnegativity forced in observer forcing and the primitive recognition calculus, so the GRB timing match stays inside the RS cost framework rather than as an external numerical fit. It does not itself invoke T5--T8, but inherits the J-cost minimum structure those steps force.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.