RSMTHStructural003Cert
plain-language theorem explainer
A certificate structure packaging three structural facts: domain cost vanishes on the diagonal, is nonnegative for positive measure and energy, and the canonical threshold is strictly positive. Cited by the module's inhabited certificate and any consumer of the RS Count Law structural package. Pure data layout; no proof body.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of $(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
Module RS_MTH_Structural_003 packages the RS Count Law: $2^D-1=7$ independent channels, forced exactly by the $D=3$ configuration dimension (T8 in the forcing chain). Status is structural theorem with zero sorry and zero axiom.
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (measure and energy). The diagonal vanishing condition says matched scales carry zero cost. Nonnegativity mirrors the upstream recognition-event fact that "the cost of any recognition event is non-negative," which itself rests on $J$-cost nonnegativity for positive states. The canonical threshold is the positive cutoff used to separate admissible from inadmissible domain configurations in the count-law argument.
proof idea
No proof: this is a structure declaration whose three fields are propositions. Inhabitation is supplied downstream by cert, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas in turn lean on the foundation nonnegativity of $J$-cost.
why it matters
Gives a single named bundle for the three numeric hypotheses needed by the RS Count Law structural package. Downstream, cert constructs an explicit inhabitant and cert_inhabited records Nonempty of the certificate type, closing the module's zero-sorry structural claim. Ties to T8 ($D=3$) via the module's count identity $2^D-1=7$, and to the nonnegativity of recognition cost that underwrites all later mass and coupling ladders. Does not itself derive the channel count; it only certifies the cost-side side conditions the count argument consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.