domainCost
plain-language theorem explainer
Domain cost assigns to a real pair (m, e) the recognition cost of their ratio m/e. It is the local cost functional used in the many-worlds module when comparing branch amplitudes against the phi threshold. Anyone citing the structural many-worlds claim (branches multiply only when J exceeds J(phi)) uses this as the cost of a domain. The body is a one-line specialization of the unique J-cost.
Claim. For real numbers $m$ and $e$, define the domain cost by $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The ambient module treats many-worlds branching as a recognition phenomenon: branches multiply when the J-cost of an amplitude exceeds $J(\varphi)$, while subthreshold branches remain recognition-undetectable. Only branches with $J\ge J(\varphi)$ count as macroscopically distinct.
The cost functional is the unique $J$ forced by the Recognition Composition Law (forcing chain T5): $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream definitions across Cost, CoherenceCollapse, and EnergyProcessingBridge all pin the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Here the arguments are a mass-like scale $m$ and an energy-like scale $e$; the domain cost is simply $J$ evaluated on their ratio. Sibling lemmas then record evaluation identities and nonnegativity for this specialization.
proof idea
Pure definitional abbreviation: apply the global $J$-cost to the ratio $m/e$. No lemmas, no tactics; the equality domainCost m e = Jcost (m/e) is definitional (rfl).
why it matters
This is the cost primitive for the structural many-worlds theorem in the module (status: 0 sorry, 0 axiom). The module thesis is that branching is gated by comparing $J$ of amplitudes to $J(\varphi)$; domain cost is the concrete $J(m/e)$ form of that comparison for mass/energy domain pairs.
It sits on the T5 uniqueness of $J$ and on the RCL-forced shape $J(x)=\frac12(x+x^{-1})-1$. Downstream siblings (domainCost_nonneg, canonicalThreshold, ManyWorlds3Cert) build the nonnegativity, the phi-threshold, and the certificate that only superthreshold branches are macroscopically distinct. Without this def, the many-worlds cost language has no local handle on $(m,e)$ pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.