cert
plain-language theorem explainer
Packages two local facts into a MilestoneCert witness for FinalModule_1399: domain cost vanishes on the diagonal for every nonzero real, and the canonical threshold is strictly positive. Cited by anyone auditing structural domain-coverage milestones in the RS physics stack. Construction is a pure structure literal wiring two already-proved sibling lemmas.
Claim. The milestone certificate for FinalModule_1399 is the pair of statements that $\mathrm{domainCost}(r,r)=0$ for every real $r\neq 0$, and that the canonical threshold is strictly positive.
background
FinalModule_1399 is a structural milestone module in the Recognition Science physics layer (Plan v7, 109th pass). Its stated status is a structural theorem with zero sorry and zero axioms: a domain-coverage certificate rather than a dynamical derivation.
The certificate type is the structure MilestoneCert, whose two fields are (i) diagonal vanishing of the domain cost for every nonzero real argument, and (ii) strict positivity of a fixed canonical threshold. Domain cost is the local cost functional imported from the Cost and Constants modules; on the diagonal it records self-comparison of a scale $r$ with itself, which RS expects to be zero away from the singular point $r=0$.
The module therefore sits downstream of the J-cost apparatus (the unique cost forced by the Recognition Composition Law) only insofar as domainCost is built from that stack; the certificate itself does not re-derive J-uniqueness or the forcing chain T5–T8.
proof idea
One-line structure constructor. The field cost_at_eq is filled by the sibling lemma domainCost_at_eq; the field threshold_pos is filled by the sibling lemma canonicalThreshold_pos. No additional tactics or algebraic work occur at this declaration.
why it matters
Gives the inhabited MilestoneCert that marks FinalModule_1399 as a closed structural domain-coverage milestone. Downstream, cert_inhabited and any audit harness that demands a MilestoneCert instance can point here rather than reassemble the two field proofs. In the broader RS stack this is bookkeeping for domain coverage, not a step of the T0–T8 forcing chain, the mass ladder, or the alpha band; it records that the local cost and threshold obligations for this module are discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.