weightSum
plain-language theorem explainer
The definition sums the integer weights selected by a witness support inside an 8-balanced J-subset sum instance. RS modelers and subset-sum analysts cite it when verifying whether a candidate subset meets the declared integer target. It is implemented as a direct finite summation over the support indices using the instance weight map.
Claim. Let $I$ be an 8-balanced J-subset sum instance equipped with weight map $w : [n] → ℤ$ and let $W$ be a witness whose support is the finite set $S ⊆ [n]$. The weight sum equals $∑_{i ∈ S} w(i)$.
background
The module presents 8-Balanced J-Subset Sum as a deliberately elementary RS-native candidate problem. An instance packages a finite collection of items, each carrying an integer weight, a residue in ℤ/8ℤ, a phi-rung index, an integer target, and a real J-cost bound. A witness records only the chosen support as a finite subset of indices.
proof idea
The definition is a one-line wrapper that applies summation over the support set of the witness, indexing directly into the instance weight function.
why it matters
This definition supplies the integer sum required by the weight-target predicate, which is invoked both by the from-subset-sum-is-solution theorem and by the uniform-weight results in the N-dimensional cost calibration module. It therefore links the cryptography constructions to the broader cost and rung machinery. Within the Recognition framework the sum serves as a concrete primitive for subset selection under the J-cost and phi-ladder conventions, remaining auxiliary to the T0-T8 forcing chain and carrying no security assertions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.