WPDuality3Cert
plain-language theorem explainer
A certificate bundling three elementary facts about the wave–particle domain cost: it vanishes on the diagonal, stays non-negative off the diagonal for positive arguments, and the canonical threshold is positive. Anyone citing the structural wave–particle duality theorem from J-cost uses this bundle. It is a pure structure definition; inhabitance is discharged separately by wiring the three sibling lemmas.
Claim. A certificate consists of three properties of the domain cost $C$ and the canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats wave–particle complementarity as a continuous transition in J-cost between a pure-interference (wave) limit and a pure-detection (particle) limit. Concretely, the domain cost $C(m,e)$ is the J-cost of the ratio of the two path amplitudes (or measurement channels); the Recognition Composition Law forces $J(x)=(x+x^{-1})/2-1$, so $C$ vanishes exactly when the ratio is $1$ and is non-negative elsewhere.
The canonical threshold $\tau$ marks the crossover scale separating the wave-dominated and particle-dominated regimes. Upstream, ObserverForcing already records that every recognition-event cost is non-negative via $J\ge 0$ on the positive reals. The three fields of this structure simply package the corresponding statements for the domain cost and the threshold, ready for a single inhabitance proof.
proof idea
No proof body: the declaration is a structure (data bundle). The three fields are Prop-valued requirements. Downstream, cert fills them by direct assignment of the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then exhibits non-emptiness by ⟨cert⟩.
why it matters
This certificate is the interface that the structural wave–particle duality theorem exposes. Downstream cert and cert_inhabited show the interface is realized with zero sorry and zero axioms, matching the module claim that complementarity is a continuous J-cost transition (wave limit $J=0$, particle limit $J=1$). It sits in the Foundation layer that derives physical dualities from the unique J forced by the Recognition Composition Law (T5), rather than postulating them. Parent consumers only need Nonempty of this structure; they never re-prove diagonal vanishing or non-negativity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.