cert_inhabited
plain-language theorem explainer
The structural certificate packing diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold is inhabited. Anyone citing the RS Count Law module (2^D−1=7 channels from D=3) uses this as the existence witness. Proof is a one-line term: the explicit certificate constructor.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), the domain cost is nonnegative for positive arguments, and 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 theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary properties of the local cost data. Domain cost $C(m,e)$ is the cost functional on a mass/energy pair (imported from the Cost layer). The three fields require: $C(r,r)=0$ off zero, $C(m,e)\ge 0$ for $m,e>0$, and a strictly positive canonical threshold used as a comparison scale.
These are the minimal algebraic hygiene conditions needed before counting independent channels against the octave structure.
proof idea
One-line term proof. The witness cert (an explicit inhabitant of the certificate structure, assembled from the sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity) is wrapped by the Nonempty constructor. No tactics, no further lemmas.
why it matters
Closes the existence side of the structural certificate for Module 3 of the mathematics layer. The module's stated content is the RS Count Law $2^D-1=7$, exact once $D=3$ is fixed by the forcing chain (T8). Without an inhabited certificate, downstream channel-counting arguments would have no packaged hypothesis bundle.
No further used-by edges are recorded yet; the declaration is the terminal existence stamp for this certificate. It sits beside the T7 eight-tick octave and T8 dimension forcing as pure structural bookkeeping, not a dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.