MilestoneCert
plain-language theorem explainer
A structural certificate packing two domain-coverage facts: the domain cost vanishes on the diagonal for every nonzero real scale, and the canonical threshold is strictly positive. Physicists tracking RS milestone modules cite it as the typed witness that FinalModule_1397 has closed its coverage obligations. It is a bare structure definition, not a proved theorem.
Claim. A milestone certificate is a pair of assertions: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (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: the module asserts that a designated cost functional and threshold behave as required for the coverage claim.
The domain cost is the local cost functional on pairs of real scales (imported via the Cost and Constants layers). Vanishing on the diagonal means equal nonzero arguments incur zero cost, the fixed-point identity expected of a recognition cost. The canonical threshold is the positive cutoff used to mark when a domain contribution counts as covered.
Upstream, the module sits on the primitive recognition calculus (one-primitive structure) and the standard RS cost stack. The certificate does not re-derive the J-cost or the forcing chain; it only packages the two numerical/algebraic side conditions the milestone needs.
proof idea
No proof body: this is a structure declaration. Inhabitation is deferred to sibling constructors (cert, cert_inhabited) that supply the two fields from the companion lemmas domainCost_at_eq and canonicalThreshold_pos. The structure itself only names the interface.
why it matters
In the RS physics layer, milestone modules are typed checkpoints that a coverage or calibration obligation has been discharged without axioms. This certificate is the local witness for FinalModule_1397: diagonal vanishing of the domain cost plus positivity of the canonical threshold.
It does not itself touch the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3) or the mass ladder. It is bookkeeping infrastructure so downstream physics claims can assume domain coverage rather than re-prove the two side conditions. With empty used_by in the current graph, it is a leaf certificate for the milestone pass, not yet an input to a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.