domainCost_nonneg
plain-language theorem explainer
The domain cost of two positive reals (mass and energy parameters) is nonnegative. Citation target for anyone assembling the J-cost error-correction certificate in this module. Proof is a one-line unfold of domainCost to J-cost of the ratio, then the standard AM-GM nonnegativity lemma.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative. Equivalently, if domain cost is the Recognition cost $J$ of the ratio $m/e$, then $0\leq J(m/e)$.
background
Recognition cost is $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), forced unique by the Recognition Composition Law (forcing-chain T5). Upstream lemma: $J(x)\geq 0$ for every $x>0$, proved by rewriting as a square over a positive denominator (AM-GM).
This module treats error-correction capacity as a structural consequence of that cost. Module status is structural theorem (zero sorry, zero axiom). At the RS rate $R=J(\phi)\approx 0.118$ the Hamming bound supports error fraction $t/n=J(\phi)/2\approx 0.059$.
Domain cost packages $J$ on the positive ratio of two scale parameters $m$ and $e$ (mass-like over energy-like), the natural dimensionless argument for the information-domain certificate built later in the file.
proof idea
One-line wrapper. Unfold domainCost (definitionally $J(m/e)$), obtain positivity of the quotient by div_pos on the two hypotheses $m>0$ and $e>0$, then apply the upstream lemma Jcost_nonneg.
why it matters
Supplies the elementary positivity fact required by the local error-correction certificate (ErrCorr3DeepCert, cert, cert_inhabited) and by sibling facts such as positivity of the canonical threshold. Ties the forced J-cost (T5) to coding capacity at the golden-ratio rate inside the Information domain. No recorded downstream users outside the module; the lemma is internal structural glue rather than a global forcing-chain step. Closes a trivial but necessary nonnegativity obligation so the certificate can stay axiom-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.