domainCost
plain-language theorem explainer
Domain cost assigns to a mass scale m and energy scale e the recognition cost of their ratio m/e. It is the local shorthand used throughout the Weinberg-angle physics module whenever a mass-energy mismatch must be scored. The body is a one-line alias of the standard J-cost functional.
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
Recognition Science scores any positive ratio $x$ by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream definitions in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse all fix this same functional; a genuine distinction ($x\neq 1$) has strictly positive cost, and $J$ is nonnegative on positives.
Physics RS Module 4 treats the tree-level Weinberg angle $\sin^2\theta_W=J(\phi)/(1+J(\phi))\approx 0.1054$, later loop-corrected toward $0.231$. Domain cost is the module's working name for applying $J$ to a mass-over-energy ratio, the natural dimensionless input when comparing particle or interaction scales inside that derivation.
proof idea
Pure definitional abbreviation: the body is exactly Jcost (m / e). No tactics, no lemmas, no side conditions are discharged at this declaration.
why it matters
Gives the module a single named map from mass-energy pairs into the J-cost that already forces $\phi$, the eight-tick octave, and $D=3$ in the T5-T8 chain. Sibling lemmas (domainCost_at_eq, domainCost_nonneg) and the certificate RSPhysics004Cert sit on top of this alias, so every later threshold comparison in the Weinberg-angle development is phrased uniformly. No downstream users are recorded yet outside the module siblings; the definition is local scaffolding for that structural theorem (0 sorry, 0 axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.