domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Forcing-chain and cost-functional arguments cite this when lower-bounding recognition costs along the T0–T8 chain. Proof is a one-line unfold of the domain-cost definition, then the standard J-cost nonnegativity lemma on the ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$, i.e. $J(m/e)$ with $J(x)=(x+x^{-1})/2-1$.
background
Module ForcingChainCompleteness3 records structural completeness of the T0–T8 forcing chain: physical constants derived from the unique J-cost functional, with status “structural theorem (0 sorry, 0 axiom).” Local siblings package domain cost, a canonical threshold, and the completeness certificate.
The J-cost on positive reals is $J(x)=(x+x^{-1})/2-1$, equivalently $(x-1)^2/(2x)$. Upstream lemma Jcost_nonneg states “$J(x)\ge 0$ for positive $x$ (AM-GM inequality)” and is proved by rewriting to a square over a positive denominator. Domain cost is the specialization of that cost to a mass-to-energy ratio: unfolding yields $J(m/e)$ whenever $m,e>0$.
Positivity of the ratio follows from the ordered-field fact that the quotient of two positive reals is positive, so the AM-GM form of $J$ applies directly.
proof idea
One-line wrapper. Unfold the definition of domain cost (exposing J-cost of the ratio $m/e$). Discharge the goal by exact application of Jcost_nonneg to the hypothesis that $m/e>0$, obtained from div_pos on the two positivity assumptions. No further algebraic rewriting is required in this file; the work sits in the upstream nonnegativity lemma.
why it matters
Supplies the elementary positivity fact for domain cost inside the T0–T8 completeness package. The module aims at a full structural derivation of constants from J (T0 J-uniqueness through T8 Lambda), and nonnegativity of every cost specialization is prerequisite bookkeeping before thresholds and certificates. Sibling declarations include the domain-cost definition, evaluation-at-equality, the canonical threshold and its positivity, and ForcingChainComp3Cert with cert_inhabited; this lemma is the nonnegativity half of that local API. Framework landmark: T5 J-uniqueness fixes $J(x)=\cosh(\log x)-1$, whose range is $[0,\infty)$, so every derived cost (including domain cost) inherits $J\ge 0$. No downstream used_by edges are recorded yet; the lemma is infrastructure for the certificate rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.