domainCost
plain-language theorem explainer
Domain cost assigns to a mass-energy pair the recognition cost of their ratio. Module-7 top-Yukawa work cites it as the cost on m/e when the top coupling sits at the phi^0 = 1 fixed point. It is a one-line definition wrapping the standard J-cost.
Claim. For real $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
Physics RS Module 7 is the structural package for the top Yukawa: $y_t=1$ at unification, with the top quark as the $\phi^0=1$ coupling. Status is a structural theorem (zero sorry, zero axiom).
The underlying cost is the RS J-functional $J(x)=\frac12(x+x^{-1})-1$, the unique recognition cost of a positive ratio (forcing-chain T5). Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all expose the same $J$: a genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positive reals.
Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when comparing a particle mass scale to an energy scale in the module.
proof idea
Pure definitional wrapper. The body is the single term $J(m/e)$; there is no tactic proof and no lemma application beyond the imported $J$-cost abbreviation.
why it matters
Gives Module 7 a named cost on mass/energy pairs so later lemmas (nonnegativity, evaluation at equality, canonical threshold) can speak uniformly. Downstream siblings in the same file build the certificate RSPhysics007Cert around this cost and the top-Yukawa structural claim $y_t=1$.
In the broader framework it sits on T5 J-uniqueness and the Recognition Composition Law: every dimensionless ratio is scored by the same $J$, here applied to $m/e$. The top coupling at $\phi^0=1$ is the zero-cost fixed point of that ladder; domain cost is the bookkeeping object that makes the cost of departures from that point explicit. No open scaffold: the declaration is closed definitional content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.