cert
plain-language theorem explainer
Packages a domain-coverage milestone certificate: domain cost vanishes on the diagonal for every nonzero real scale, and the canonical threshold is strictly positive. Anyone citing FinalModule_1396 as a closed structural unit uses this inhabitant. Construction is a two-field structure fill from the named equality and positivity lemmas.
Claim. There is a milestone certificate whose two fields assert: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) the canonical threshold is strictly positive.
background
FinalModule_1396 is a Recognition Science milestone module (Plan v7, 109th pass) marked as a structural theorem with no sorry and no axioms. Its role is a domain-coverage certificate: a small, checkable package that the local cost and threshold data are in the expected shape.
The certificate type has two fields. The first requires that domain cost, evaluated on equal nonzero arguments, is identically zero (the diagonal of the cost vanishes away from the origin). The second requires that the module's canonical threshold is a positive real. Both fields are pure real-analytic side conditions; they do not yet encode particle spectra or coupling values.
Sibling lemmas in the same file supply exactly those two facts: an equality lemma for domain cost on the diagonal, and a positivity lemma for the canonical threshold. The present definition only assembles them.
proof idea
Definitional structure inhabitant, not a tactic proof. The two structure fields are filled by direct assignment: the diagonal cost identity is taken from the sibling equality lemma, and threshold positivity from the sibling positivity lemma. No further rewriting or case analysis occurs.
why it matters
Gives FinalModule_1396 a single named certificate object that downstream milestone or audit code can require as a hypothesis or inhabitance witness. In the Recognition framework this is bookkeeping for domain coverage rather than a forcing-chain step (T5–T8) or a mass/coupling derivation: it records that the local cost functional is normalized on the diagonal and that the threshold used for the milestone is positive. With zero sorry and zero axioms in the module, the certificate is the closed structural token for this pass of the plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.