weightTarget
plain-language theorem explainer
weightTarget asserts that the integer sum of weights over a witness support equals the instance target. Cryptographers testing RS-native subset-sum candidates would reference the predicate when isolating the weight-matching clause inside solution checks. The definition is realized as a direct equality to the module's weightSum.
Claim. For an instance with $n$, weights $w_i : Fin n → ℤ$, residues in $ℤ/8ℤ$, rungs, target $t ∈ ℤ$ and bound, together with a witness support $S ⊆ Fin n$, the predicate holds when $∑_{i ∈ S} w_i = t$.
background
The module defines the 8-Balanced J-Subset Sum problem as an RS-native cryptography candidate with no security claims. BJSSInstance packages a finite collection of integer weights, ZMod 8 residues, phi-rungs, an integer target, and a real-valued J-cost bound. BJSSWitness records only the selected support subset of indices.
proof idea
One-line definition that applies the local weightSum (itself a sum over the witness support) and equates it to the instance target field.
why it matters
weightTarget supplies the integer-weight clause inside the isSolution predicate. It is invoked directly by fromSubsetSum_isSolution to embed ordinary subset-sum solutions and by isSolution itself. The predicate therefore participates in the first RS-native cryptography construction built on J-cost and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.