domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e) with the standard RS J-cost. Physicists working the proton-electron mass-ratio module cite it as the local cost functional on (m,e). The body is a one-line definition wrapping Jcost.
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 cost of a positive ratio.
background
Physics RS Module 9 treats the proton-electron mass ratio structurally. The module notes that $\phi^{12}\approx 321.9$ sits a factor $\sim 5.7$ below the observed $\approx 1836$, so a correction gap remains; the status is a structural theorem with no sorry and no axioms.
The underlying cost is the RS J-functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced uniquely at T5 of the forcing chain and obeying the Recognition Composition Law. Upstream definitions state that $J$ is the recognition cost of a positive ratio, that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is non-negative for positive $x$.
Domain cost simply specializes that functional to a mass-energy pair by feeding the ratio $m/e$ into $J$.
proof idea
Pure definition: the body is the term $J(m/e)$ with no proof obligations. It reuses the shared noncomputable $Jcost$ from Cost (and identical aliases in Cosmology and Gravity). Sibling lemmas such as evaluation-at-equality and non-negativity are proved separately from this def.
why it matters
Gives the module a named cost on mass-energy pairs so later certificates (canonical threshold positivity, the RSPhysics009Cert bundle) can talk about when a ratio is costly enough to count as a domain distinction. It sits inside the proton-electron mass-ratio story: $\phi^{12}$ is the bare ladder prediction, and domain cost is the natural J-measure of how far a candidate $(m,e)$ sits from unity. No downstream uses are wired yet in the graph; the def is scaffolding for those certs rather than a forcing-chain step itself. Landmarks in play are T5 J-uniqueness and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.