domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass-energy pair is nonnegative. Researchers comparing recognition costs on mass-to-energy ratios inside the forcing chain would cite this. The argument is a one-line unfold that reduces to nonnegativity of the J-cost on the positive ratio m/e.
Claim. If $m>0$ and $e>0$ are real, then the domain cost of the pair is nonnegative: $0\le J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost functional.
background
Foundation Module 8 records structural theorems on RS phi uniqueness: $\varphi=(1+\sqrt{5})/2$ is the unique fixed point of the recognition recursion. The module is marked fully proved (zero sorry, zero axioms).
The recognition cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). By AM-GM it is nonnegative for every positive real argument. Domain cost of a positive mass $m$ and energy scale $e$ is exactly this $J$ evaluated at the ratio $m/e$.
Upstream, the Cost library lemma states: "$J(x)\ge 0$ for positive $x$ (AM-GM inequality)". A parallel statement appears in the CoherenceCollapse development.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J$ at $m/e$), then apply Jcost_nonneg to the positive ratio produced by div_pos from the two positivity hypotheses.
why it matters
Lives in Foundation Module 8 of the RS forcing chain, whose theme is uniqueness of $\varphi$ as the self-similar fixed point (landmark T6). Nonnegativity of domain cost is the basic positivity fact needed before any cost comparison or threshold (the sibling canonical-threshold lemmas) can be formed from mass-energy data. No downstream dependents are recorded in the graph yet; the lemma discharges a local positivity obligation inside the module certificate. It does not itself advance the T0-T8 forcing steps beyond supplying a sign constraint on the cost used throughout the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.