domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition J-cost of their ratio. Collapse-threshold work in the wavefunction module uses it as the elementary cost of a mass-to-energy mismatch. The body is a one-line application of the standard J functional to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module develops a structural account of objective (GRW-style) wavefunction collapse from Recognition Science cost, with status zero sorry and zero axiom. The stated objective is a collapse rate built from J at phi, nucleon mass, and a phi-power denominator; the numerical check is flagged as off by many orders and kept as structural only.
The upstream cost is the standard RS recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ on positive ratios (also written $\cosh(\log x)-1$). Sibling material in Cosmology, Cost, and Gravity packages all use this same functional: genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positive arguments.
Here the two arguments are read as a mass-like scale $m$ and an energy-like scale $e$. Domain cost packages the single ratio $m/e$ as the cost input for later threshold and certificate definitions in the same file.
proof idea
Pure definition: apply the imported J-cost functional to the quotient $m/e$. No lemmas, tactics, or side conditions appear in the body.
why it matters
This is the local cost primitive for the Plan v7 wavefunction-collapse pass. Sibling lemmas (evaluation at equality, nonnegativity) and the canonical threshold / WFCollapse3 certificate stack sit on top of it. In the broader RS chain it is the same T5 J uniqueness functional used for recognition cost, specialized to a mass-energy ratio rather than a free positive scale.
The module objective ties collapse rate to $J(\phi)$ over nucleon mass times a high phi power. Domain cost is the intermediate that lets those arguments speak in ratio language. No used-by edges are recorded yet; the declaration is infrastructure for the in-module certificate rather than a finished physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.