domainCost
plain-language theorem explainer
Defines the recognition cost of a mass-to-energy ratio as the J-cost of m/e. Structural Physics certificates at rung 96 use this as the domain-level cost functional. The body is a one-line abbreviation of the unique RS cost J.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the Recognition Science cost of a positive ratio.
background
Recognition Science forces a unique nonnegative cost on positive ratios: $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules record the same functional (Cost, Cosmology.RefineTrigger, Gravity bridges, SpiralField) and note that it is the unique solution of the Recognition Composition Law (RCL).
This module is the structural Physics certificate at recognition rung 96 (Plan v7, 120th pass): zero sorry, zero axiom. Domain-level quantities are scored by feeding a mass-to-energy ratio into $J$, so the cost vanishes only when $m=e$ (ratio one) and is strictly positive for any genuine distinction.
Sibling lemmas in the same file establish nonnegativity and evaluation identities for this cost, and feed a canonical threshold used by the structural certificate.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No proof obligations; the mathematical content is inherited from the forced uniqueness of $J$ (T5 / RCL).
why it matters
Gives the Physics-domain cost used by the structural certificate at rung 96. In the RS forcing chain, $J$ is the unique cost (T5); applying it to $m/e$ is the natural domain score for mass-energy mismatch. Downstream siblings (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, StructPhysicsM96Cert) build the certificate around this definition. No external used_by edges yet; the local certificate is the consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.