cert
plain-language theorem explainer
Packages two local facts into a MilestoneCert witness for FinalModule_1395: domain cost vanishes on the diagonal for every nonzero real, and the canonical threshold is positive. Domain-coverage auditors and milestone trackers cite it as the structural certificate for this pass. The body is a one-line structure constructor wiring the two sibling lemmas.
Claim. There is a milestone certificate whose fields are: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals zero; (ii) the canonical threshold is strictly positive.
background
FinalModule_1395 is a Recognition Science milestone module (Plan v7, 109th pass) whose stated status is a structural theorem with zero sorry and zero axioms. Its role is a structural certificate for domain coverage.
MilestoneCert is the local certificate structure. It demands two propositions: the domain cost functional evaluates to zero whenever both arguments equal the same nonzero real $r$, and a fixed positive real called the canonical threshold. Domain cost is the module's cost-on-domain pairing (imported Cost/Constants infrastructure); the diagonal vanishing identity is the coverage sanity check that equal nonzero inputs incur no residual cost.
The certificate does not re-prove physics constants or the forcing chain; it only bundles the two local obligations that the milestone treats as the coverage gate.
proof idea
One-line structure value. Field cost_at_eq is filled by the sibling lemma domainCost_at_eq; field threshold_pos is filled by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Gives the inhabited MilestoneCert that marks FinalModule_1395 as a closed structural domain-coverage milestone in the RS physics layer. Downstream, cert_inhabited and any aggregator that requires a MilestoneCert instance can point here rather than reassemble the two obligations. It sits downstream of the Cost/Constants imports and upstream of any plan-v7 pass checklist that counts certified modules. It does not itself invoke T5–T8, RCL, or the mass ladder; it only certifies the local cost-diagonal and threshold gates those layers assume when domain coverage is claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.