domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition cost of their ratio m/e. Anyone building the wave-particle duality certificate cites it as the continuous cost that sits at zero for pure interference and one for pure detection. It is a one-line definition wrapping the unique J-cost functional forced by the Recognition Composition Law.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module treats wave-particle duality as a continuous transition in recognition cost: pure path interference has cost 0, pure path detection has cost 1, and intermediate regimes sit between those limits. The cost functional is the unique J forced by the Recognition Composition Law (T5): $J(x)=\frac{x+x^{-1}}{2}-1$, also written $\cosh(\log x)-1$, defined on positive ratios.
Upstream, every copy of Jcost is the same noncomputable map: recognition cost of a positive ratio, strictly positive when the ratio is not 1. Domain cost simply specializes that map to the mass-over-energy ratio that labels the experimental domain (interference versus detection).
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No lemmas, no tactics, no proof obligations.
why it matters
Gives the module a named cost on the (mass, energy) domain so later lemmas can state non-negativity, the equality case, and the canonical threshold that separates wave-like from particle-like regimes. That threshold and the WPDuality3Cert certificate sit on top of this definition; the module status is a structural theorem (0 sorry, 0 axiom) that complementarity is exactly the continuous J-cost path between the J=0 and J=1 limits. Ties directly to T5 J-uniqueness and the RCL that forces J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.