domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the RS J-cost of that ratio: J(m/e) = (m/e + e/m)/2 - 1. Used in the electron-spin-from-config-dimension development to score how far a candidate (m,e) pair sits from the unit ratio. Pure abbreviation of the standard recognition cost on 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
The module derives the electron spin quantum number $s = 1/2$ from configuration dimension: spin emerges as $s = 1/D$ with $D = 2$ for the spinor representation (Clifford algebra in two dimensions for SU(2)), equivalently $s = 1/2^1$ on the binary recognition lattice.
The unique cost forced by the Recognition Composition Law is $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (also written $\cosh(\log x) - 1$). Upstream docs state it is the RS recognition cost of a positive ratio, nonnegative for $x > 0$, and strictly positive when the ratio is not one. Domain cost simply evaluates that functional on the mass-to-energy quotient $m/e$.
proof idea
One-line definitional wrapper: apply the standard J-cost to the ratio $m/e$. No lemmas, no tactics; the body is exactly Jcost (m / e).
why it matters
Supplies the local cost functional for the electron-spin-from-config-dimension certificate chain (siblings include nonnegativity, evaluation identities, a canonical threshold, and SpinQuantumNumCert). In the broader RS forcing picture this is the T5 J-cost specialized to a mass/energy domain ratio, so later spin and threshold arguments can quote a single named quantity rather than inlining $J(m/e)$ everywhere. No downstream users are recorded yet; the def is infrastructure for the structural $s = 1/2$ theorem in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.