RSAstro010Cert
plain-language theorem explainer
Certificate bundle for astrophysics module 10 (pulsar periods on the phi ladder): diagonal domain-cost vanishes, domain-cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code cites it to inhabit the module certificate and prove Nonempty. Pure structure definition packing three Prop fields; no proof body.
Claim. A certificate for RS astrophysics module 10 is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 treats pulsar periods as phi-ladder timescales: a typical period near $\phi^{-1},\mathrm{s}\approx 0.618,\mathrm{s}$, and millisecond pulsars near $\phi^{-10},\mathrm{s}\approx 8.1,\mathrm{ms}$. The module is marked structural (zero sorry, zero axiom).
The local cost functional domainCost scores pairs of positive reals (mass- or energy-like coordinates) in this astrophysics slice. The canonical threshold is the positive cutoff that anchors the claimed period range. Upstream, recognition-event cost is already known nonnegative: any recognition event has cost $\ge 0$ because $J$-cost is nonnegative on positive states.
The certificate simply packages the three structural inequalities the rest of the module needs: vanishing on the diagonal, nonnegativity off-diagonal, and a positive threshold.
proof idea
No proof: this is a structure declaration whose fields are propositions. Inhabitation is deferred to the sibling definition that assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and to the one-line Nonempty theorem that wraps that inhabitant.
why it matters
Gives a single named type for the structural side-conditions of the pulsar-period module so downstream proofs can assume one certificate rather than three loose lemmas. Direct consumers are the canonical inhabitant and the Nonempty theorem in the same module.
In the broader Recognition framework this sits on the phi-ladder timing story (T6 forces $\phi$ as the self-similar fixed point; times and masses are read as integer rungs). The module links those rungs to the observed pulsar band ($\phi^{-1}$ typical, $\phi^{-10}$ millisecond). The certificate does not itself derive the periods; it freezes the cost and threshold hygiene the range claim depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.