cert
plain-language theorem explainer
Packages three structural facts into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cited by any QFT structural argument that needs a single inhabited witness for module 9. The body is a pure record assembly of three sibling lemmas; no new mathematics is proved here.
Claim. There is a structural certificate whose fields assert: (i) for every real $r\neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 9 sits in the QFT layer of the Recognition Science forcing chain (T5 J-uniqueness through T8, $D=3$). Status is structural: zero sorry, zero axioms. The local cost is a two-argument domain cost on reals (mass/energy style pairs), not the bare one-argument J-cost $J(x)=(x+x^{-1})/2-1$, though nonnegativity ultimately traces to $J\ge 0$.
The certificate structure bundles three Prop fields: diagonal vanishing of domain cost, nonnegativity on the positive quadrant, and positivity of a fixed canonical threshold. Upstream, ObserverForcing records that every recognition event has nonnegative cost via Jcost_nonneg at a positive state; the domain-cost nonnegativity field is the QFT-facing analogue of that fact.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos already discharge the three fields; this definition only names the packed witness.
proof idea
Definitional record construction, not a tactic proof. The three structure fields are filled by direct assignment: diagonal vanishing from domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No rewriting or case analysis occurs in the body.
why it matters
Gives a single named inhabitant of the module-9 structural certificate so downstream QFT arguments can depend on one object rather than three separate lemmas. The module header places this in the RS forcing spine T5 (J-uniqueness) $\to$ T6 ($\varphi$ fixed) $\to$ T7 (eight-tick octave) $\to$ T8 ($D=3$), as a structural theorem with empty axiom surface.
No used_by edges are recorded yet; the natural consumer is any lemma that assumes an RSQFTStructural009Cert (for example the sibling cert_inhabited). The certificate does not itself advance a paper proposition beyond packaging the local cost and threshold facts required by the QFT structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.