residueSum
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assert existence of solutions for any instance.
- Does not incorporate weights, rungs, or J-cost into the sum.
- Does not claim cryptographic hardness or security properties.
- Does not extend beyond ZMod 8 arithmetic.
Lean usage
residueNeutral inst w := residueSum inst w = 0formal statement (Lean)
54def residueSum (inst : BJSSInstance) (w : BJSSWitness inst) : ZMod 8 :=
proof body
Definition body.
55 ∑ i ∈ w.support, inst.residue i
56
57/-- J-cost contribution of a selected item. -/