cert
plain-language theorem explainer
Packages three proved properties of the module's domain cost and canonical threshold into a single certificate witness for RS Structural 003 (the count-law module: 2^D-1=7 channels from D=3). Anyone citing the structural certificate for this physics module uses this inhabitant. The body is a pure structure assembly: three sibling lemmas fill the three fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: for every nonzero real $r$, $\mathrm{domainCost}(r,r)=0$; (ii) domain cost is nonnegative on positive arguments; and (iii) the canonical threshold is strictly positive.
background
Module RS_PHY_Structural_003 is the structural home of the RS count law: with spatial dimension $D=3$ forced upstream (T8), one has $2^D-1=7$ independent channels. Status is structural theorem (zero sorry, zero axiom).
The certificate structure bundles three analytic side conditions on a real bivariate domain cost and a positive real threshold. Domain cost is the local cost functional used in this physics module; the diagonal-vanishing clause says equal positive arguments incur zero cost, matching the J-cost minimum at identity in the Recognition Composition Law setting. Nonnegativity is the standard cost axiom (cf. ObserverForcing: "The cost of any recognition event is non-negative").
Canonical threshold positivity supplies a strict positive cutoff against which domain-cost comparisons are made in the surrounding structural development.
proof idea
One-line structure inhabitant. The three fields of RSPHYStructural003Cert are filled by the already-proved sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No new arithmetic is performed; the definition only witnesses that those three facts inhabit the certificate type.
why it matters
Gives a single named witness that the cost/threshold side conditions of Structural 003 hold, so downstream consumers (and the sibling inhabitedness lemma) can quote one object rather than three separate facts. Sits inside the D=3 count-law module whose headline is $2^D-1=7$ independent channels, the configuration-dimension consequence of T8 in the forcing chain. No used-by edges are recorded yet; the certificate is the packaging step that closes the local structural interface for this physics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.