cert
plain-language theorem explainer
Packages the three structural facts needed for the pulsar-period module certificate: the domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Astrophysicists citing the RS pulsar timing band (φ^{-1} s typical, φ^{-10} s millisecond) use this bundle. The definition is a pure structure inhabitant wiring three already-proved local lemmas.
Claim. There exists a certificate for Astrophysics Module 10 consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 10 of the RS astrophysics layer treats pulsar periods on the φ-ladder: the typical scale is $\phi^{-1},\mathrm{s}\approx 0.618,\mathrm{s}$ and the millisecond scale is $\phi^{-10},\mathrm{s}\approx 8.1,\mathrm{ms}$. The module is marked structural (zero sorry, zero axiom).
The local cost domainCost is the recognition cost specialized to this domain; its diagonal vanishing and nonnegativity mirror the global J-cost properties (J-cost is nonnegative and minimized at the identity ratio). Upstream, cost_nonneg from ObserverForcing states that every recognition event has nonnegative cost, via Jcost_nonneg.
RSAstro010Cert is the structure that packages exactly three obligations: diagonal cost zero, off-diagonal nonnegativity under positive arguments, and positivity of canonicalThreshold. The definition cert is the concrete inhabitant of that structure.
proof idea
One-line structure construction. Each field is filled by a sibling lemma already proved in the same module: cost_at_eq by domainCost_at_eq, cost_nonneg by domainCost_nonneg, and threshold_pos by canonicalThreshold_pos. No additional tactic work; the definition merely assembles those three facts into the certificate record.
why it matters
Gives a single named certificate object for the pulsar-period structural theorem in RS Astrophysics Module 10. Downstream consumers can depend on cert rather than on the three separate lemmas. The module anchors the φ-ladder timing scales (typical $\phi^{-1},\mathrm{s}$, millisecond $\phi^{-10},\mathrm{s}$) inside the broader Recognition forcing chain, where φ is the self-similar fixed point (T6) and the cost law descends from J-uniqueness (T5) and the Recognition Composition Law. With used_by currently empty, this is a leaf certificate ready for higher astrophysics aggregation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.