domainCost
plain-language theorem explainer
Defines the domain cost of a mass–energy pair as the recognition cost of their ratio: J(m/e). Anyone working the Logo5 structural package or threshold comparisons cites it as the basic scalar. The body is a one-line abbreviation of the unique J-cost on the positive reals.
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 takes a single cost on positive ratios, $J(x)=(x+x^{-1})/2-1$, forced by the Recognition Composition Law and unique up to the T5 step of the forcing chain. $J$ vanishes only at $x=1$, is nonnegative for $x>0$, and equals $J(\varphi)$ at the golden ratio fixed point.
The Logo5 module treats this curve as the structural logo of the framework: one plot on $(0,\infty)$ that encodes the whole theory. Domain cost simply specializes $J$ to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass scale $m$ to an energy scale $e$.
Upstream, every module that imports cost uses the same Jcost definition; the Cosmology, Gravity, and Spiral copies are identical aliases of that functional.
proof idea
Pure definitional abbreviation: apply the shared $J$-cost to the quotient $m/e$. No lemmas, no tactics, no side conditions in the body itself. Nonnegativity and evaluation identities appear in sibling lemmas, not here.
why it matters
Logo5 packages the claim that the single curve $J$ is the entire structural content of Recognition Science. Domain cost is the first named specialization in that package: it turns an abstract ratio cost into a mass–energy observable used by the certificate and the canonical threshold siblings.
It sits on the T5 landmark (uniqueness of $J$) and feeds the Logo5 certificate chain (RSLogo5Cert, cert, cert_inhabited). Downstream use count is currently empty in the graph, so its role is local scaffolding for the threshold and nonnegativity facts rather than a widely imported lemma.
No open forcing-chain gap is closed here; the definition merely names the ratio cost that those later facts quantify.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.