domainCost
plain-language theorem explainer
The domain cost of a pair of real parameters is the recognition cost of their ratio. Anyone working the Gap-45 exact certificate cites this as the local cost on a mass-to-energy (or scale-to-scale) ratio. The body is a one-line abbreviation of the forced J-functional at m/e.
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 Gap45_Exact_v2 records the structural identity gap-45 = 45 = D^2(D+2) = 9·5 forced by D = 3, together with the classical and cultural 45-degree / 45-count coincidences that sit on that integer. Status is a structural theorem with no sorry and no axioms.
The recognition cost J is the unique nonnegative functional forced by the Recognition Composition Law: J(x) = (x + x^{-1})/2 - 1 (equivalently cosh(log x) - 1). Upstream modules (Cost, CoherenceCollapse, EnergyProcessingBridge, RefineTrigger, SpiralField) all expose the same Jcost on positive reals; a genuine distinction (ratio ≠ 1) has strictly positive cost.
Here the two arguments are treated as a single ratio m/e before J is applied, so domainCost is the cost of that scale mismatch rather than a bivariate primitive.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No lemmas, no tactics, no proof obligations.
why it matters
Gap-45 is the integer D^2(D+2) forced once spatial dimension is fixed at D = 3 (forcing-chain step T8). The module packages that identity as a structural certificate. domainCost supplies the local cost reading of a mass-to-energy (or analogous scale) ratio inside that certificate stack; sibling lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold, Gap45ExactV2Cert) sit on top of it. It does not itself prove the 45-count; it is the cost primitive those later statements evaluate. Framework landmarks in play: T5 J-uniqueness and the RCL that force J, and T8 D = 3 that forces the integer 45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.