domainCost
plain-language theorem explainer
The domain cost of a pair of real scales is the recognition cost of their ratio. Anyone deriving the 3D Anderson localization threshold in RS units cites this as the disorder-to-bandwidth cost functional. It is a one-line definition: apply J to m/e.
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
The module treats the 3D Anderson localization-delocalization transition as a structural consequence of the RS J-cost: critical disorder sits at $W_c \sim J(\varphi)^{-1}$ times the bandwidth energy scale.
Upstream, $J$ is the unique cost forced by the Recognition Composition Law, $J(x)=\frac12(x+x^{-1})-1$ (T5 J-uniqueness). Several modules re-export the same definition; Cosmology.RefineTrigger states it as "the RS recognition cost of a positive ratio," and EnergyProcessingBridge notes it is forced by RCL.
Domain cost simply specializes that functional to a mass-or-disorder scale over an energy-or-bandwidth scale, the ratio that later thresholds compare against $J(\varphi)$.
proof idea
Pure definitional abbreviation with no proof body: domainCost m e is defined to be Jcost (m / e). No lemmas are applied; the equality is definitional.
why it matters
This is the local cost primitive for the Anderson-from-J-cost development. Sibling facts (domainCost_at_eq, domainCost_nonneg) and the certificate stack (canonicalThreshold, AndersonLoc4Cert, cert) sit on top of it. The module status line frames the whole file as a structural theorem (0 sorry, 0 axiom) identifying the 3D Anderson transition with $W = J(\varphi)^{-1}$ times bandwidth. Without a named domain cost, that identification has no RS-native expression. Landmark tie-in: T5 forces $J$, T6 forces $\varphi$, and the threshold is built from both.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.