domainCost
plain-language theorem explainer
The domain cost of a mass-to-energy ratio is the J-cost of that ratio: J(m/e) = (m/e + e/m)/2 − 1. Structural Physics certificate 46 uses this as the scalar cost assigned to a physics-domain pair (m, e). The definition is a one-line specialization of the forced recognition cost functional to the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $\mathrm{domainCost}(m,e) := J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the recognition cost of a positive ratio.
background
Recognition Science forces a unique nonnegative cost on positive ratios via the Recognition Composition Law. That cost is $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$), fixed at forcing step T5. It vanishes only at $x = 1$ and is strictly positive for any genuine distinction.
This module is Structural Certificate 46 for the Physics domain (Plan v7, 120th pass): a structural RS prediction at recognition rung 46, with zero sorry and zero axiom. The certificate needs a scalar cost on pairs of real parameters that can stand for mass-like and energy-like scales.
Upstream, every copy of Jcost in Cost, Cosmology, Gravity, and Spiral is the same functional: "the unique cost functional forced by the Recognition Composition Law" and "the RS recognition cost of a positive ratio." Domain cost simply feeds the ratio $m/e$ into that functional.
proof idea
Pure definitional abbreviation: expand domainCost m e to Jcost (m / e). No lemmas, tactics, or side conditions are involved at the definition site. Nonnegativity and evaluation identities appear in sibling lemmas (domainCost_nonneg, domainCost_at_eq), not here.
why it matters
Certificate 46 needs a named Physics-domain cost before it can state thresholds and inhabit the structural certificate (canonicalThreshold, StructPhysicsM46Cert, cert_inhabited). Domain cost is that scalar: it measures how far the mass-to-energy ratio sits from unity under the forced J-cost.
In the broader framework this is the local instance of T5 J-uniqueness applied to a physics ratio, not a new cost law. It keeps the Physics rung-46 certificate aligned with the same $J$ used in gravity bridges, coherence collapse, and spiral fields. No downstream theorems currently depend on it in the graph; its role is internal scaffolding for the mod-46 certificate bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.