cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into an inhabited wave-particle duality certificate. Anyone citing the J-cost account of complementarity (wave limit cost 0, particle limit cost 1) would point here. The body is a pure structure constructor: three sibling lemmas are assigned to the three certificate fields.
Claim. There is an inhabited wave-particle duality certificate: the domain cost vanishes on the diagonal ($\mathrm{domainCost}(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
The module treats wave-particle duality as a continuous transition in J-cost between a pure-interference (wave) limit at cost 0 and a pure-detection (particle) limit at cost 1. Recognition Science identifies complementarity with that continuous path rather than with a discrete dichotomy.
The certificate structure bundles three elementary properties of the domain cost used in that story: vanishing when the two arguments are equal and nonzero, nonnegativity for positive mass and energy-like arguments, and positivity of a fixed canonical threshold. Upstream, the general recognition-event cost is already known to be nonnegative via the standard J-cost nonnegativity lemma (cost of any recognition event is $\ge 0$).
Sibling lemmas in the same file discharge each field: equality on the diagonal, nonnegativity of the domain cost, and positivity of the threshold.
proof idea
Pure structure inhabitation. The three certificate fields are filled by direct assignment of the corresponding sibling lemmas: diagonal vanishing, domain-cost nonnegativity, and canonical-threshold positivity. No additional tactics or algebraic work.
why it matters
Closes the certificate side of the structural theorem "wave-particle duality from J-cost" (module status: 0 sorry, 0 axiom). In the Recognition framework this is the bookkeeping object that records the three inequalities and identities needed before one can speak of a continuous J-cost path from wave ($J=0$) to particle ($J=1$). It sits under the Foundation forcing narrative that derives physical structure from the unique J-cost (T5) and the Recognition Composition Law; no downstream consumers are wired yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.