cert
plain-language theorem explainer
Packages three elementary facts about the structural domain cost into a single certificate: the cost vanishes on the diagonal, is nonnegative off it for positive arguments, and the canonical threshold is strictly positive. Anyone citing the module-level structural theorem for the T5–T8 forcing chain can point at this inhabited certificate. The definition is a pure field-by-field assembly of three already-proved sibling lemmas.
Claim. There exists a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $\tau$ obeys $\tau>0$.
background
Module RS_MTH_Structural_009 sits in the mathematics layer of the Recognition Science forcing chain (T5 J-uniqueness through T8 spatial dimension three). It is marked structural: zero sorry, zero axioms.
The local cost is a real bivariate function domainCost on nonzero/positive reals. Sibling lemmas already show it is zero when both arguments agree, and nonnegative when both are positive. A separate constant canonicalThreshold is proved strictly positive. These three facts are the only fields of the structure RSMTHStructural009Cert.
Upstream, the foundation layer already has nonnegativity of recognition-event cost via the J-cost (cost_nonneg: "The cost of any recognition event is non-negative"), which motivates the same sign convention here for the structural domain cost.
proof idea
One-line structure instance. Each field is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Gives a single named inhabitant that downstream structural results can require instead of three separate hypotheses. The module frames this as part of the RS forcing chain from T5 (J-uniqueness, $J(x)=(x+x^{-1})/2-1$) through T6 ($\varphi$ fixed), T7 (eight-tick octave), and T8 ($D=3$). No used_by edges are recorded yet; the companion cert_inhabited and any later structural theorems in the same series are the natural consumers. Closes the certificate side of Structural Module 9 with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.