rungCost_nonneg
plain-language theorem explainer
Nonnegativity of the J-cost contribution from each rung in a balanced J-subset sum instance follows immediately from the positivity of rung values and the AM-GM property of Jcost. Cryptography modelers in the Recognition Science setting would reference this when verifying cost bounds on subset sum witnesses. The argument is a one-line wrapper that applies the established Jcost nonnegativity lemma after unfolding the rungCost definition.
Claim. Let $I$ be an 8-balanced J-subset sum instance with $n$ elements. For each index $i$ in the finite set of size $n$, the inequality $0 ≤ Jcost(rungValue(I.rung(i)))$ holds.
background
The 8-Balanced J-Subset Sum module defines a structure BJSSInstance consisting of a natural number n, functions assigning integer weights, ZMod 8 residues, and rung indices to each of the n positions, together with an integer target and a real bound. This setup encodes a candidate for RS-native cryptography in a simple form that makes no security assertions, as stated in the module documentation.
proof idea
Unfold rungCost to obtain Jcost of rungValue applied to the rung entry, then apply the lemma Jcost_nonneg using the positivity supplied by rungValue_pos.
why it matters
The result is invoked in the proof of totalJCost_nonneg to conclude that the sum of rung costs over any witness is nonnegative. It supplies the elementary nonnegativity step required for cost accounting in the balanced subset sum construction, aligning with the Recognition Science framework where J-costs are nonnegative by the functional equation and the definition of J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.