residueSum
plain-language theorem explainer
This definition computes the sum in ZMod 8 of the residues attached to items selected by a witness in an 8-Balanced J-Subset Sum instance. Cryptography and subset-sum constructions in Recognition Science would cite it to enforce the neutrality condition. The definition is a direct summation over the witness support using the instance residue map.
Claim. For an 8-Balanced J-Subset Sum instance with residue map $r: [n] → ℤ/8ℤ$ and a witness whose support is a finite set $S ⊆ [n]$, the residue sum is $∑_{i∈S} r(i)$ computed in $ℤ/8ℤ$.
background
The module defines 8-Balanced J-Subset Sum instances as finite collections of items, each carrying an integer weight, a residue in ZMod 8, a phi-rung, together with an integer target and a real J-cost bound. A witness is simply a Finset support selecting a subset of those items. The local setting is deliberately non-cryptographic: the construction supplies a candidate problem whose solutions must meet the target equation, 8-neutrality, and the cost bound, without any security claim.
proof idea
One-line definition that applies the Finset sum operator to the residue function of the instance restricted to the witness support.
why it matters
The definition supplies the left-hand side of the residueNeutral predicate used by fromSubsetSum_isSolution and by any later solver that must enforce 8-neutrality. It directly implements the eight-tick octave (T7) constraint inside the Balanced J-Subset Sum candidate. The parent theorem fromSubsetSum_isSolution shows that ordinary subset-sum solutions embed as degenerate cases satisfying this residue condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.