domainCost_nonneg
plain-language theorem explainer
For positive reals m and e, the domain cost of the pair is nonnegative. Structural arguments that treat mass/energy ratios as J-costs cite this bound before comparing to thresholds. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive ratio m/e.
Claim. Let $m,e\in\mathbb{R}$ with $m>0$ and $e>0$. Then the domain cost of $(m,e)$ is nonnegative: $0\le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
Module RS_FDN_Structural_008 records structural facts about Recognition Science rung spacing: adjacent rungs differ by the golden ratio $\varphi\approx 1.618$. Status is a structural theorem block (zero sorry, zero axiom).
The domain cost of a positive pair $(m,e)$ is the J-cost of their ratio. The J-cost is the unique nonnegative cost forced by the Recognition Composition Law and T5 uniqueness: $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $\cosh(\log x)-1$. Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved via the squared form $(x-1)^2/(2x)$ (AM-GM / positivity).
proof idea
One-line wrapper. Unfold domainCost to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg to that positive ratio.
why it matters
Nonnegativity is the first structural property needed before any comparison of domain cost to a canonical threshold (sibling canonicalThreshold_pos and the module certificate RSFDNStructural008Cert). In the forcing chain this rests on T5 J-uniqueness: the same $J$ that solves the RCL is the cost used on mass/energy ratios along the $\varphi$-ladder. No downstream theorems are wired yet (used_by is empty); the lemma exists to discharge the nonnegativity obligation inside the structural-008 certificate rather than to feed a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.