cert
plain-language theorem explainer
Packages a domain-coverage milestone certificate: the domain cost vanishes on every nonzero diagonal pair, and the canonical threshold is strictly positive. Anyone needing an inhabited MilestoneCert for FinalModule_1397 cites this. It is a pure structure construction wiring two sibling lemmas into the certificate fields.
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_1397 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 domain-coverage certificate rather than a new dynamical law.
The certificate type is a two-field structure. The first field demands that the module's domain cost functional evaluates to zero whenever both arguments equal the same nonzero real. The second demands that a fixed positive real, the canonical threshold, is strictly above zero. Both obligations are discharged by named sibling results in the same file (domainCost_at_eq and canonicalThreshold_pos).
Imports pull Mathlib together with the RS constants and cost layers, so the cost functional and threshold live in the standard RS cost calculus (J-cost and related defect measures), not in an ad-hoc local definition.
proof idea
Definitional structure construction, not a tactic proof. The two fields of MilestoneCert are filled by direct assignment: the diagonal-vanishing field is set to the sibling lemma that proves domain cost is zero on nonzero diagonal pairs, and the positivity field is set to the sibling lemma that proves the canonical threshold is positive. No further rewriting or case analysis occurs.
why it matters
Gives an explicit inhabitant of the milestone certificate for FinalModule_1397, which the module doc frames as the structural certificate for domain coverage. Downstream, the sibling cert_inhabited and any consumer that requires a MilestoneCert value can point here instead of rebuilding the pair of obligations. In the broader RS ledger this is bookkeeping for a coverage pass, not a step of the T0–T8 forcing chain; it records that the local domain cost and threshold obligations are closed with no axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.