domainCost
plain-language theorem explainer
Domain cost scores a mass against an energy scale by the recognition cost of their ratio. Anyone working the φ-ladder compactification radius or string-length certificates cites it as the local cost functional. The body is a one-line abbreviation of J applied to m/e.
Claim. For real $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
The module fixes extra-dimension compactification on the φ-ladder: $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}},\varphi^{-k}$. Planck-scale compactification is $k=0$; electroweak scale needs roughly $k\approx 106$ rungs. Status is structural (no sorry, no axioms).
The underlying cost is the RS J-functional $J(x)=\frac12(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream docs call it "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is non-negative for positive $x$. Domain cost simply specializes that functional to a mass-over-energy ratio.
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into the existing noncomputable $J$-cost. No lemmas, no tactics.
why it matters
Supplies the local cost used by the string-length certificate machinery in the same module (siblings such as non-negativity, the equality-at-equality lemma, and the inhabited certificate). In the broader RS chain it is the T5 J-cost specialized to a mass/energy domain, so compactification radii measured in φ-rungs can be scored by recognition cost rather than by an ad-hoc length functional. No downstream edges are recorded yet; the definition is infrastructure for the structural theorem that $R_{\mathrm{comp}}$ sits on the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.