cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the structural certificate for Foundation module 3 (RS Count Law: 2^D−1=7 channels from D=3). Anyone who needs a single inhabited witness that the cost vanishes on the diagonal, stays non-negative, and has a positive threshold cites this. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is 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 $T$ obeys $T>0$.
background
Module 3 of the Foundation structural series records the RS Count Law: with spatial dimension $D=3$ forced upstream, the number of independent channels is $2^D-1=7$. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three cost-side obligations used by that count. The domain cost $C(m,e)$ is the local cost functional on positive real pairs (model and evidence scales). Its diagonal vanishing $C(r,r)=0$ and non-negativity for positive arguments are the minimal analytic properties needed before any threshold comparison. The canonical threshold is the positive cutoff against which those costs are later compared.
Upstream, non-negativity of recognition-event cost is already known from ObserverForcing via the J-cost: every recognition event has cost $\ge 0$ because $J$ is non-negative on the positive reals. The present certificate lifts the analogous statements to the domain-cost interface used by this structural module.
proof idea
One-line structure instance. The three fields of RSFDNStructural003Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity on the positive quadrant), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives a single named witness that the cost interface for Structural Module 3 is inhabited. The module itself is the RS Count Law step: $2^D-1=7$ independent channels, exact once $D=3$ is fixed. That dimension count is the T8 landmark of the forcing chain (three spatial dimensions). Downstream consumers that need an RSFDNStructural003Cert value can take this definition rather than reassemble the three obligations. No further used-by edges are recorded yet; the immediate sibling cert_inhabited is the natural next consumer. The declaration closes no open scaffold; it only packages already-proved local facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.