total_jcost_nonneg
plain-language theorem explainer
The total J-cost summed over all positive ratios in any ledger configuration is non-negative. Researchers analyzing Recognition Science complexity classes cite this to bound ledger energy above the balanced ground state. The proof unfolds the finite sum definition and reduces each term to the non-negativity of J via the AM-GM lemma on positive arguments.
Claim. For any natural number $N$ and any ledger configuration consisting of $N$ positive real ratios $r_i > 0$, the total J-cost satisfies $J(r_1) + J(r_2) + ... + J(r_N) ≥ 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The IC-005 module frames the computational complexity of physics through J-cost minimization on ledger states. LedgerConfig N is the structure holding N positive real ratios together with the proof that each ratio exceeds zero. totalJCost is the sum of J applied to each ratio, with J itself defined via the Recognition Composition Law as the strictly convex function whose unique minimum lies at argument 1.
proof idea
The term proof unfolds totalJCost to a Finset sum, then applies the library lemma Finset.sum_nonneg. This reduces the claim to non-negativity of each summand. For every index the configuration's positivity hypothesis is passed directly to the upstream lemma Cost.Jcost_nonneg, which concludes via the squared representation of J.
why it matters
IC-005.9 supplies the non-negativity half of the complexity summary that appears in the downstream ic005_certificate. It anchors the claim that ground-state verification is linear-time and that J-cost minimization is convex, consistent with the eight-tick octave and the phi-ladder mass formula. The result closes one link in the chain from T5 J-uniqueness to the D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.