cert
plain-language theorem explainer
Packages three structural facts on domain cost into one certificate: cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the RS structural module on the eight-tick lattice would use this bundle. The definition is a structure instance that wires three sibling lemmas.
Claim. There is a certificate recording that $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, that $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_005 treats the eight-tick structural layer of Recognition Science: one full traversal of the binary recognition lattice has period $2^D=8$ (the T7 octave with $D=3$). Status is structural theorem, zero sorry and zero axiom.
Domain cost is the local cost functional on pairs of positive reals (measure versus expectation). The certificate structure demands three properties: vanishing when the two arguments agree and are nonzero; nonnegativity on the positive quadrant; and positivity of a fixed canonical threshold. Upstream, the foundation layer already has nonnegativity of recognition-event cost via the J-cost ($J(x)=(x+x^{-1})/2-1$), which underwrites the domain-cost nonnegativity field.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra is performed at this site.
why it matters
Gives a single named inhabitant of the structural certificate for module 5, so downstream code can depend on one object rather than three separate lemmas. The module sits on the eight-tick forcing step (T7: period $2^3=8$), the lattice traversal that pairs with T8 ($D=3$). No used-by edges are recorded yet; the natural consumer is any theorem that assumes the full structural package (diagonal vanishing, cost nonnegativity, positive threshold) rather than piecemeal hypotheses. Closes the certificate side of a zero-sorry structural module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.