cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the structural certificate for RS Standard Model module 3 (the count law 2^D-1=7 from D=3). Anyone who needs an inhabited witness that the module's cost and threshold axioms hold cites this value. The body is a pure structure assembly: three already-proved sibling lemmas are wired into the certificate fields.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
Module 3 of the RS Standard Model structural layer encodes the count law $2^D-1=7$ independent channels, forced exactly by the $D=3$ configuration dimension (forcing chain T8). Status is structural: zero sorry, zero axioms.
The certificate structure demands three properties of a real bivariate domain cost $C$ and a positive real threshold $T$: vanishing on the diagonal away from zero, nonnegativity on the positive quadrant, and positivity of $T$. Domain cost is the local cost functional used to score recognition mismatch in this module; nonnegativity is the same qualitative constraint that the global J-cost obeys (upstream: cost of any recognition event is nonnegative).
Sibling lemmas already establish each field: diagonal vanishing, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold.
proof idea
Pure structure construction, not a tactic proof. The three certificate fields are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further rewriting or case analysis occurs; the definition is the inhabited witness itself.
why it matters
Gives the concrete inhabited certificate that the structural layer of module 3 is well-formed: cost axioms and threshold positivity hold, so the count-law package $2^D-1=7$ sits on a nonnegative cost with a positive decision threshold. Downstream consumers (none yet linked in the graph) and the sibling inhabitance lemma can point at this value rather than re-proving the three facts. Ties directly to the D=3 forcing landmark and the RS claim that the seven independent Standard Model channels are configuration-dimension exact, not phenomenological. Closes no open sorry; it is the definitional witness inside an already-sorry-free structural module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.