domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the Recognition J-cost of their ratio m/e. Materials work on the Mott U/t match (Module 10) uses this as the local cost of a mass-to-energy or interaction-to-hopping ratio. The body is a one-line definitional wrapper around the unique RS cost functional J.
Claim. For real numbers $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
Materials RS Module 10 treats the Mott transition ratio U/t, claiming a structural match to $\varphi^3\approx 4.24$ inside the empirical window 3–5, with status STRUCTURAL THEOREM (0 sorry, 0 axiom).
The cost functional is the standard RS J-cost $J(x)=\frac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law (T5 / RCL). Upstream docs phrase it as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; non-negativity for $x>0$ is the companion fact used by siblings.
Here $m$ and $e$ are generic positive scale parameters (mass vs energy, or Hubbard $U$ vs hopping $t$). Domain cost simply evaluates $J$ on their ratio, so the materials layer speaks the same cost language as cosmology, gravity, and spiral modules.
proof idea
Definitional one-liner: domainCost m e is exactly Jcost (m / e). No tactics, no lemmas, no hypotheses. All analytic content (non-negativity, equality cases, thresholds) lives in sibling declarations such as domainCost_nonneg and canonicalThreshold.
why it matters
Gives the materials stack a named cost on scale ratios so Mott U/t can be compared to the forced golden ratio ladder rather than an ad-hoc number. Module 10's structural claim is that the Mott window centers on $\varphi^3$, which is the natural cubic self-similar scale once $\varphi$ is fixed by T6. Downstream certificate objects in the same file (RSMatl010Cert, cert) package the match; this def is the cost primitive those certificates evaluate. It ties materials phenomenology to the same J forced by RCL and used across cosmology and gravity bridges, keeping the cost language uniform.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.