domainCost
plain-language theorem explainer
The domain cost of a mass scale m relative to an energy reference e is the recognition cost J(m/e). Anyone working the RS SUSY-breaking ladder (M_SUSY versus M_Z) cites this as the scalar that measures how far the ratio sits from unity. It is a one-line definition wrapping the unique J-cost functional.
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
Recognition Science measures mismatch of positive scales by the J-cost $J(x) = \frac12(x + x^{-1}) - 1$. Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all fix the same formula; EnergyProcessingBridge records that it is the unique functional forced by the Recognition Composition Law. $J(x) \ge 0$ for $x > 0$, with equality only at $x = 1$.
This module treats MSSM/SUSY breaking in RS units. The structural claim is that the SUSY scale sits near $M_{\mathrm{SUSY}} \sim \varphi^{10} M_Z \sim 11,\mathrm{TeV}$ (empirically $M_{\mathrm{SUSY}}/M_Z \approx 110 \approx \varphi^{10.7}$). Domain cost is the scalar that scores any candidate mass-to-energy ratio before thresholds and certificates are applied.
proof idea
Pure definitional abbreviation: apply the shared J-cost to the ratio $m/e$. No lemmas, no tactics, no hypotheses.
why it matters
Gives the local cost primitive for the MSSM-breaking certificate stack in this module (siblings include non-negativity, evaluation at equality, and the canonical threshold). In the forcing chain, J is the T5 unique cost; here it scores how far a SUSY scale sits from the electroweak reference on the phi-ladder. The module status is structural (0 sorry, 0 axiom), so this def is the entry point for all later positivity and threshold facts about $M_{\mathrm{SUSY}}/M_Z$. No downstream used_by edges are recorded yet; the immediate consumers are the in-module lemmas that bound or specialize it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.