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 Module 8 phi-uniqueness forcing material and by anyone comparing mass and energy scales on the RS ladder. The declaration is a one-line abbreviation of the standard J-cost at m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Module 8 of the foundation chain records the structural theorem that $\varphi=(1+\sqrt{5})/2$ is the unique fixed point of recognition recursion (zero sorry, zero axiom). The ambient cost is the RS J-functional fixed at T5: $J(x)=\frac{1}{2}(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream docs state it as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost, with non-negativity for positive $x$.
Domain cost simply specializes that functional to the ratio of two real scales $m$ and $e$ (mass versus energy, or any comparable pair in the forcing setup). Sibling lemmas in the same file then record evaluation identities and non-negativity for this specialization.
proof idea
Definitional abbreviation only: domainCost m e is set equal to Jcost (m / e). There is no tactic proof and no lemma application; the body is the single application of the imported J-cost to the quotient.
why it matters
Gives the Module 8 forcing material a named cost on scale pairs so that threshold and certificate lemmas (canonical threshold positivity, the RSForcingChain008 cert) can speak about cost without reopening the J definition. It sits under T5 J-uniqueness in the forcing chain and under the Recognition Composition Law background, even though this file does not re-prove those facts. No downstream used_by edges are recorded yet; the immediate consumers are the sibling facts domainCost_at_eq and domainCost_nonneg inside the same structural certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.