domainCost
plain-language theorem explainer
The domain cost of a mass–energy pair is the recognition cost of their ratio: J(m/e). Summary and certificate modules cite it as the scalar that measures how far a domain sits from balance. The body is a one-line abbreviation 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)=(x+x^{-1})/2-1$ is the recognition cost of a positive ratio.
background
Recognition Science is built on a single cost functional $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, EnergyProcessingBridge, CoherenceCollapse, RefineTrigger) all define the same $J$: the unique nonnegative functional forced by the Recognition Composition Law, vanishing only at ratio one.
This module is the Plan-v7 structural summary certificate: zero sorry, zero axiom. It packages the forcing chain (J uniqueness, $\phi$ fixed point, eight-tick octave, $D=3$) and derived constants into a single certifiable interface. Domain cost is the local scalar that scores a mass–energy pair by feeding their ratio into $J$.
Sibling lemmas immediately specialise the definition: evaluation at equality, nonnegativity for positive arguments, and comparison against a canonical threshold.
proof idea
Pure definitional abbreviation. The body is Jcost (m / e) with no tactics or lemmas; all analytic content lives in the shared Jcost definition and its upstream uniqueness and nonnegativity theorems.
why it matters
In the RS summary layer this is the working scalar for “how expensive is this domain.” It sits under the complete summary certificate (RSSummary3Cert / cert) that asserts the structural theorem package: one equation $J$ forced by four axioms, implying $\phi$, gap-45, $D=3$, and the derived constants. Framework landmarks: T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. No downstream theorem edges are recorded yet; the definition exists so certificate and threshold lemmas can quote a single name rather than inline $J(m/e)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.