RSSTDStructural003Cert
plain-language theorem explainer
Certificate bundle for the RS Standard Model structural count-law module: diagonal vanishing of the domain cost, nonnegativity of that cost on positive reals, and positivity of the canonical threshold. Downstream code cites it as the single witness type for the package. Pure structure of propositions; no proof body.
Claim. A structural certificate is a triple of assertions: the domain cost vanishes on the diagonal, $C(r,r)=0$ for every real $r\neq 0$; the domain cost is nonnegative whenever both arguments are positive; and the canonical threshold is strictly positive.
background
This module packages the RS count law $2^D-1=7$ independent channels, exact once spatial dimension is fixed at $D=3$. Status is structural: zero sorry, zero axiom. The certificate sits beside a domain cost $C(m,e)$ on positive reals and a canonical threshold scalar used as a positivity gate.
Upstream, recognition cost is already known to be nonnegative: every recognition event has cost $0\le e.\mathrm{cost}$, via nonnegativity of the $J$-cost at positive state. The identity event sits at the $J$-minimum $x=1$. The present fields lift that nonnegativity pattern to the Standard Model domain cost and add diagonal vanishing plus threshold positivity.
Notation: $C$ is the module-local domain cost; the threshold is the module-local positive cutoff. Both are defined as siblings in the same file and only appear here as field types.
proof idea
No proof: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that witness.
why it matters
Gives a single named type for the structural side-conditions of RS Standard Model module 3 (count law $2^D-1=7$ from $D=3$). Downstream, cert assembles the three sibling lemmas into one value of this type, and cert_inhabited records that the type is nonempty. That pattern lets later SM structural results demand one certificate rather than three separate hypotheses.
Framework link: the count $7=2^3-1$ is the channel count forced once T8 fixes $D=3$ spatial dimensions (and T7 the eight-tick octave $2^3$). The cost fields echo the global $J$-cost nonnegativity and identity minimum from the forcing chain, specialized to the SM domain cost. No open sorry is closed here; the declaration is the interface those lemmas inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.