totalJcost_nonneg
plain-language theorem explainer
The theorem shows that the sum of J-cost terms J(v/n) over a list of positive neighbors n is non-negative for any v > 0. Researchers citing the F1 foundation paper on log-domain J-cost geometry use it to secure positivity before proving geometric-mean optimality. The short tactic proof unfolds the sum definition, applies the lemma that a sum of non-negative reals is non-negative, and reduces each term to Jcost_nonneg on the positive ratio v/n.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For $v > 0$ and any finite list $ns$ of positive reals, the sum over $n$ in $ns$ of $J(v/n)$ satisfies $0$ ≤ sum.
background
The module F1 — Log-Domain J-Cost Geometry collects identities for the canonical reciprocal cost $J(x) = ½(x + x^{-1}) − 1$ and its log-domain geometry. The definition totalJcost(v, ns) is the sum of J(v/n) over the list ns, introduced as F1.2.3 to quantify total bond cost in a small-deviation state. Upstream, Jcost_nonneg states that J(x) ≥ 0 for positive x by the AM-GM inequality, with an equivalent form proved via Jcost_eq_sq and positivity of squares.
proof idea
The proof unfolds totalJcost to expose the mapped sum, then applies List.sum_nonneg. For each element it rewrites the membership condition via List.mem_map, obtains the original neighbor n, rewrites the equality, and invokes Jcost_nonneg on the ratio v/n shown positive by div_pos.
why it matters
This non-negativity result supports the geometric-mean optimality theorem in the same module and supplies the positivity step required by HamiltonianEmergence.totalJcost and NucleosynthesisTiers. It fills the F1.2.3 slot in the foundation paper and is cited by NS, P vs NP, Yang-Mills, and RH arguments. The eight-tick octave and D = 3 landmarks rest on such J-cost bounds remaining non-negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.