domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Anyone working the phi-square identity module or threshold comparisons cites this as the local cost functional on positive reals. It is a one-line definitional wrapper around the standard J-cost.
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 proves the structural identity $\varphi^2 = \varphi + 1$ and records its Fibonacci-style consequences for the recognition recursion. Status is fully closed: zero sorry, zero axioms.
The underlying cost is the unique J-functional forced by the Recognition Composition Law: $J(x) = \frac{1}{2}(x + x^{-1}) - 1$. Upstream copies state the same formula and note that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Domain cost simply specializes that functional to a mass-over-energy ratio, giving a named cost on pairs $(m,e)$ used by the sibling lemmas in this file (nonnegativity, evaluation identities, canonical thresholds).
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is defined to be $J(m/e)$. No proof obligations; the body is the single application of the imported J-cost.
why it matters
Gives the local cost language for the phi-square identity development. Sibling results (nonnegativity of domain cost, evaluation at equality, canonical threshold positivity) build directly on this abbreviation. In the broader forcing chain, J is the T5 unique cost; specializing it to $m/e$ keeps mass-energy comparisons inside the same functional that later feeds ladder rungs, coherence collapse, and energy-processing bridges. No downstream external users are recorded yet; the definition is scaffolding for the in-module certificate PhiSqIdentCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.