domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio: J(m/e). Gravity and BH-entropy arguments in this module use it as the local cost of a mass scale relative to an energy scale. The definition is a one-line specialization of the unique J-cost forced by the Recognition Composition Law.
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 derives the black-hole entropy logarithmic correction coefficient from the RS J-cost, targeting $c_{\mathrm{RS}}=-\log\phi/2\approx-0.2406$, which matches Sen’s 2013 Kerr–Newman 4D result exactly and Falls–Litim asymptotic safety (~−0.241).
Upstream, $J$ is the unique cost functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ for $x>0$. It vanishes only at ratio one and is nonnegative on positives. Domain cost simply evaluates that functional on the dimensionless ratio of a mass parameter to an energy parameter, so the same J-geometry used in coherence collapse and energy-processing bridges applies to BH entropy bookkeeping.
proof idea
Pure definition: no proof obligations. The body is the term $J(m/e)$, i.e. a direct application of the shared $J$-cost functional to the ratio of the two real arguments.
why it matters
Gives the module a named mass–energy cost so later certificates (canonical threshold, nonnegativity, and the BH entropy log-2 certificate) can speak in gravity language rather than raw $J$. It sits on the T5 J-uniqueness landmark: once $J$ is forced, every domain-specific cost is just $J$ of the relevant ratio. Downstream siblings in this file use it to pin the log-correction coefficient against Sen and Falls–Litim; used_by is empty at present, so it is infrastructure for those local theorems rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.