domainCost
plain-language theorem explainer
Domain cost assigns to a real pair (m, e) the recognition cost of their ratio m/e. It is the local cost functional used in the structural proton-radius development that ties charge radius to the phi-ladder and J. Anyone citing the nonnegativity or threshold lemmas in this module will use it. The body is a one-line abbreviation of J on the quotient.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x) = \frac{x + x^{-1}}{2} - 1$ (for $x \neq 0$).
background
The module develops a structural account of the proton charge radius from the phi-ladder and the J-cost, marked as a structural theorem with no sorry and no axioms. The experimental target is $r_p \approx 0.841,\mathrm{fm}$; the text contrasts naive ladder scalings against a structural reading rather than a fitted numerical claim.
The recognition cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law: $J(x) = \frac{1}{2}(x + x^{-1}) - 1$. Upstream copies state the same formula and that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply specializes $J$ to a mass-scale ratio $m/e$, the natural input for threshold and certificate lemmas later in the file.
proof idea
Pure definition: no proof obligations. The right-hand side is the standard $J$-cost applied to the single ratio $m/e$. Downstream facts (equality at equal arguments, nonnegativity) inherit directly from the corresponding properties of $J$.
why it matters
This is the cost primitive for the proton-radius-from-J session. Sibling results (value at equal arguments, nonnegativity, the canonical threshold and its positivity, and the ProtonRadius3 certificate) all read domain cost as the measure of mismatch between the two scales. In the broader framework it sits under T5 J-uniqueness: once $J$ is forced, every structural radius or mass comparison is a $J$-evaluation on a phi-ladder ratio. The module status note frames the work as structural rather than a closed numerical derivation of $0.841,\mathrm{fm}$, so the definition keeps the cost interface explicit while the certificate layer packages the claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.