cert
plain-language theorem explainer
Packages three proved facts about the QFT domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the eight-tick structural layer of RS-QFT would reach for this witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There exists 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 5 of the RS-QFT structural layer treats the eight-tick octave: one full traversal of the binary recognition lattice with period $2^D=8$ (forcing step T7). Status is structural theorem, zero sorry and zero axiom.
The domain cost is the local cost functional on mass-energy pairs used in this QFT layer. Its diagonal vanishing and nonnegativity mirror the global J-cost properties from the forcing chain (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), specialized to the recognition lattice. The canonical threshold is the positive cutoff against which domain-cost comparisons are made.
Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost, via nonnegativity of $J$. The certificate structure simply names the three Prop fields that must hold for the domain cost and threshold in this module.
proof idea
One-line structure constructor. Each field of RSQFTStructural005Cert is filled by the corresponding sibling lemma already proved in-module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No extra algebra or tactics.
why it matters
Gives a single named inhabitant of the structural certificate for Module 5, so downstream QFT arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold without reopening those lemmas. Ties directly to the eight-tick octave (T7) and the nonnegativity half of J-uniqueness (T5). No used_by edges are recorded yet; the natural consumer is any theorem that needs an inhabited RSQFTStructural005Cert (for example the sibling cert_inhabited). Closes the packaging step of a zero-sorry structural block rather than an open physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.