domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the J-cost of m/e. Anyone working the T0–T8 forcing completeness chain cites this as the local cost functional on positive reals. The body is a one-line abbreviation of the standard recognition cost J.
Claim. For real numbers $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 completes the T0–T8 forcing chain: all physical constants derived from the unique J-cost. Status is structural (zero sorry, zero axiom). Landmarks include J-uniqueness, the Recognition Composition Law, phi as self-similar fixed point, the eight-tick octave, and D = 3.
The recognition cost is $J(x) = (x + x^{-1})/2 - 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; J is nonnegative on positive reals.
Here the cost is specialized to a mass-energy ratio $m/e$, giving a domain-level scalar used by sibling lemmas on nonnegativity and evaluation at equality.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is exactly $J(m/e)$. No tactics, no lemmas. Downstream facts (nonnegativity, value at $m=e$) unfold this one line and apply the corresponding properties of $J$.
why it matters
Gives the forcing-completeness module a named cost on mass-energy pairs so later certificates can speak about thresholds without repeating the J formula. Siblings include nonnegativity of domain cost, the value at equal arguments, and a canonical positive threshold; the module certificate ForcingChainComp3Cert packages the structural claim that T0–T8 close from J alone.
In the primer chain this sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. It does not itself force phi, the eight-tick, or D=3; it only supplies the cost primitive those steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.