cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate structure for Structural Module 3. Anyone citing the RS count-law scaffolding (seven independent channels from D=3) can point at this inhabited record. The definition is a pure field assembly: each obligation is discharged by a named sibling lemma.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments: $m>0$, $e>0$ imply $\mathrm{domainCost}(m,e)\ge 0$; and (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_003 packages the RS Count Law: with spatial dimension $D=3$ forced upstream (T8), the number of independent channels is $2^D-1=7$. Status is structural (zero sorry, zero axiom).
The certificate structure bundles three cost-side obligations used by that count-law story. Domain cost is the local cost functional on pairs of positive reals (imported from the Cost layer and Constants). The first field demands that equal nonzero arguments sit at cost zero; the second demands nonnegativity on the positive orthant; the third demands that the module's canonical threshold is positive.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The present certificate specializes that spirit to the domain-cost pair used in this structural module.
proof idea
One-line structure instance. The three fields of RSMTHStructural003Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only witnesses that those three facts inhabit the certificate record.
why it matters
Gives an inhabited certificate object for Structural Module 3 so downstream count-law arguments can depend on a single named package rather than three scattered lemmas. The module frames the RS Count Law $2^D-1=7$ as exact once $D=3$ is fixed by the forcing chain (T8). No used_by edges are recorded yet; the natural consumer is any theorem that needs diagonal vanishing, nonnegativity, and a positive threshold in one hypothesis. Closes the certificate side of a zero-sorry structural module rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.