domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost J to the dimensionless ratio of a mass scale m to an energy scale e. Anyone working the QCD running-coupling certificate in RS Physics Module 1 cites it as the local cost functional on mass/energy ratios. The body is a one-line abbreviation of the standard J-cost.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost of a positive ratio.
background
Recognition Science measures mismatch of positive ratios by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all expose the same noncomputable definition: the cost of a genuine distinction (ratio not one) is strictly positive for $x>0$.
This file is Physics RS Module 1. Its structural claim is that the QCD running coupling at the Z pole equals $J(\varphi)=0.11803$, matching the PDG value $0.1180$ to the reported digits, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
Domain cost simply specializes J to the ratio of a mass parameter to an energy scale, the natural dimensionless argument when comparing particle masses to a renormalization point.
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No lemmas, tactics, or side conditions appear in the body.
why it matters
The definition supplies the local cost functional used by the module's companion lemmas (domainCost_at_eq, domainCost_nonneg) and by the certificate bundle RSPhysics001Cert. In the forcing chain, J is the unique cost fixed at T5; here it is applied to mass/energy ratios that feed the QCD $\alpha_s(M_Z)=J(\varphi)$ identification. No downstream theorems currently depend on it outside this module, so it is scaffolding for the module-local certificate rather than a global bridge lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.