weightTarget
plain-language theorem explainer
weightTarget isolates the integer target-matching condition for witnesses in the 8-Balanced J-Subset Sum problem. Cryptography researchers in the Recognition Science setting would cite it when decomposing solution predicates into weight, residue, and cost components. The definition is a direct one-line equality between the summed weights over the witness support and the instance target.
Claim. Let $I$ be an instance with $n$ items, integer weights $w_i$, residues in $ZMod 8$, phi-rungs, target integer $t$, and real bound. For a witness $W$ with support set $S$, the weight target condition holds precisely when $sum_{i in S} w_i = t$.
background
The module defines the 8-Balanced J-Subset Sum as the first RS-native cryptography candidate in deliberately elementary form, with no security claims. An instance is a finite collection of items each equipped with an integer weight, a residue modulo 8, a phi-rung, an integer target sum, and a real J-cost bound. A witness is simply the finite support set of selected indices.
proof idea
The definition is a one-line wrapper that applies the local weightSum (the integer sum of weights over the witness support) and checks equality against the instance target.
why it matters
This definition supplies the first conjunct of the isSolution predicate, which is invoked by fromSubsetSum_isSolution to embed ordinary subset-sum solutions as degenerate BJSS cases. It participates in the module's construction of an 8-neutral, phi-rung cost problem, aligning with the eight-tick octave and residue structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.