cert
plain-language theorem explainer
Packages two structural facts into a domain-coverage milestone certificate: the domain cost vanishes on equal nonzero arguments, and the canonical threshold is strictly positive. Anyone citing the FinalModule_1398 coverage milestone uses this witness. Construction is a structure instance that wires two already-proved sibling lemmas.
Claim. There is a milestone certificate whose data are: (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
This module is a Recognition Science structural certificate for a domain-coverage milestone (Plan v7, 109th pass). Status is zero sorry and zero axiom: pure packaging of already-closed facts.
The certificate type demands two fields. The first is a diagonal vanishing law for the local domain cost: on any nonzero real $r$, evaluating the cost at the equal pair $(r,r)$ yields zero. The second is positivity of a fixed canonical threshold used as the acceptance cutoff for the milestone.
Both ingredients are supplied by in-module siblings (domainCost_at_eq and canonicalThreshold_pos). The ambient cost language sits on the RS cost stack imported from Constants and Cost, where the J-cost and related defect measures live; this module only records the domain-level diagonal and threshold facts needed for the coverage stamp.
proof idea
One-line structure instance. The definition fills MilestoneCert by assigning the existing lemma that the domain cost vanishes on equal nonzero arguments to the cost_at_eq field, and the existing positivity proof for the canonical threshold to the threshold_pos field. No new arithmetic is performed.
why it matters
Gives the inhabited milestone certificate for FinalModule_1398, the structural stamp that domain coverage holds under the stated cost and threshold conditions. Downstream, the sibling inhabitance fact can point at this value as the concrete witness. In the broader RS forcing picture it is bookkeeping rather than a new T0–T8 step: it records that the local domain cost is calibrated (zero defect on matched arguments) and that the acceptance threshold is a genuine positive scale, so the coverage milestone is not vacuous. No open scaffold remains in this file; the certificate is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.