domainCost
plain-language theorem explainer
Domain cost evaluates the RS recognition cost on the dimensionless ratio of a mass parameter to an energy scale. QFT and mass-ladder arguments cite it whenever a sector needs a ratio-symmetric cost rather than a raw scale. The body is a one-line abbreviation of Jcost at m/e.
Claim. For real parameters $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures mismatch by the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$ on positive ratios. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (T5), and that $J(x)\ge 0$ with equality only at $x=1$.
This module (QFT RS Structural 7) isolates the ratio symmetry $J(x)=J(1/x)$: recognition cost depends only on the relative scale, not on which quantity is numerator. Domain cost packages that idea for a mass-versus-energy pair by feeding the single ratio $m/e$ into $J$.
No extra structure is assumed here; $m$ and $e$ are plain reals, and positivity or nondegeneracy is left to sibling lemmas.
proof idea
Pure definition: expand as the existing J-cost applied to the quotient $m/e$. No tactics, no lemmas, no hypotheses.
why it matters
Gives the QFT layer a named handle for ratio-symmetric recognition cost on mass/energy pairs, matching the module thesis that recognition cost is ratio-symmetric. Siblings such as nonnegativity and evaluation-at-equality lemmas build directly on this abbreviation; the structural certificate in the same file packages those facts.
In the forcing chain this sits under T5 (J-uniqueness) and the RCL identity that forces $J$. It does not itself force $\phi$, the eight-tick period, or $D=3$, but it is the local cost primitive those later QFT bridges expect when comparing mass and energy scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.