domainCost
plain-language theorem explainer
Domain cost of a mass scale m against an energy scale e is the recognition cost of their ratio. Cosmologists deriving RS cosmic-string tension bounds use it as the elementary cost of a domain or string scale ratio. It is a one-line definition applying the unique J-cost to m/e.
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
The module builds a cosmic-string network bound from Recognition Science J-cost. Status is structural (0 sorry, 0 axiom). The target comparison is string tension $G\mu$, with the RS form $G\mu=J(\varphi),(E_{\mathrm{string}}/M_{\mathrm{Pl}})^2$ checked against the observational ceiling $G\mu<10^{-7}$.
Upstream, $J$ is the unique cost forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$. It vanishes only at ratio one and is strictly positive for any genuine distinction. Several modules re-export the same functional under the name J-cost.
Domain cost simply specializes that functional to the dimensionless ratio of a mass parameter to an energy scale, the natural argument for domain-wall or string-scale comparisons in this cosmology file.
proof idea
One-line definition: apply the J-cost functional to the ratio $m/e$. No lemmas, no tactics, no proof obligations.
why it matters
Supplies the cost ingredient for the cosmic-string certification path in this module (siblings include non-negativity of domain cost, the canonical threshold, and the CosmicStrings4 certificate). The module doc pins the numerical claim: $G\mu=J(\varphi),(v/M_{\mathrm{Pl}})^2$, with $J(\varphi)\approx0.118$, so at $v=10^{16},\mathrm{GeV}$ one gets $G\mu\sim8\times10^{-6}$, marginally excluded and consistent with present limits.
Framework landmark: T5 J-uniqueness. String tension is controlled by the forced cost $J$, not a free parameter. No downstream edges are recorded yet; the definition is local scaffolding for the certificate in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.