RSASTStructural005Cert
plain-language theorem explainer
Packages three structural side-conditions for Astrophysics module 5: the domain cost vanishes on the diagonal for nonzero radius, stays nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Downstream code cites the type when building or inhabiting the module certificate. As a structure definition it carries no proof body; the three fields are pure Prop obligations filled by sibling lemmas.
Claim. A certificate for RS astrophysics structural claim 5 is a triple of statements: (i) for every real $r\neq 0$, the domain cost at equal arguments vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for all $m>0$ and $e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module 5 sits in the RS astrophysics structural layer tied to the eight-tick octave: one full traversal of the binary recognition lattice has period $2^D=8$ with $D=3$ (forcing chain T7–T8). Status is structural (zero sorry, zero axiom).
The domain cost is the local cost functional on mass/energy (or radius) pairs used in this module; sibling lemmas assert it equals zero on the diagonal and is nonnegative off it. The canonical threshold is the positive cutoff against which that cost is compared. Upstream, the foundation result that every recognition event has nonnegative cost (via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$) supplies the global nonnegativity pattern that the domain-cost field mirrors.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to those fields, and to the one-line nonempty theorem wrapping that witness.
why it matters
Gives the typed bundle that the module’s concrete certificate and its nonempty theorem inhabit, so later astrophysics structural claims can depend on a single named certificate rather than three loose lemmas. Anchors the eight-tick structural story (period $2^3=8$) in a checkable cost-and-threshold interface consistent with foundation nonnegativity of recognition cost. Does not itself advance mass-ladder or $\alpha$-band numerics; it only locks the structural preconditions those claims assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.