domainCost
plain-language theorem explainer
The domain cost of a mass m relative to an energy scale e is the recognition cost J(m/e). Anyone working the Higgs-mass match in RS Module 10 cites this as the local cost functional on the mass-to-energy ratio. It is a one-line definition that applies the standard J-cost to the quotient.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the recognition cost of a positive ratio.
background
Recognition Science measures mismatch of positive ratios by the J-cost $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. This is the unique cost forced by the Recognition Composition Law (forcing chain T5). It vanishes only at $x = 1$ and is nonnegative for $x > 0$.
Physics RS Module 10 treats the Higgs mass match $m_H \approx 125.25,\mathrm{GeV}$ against a $\varphi$-ladder scale (structurally $\varphi^{13}$ yields the observed value after the stated prefactor). The module is marked structural: zero sorry, zero axiom.
Upstream, Jcost is defined identically in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse as the RS recognition cost of a positive ratio.
proof idea
Pure definition: domain cost is the term $J(m/e)$. No proof obligations; the body is the single application of the upstream J-cost functional to the mass-over-energy ratio.
why it matters
Gives Module 10 a named cost on the mass-to-energy ratio used when comparing the Higgs mass to the $\varphi$-ladder yardstick. Sibling lemmas (nonnegativity, evaluation identities, canonical threshold positivity) and the module certificate RSPhysics010Cert sit on top of this abbreviation. It ties the local Higgs match to the global J-uniqueness landmark (T5) without introducing a new functional form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.