cert
plain-language theorem explainer
Packages three structural facts into one certificate: domain cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream consumers of Structural Module 9 cite this inhabited record rather than the three lemmas separately. Construction is a pure structure instance that wires in the sibling proofs.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Structural Module 9 sits on the RS forcing chain after T5 (J-uniqueness) through T8 ($D=3$). The module is marked structural: zero sorry, zero axioms. Its local objects are a domain cost on pairs of reals and a canonical positive threshold used as a comparison scale.
Domain cost is the module-level cost functional on pairs $(m,e)$. The certificate demands it vanish when the two arguments agree and are nonzero (identity events sit at the cost minimum), and that it stay nonnegative whenever both arguments are positive. That nonnegativity pattern matches the upstream recognition-event cost law: any recognition event has nonnegative cost, proved via nonnegativity of the J-cost on positive states.
The third field only asserts positivity of the module's canonical threshold, so the certificate can be used as a single inhabited witness rather than three separate hypotheses.
proof idea
One-line structure instance. The three fields of RSFDNStructural009Cert are filled by the sibling lemmas already proved in the same module: diagonal vanishing, domain-cost nonnegativity for positive arguments, and positivity of the canonical threshold. No extra algebra is performed at this site; the definition only assembles those proofs into the certificate record.
why it matters
Gives Structural Module 9 a single named witness that the domain-cost and threshold axioms hold. The module itself is part of the RS forcing spine (T5 J-uniqueness, T6 $\varphi$ fixed point, T7 eight-tick octave, T8 $D=3$), status structural with no sorry and no axioms. No downstream uses are recorded yet; the natural consumer is any later theorem that wants the three properties as one hypothesis rather than three. Together with the sibling inhabitedness lemma, this closes the certificate interface for the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.