cert
plain-language theorem explainer
Packages two elementary facts (diagonal vanishing of the domain cost and positivity of the canonical threshold) into a single MilestoneCert witness for FinalModule_1400. Cited by anyone treating this module as a closed structural certificate for domain coverage. Proof is a one-line structure constructor wiring the two sibling lemmas.
Claim. There is a milestone certificate whose two fields assert: (i) for every real $r \neq 0$, the domain cost on the diagonal vanishes, $\mathrm{cost}(r,r)=0$; (ii) the canonical threshold is strictly positive, $0 < \tau_{\mathrm{can}}$.
background
FinalModule_1400 is a Recognition Science milestone module (Plan v7, 109th pass) whose stated status is a structural theorem with zero sorry and zero axioms. It certifies domain coverage rather than a new dynamical law.
The ambient cost infrastructure comes from IndisputableMonolith.Cost (with constants from IndisputableMonolith.Constants). The local domain cost is a real bivariate cost; the sibling lemma domainCost_at_eq records that its diagonal is identically zero off the origin. The sibling canonicalThreshold is a fixed positive real cutoff used as the acceptance bar for the milestone.
MilestoneCert is the two-field structure that packages exactly those obligations: diagonal vanishing of the domain cost, and positivity of the canonical threshold. The present declaration is the concrete inhabitant of that structure.
proof idea
One-line structure constructor. The first field is filled by the sibling lemma that domainCost r r = 0 for all nonzero real $r$. The second field is filled by the sibling lemma that the canonical threshold is strictly positive. No further rewriting or case analysis occurs.
why it matters
Gives the module its closed structural certificate: once cert exists, FinalModule_1400 can be treated as a finished domain-coverage milestone (0 sorry, 0 axiom) rather than an open stub. Downstream, the sibling cert_inhabited and any aggregator that consumes MilestoneCert values can point at this witness.
In the broader Recognition framework this is bookkeeping, not a forcing-chain step: it does not re-derive J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8). It only records that the local domain cost and threshold obligations for this milestone are discharged, so the module can sit in the structural layer of the physics stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.