residueNeutral
plain-language theorem explainer
The residueNeutral definition states that a witness to an 8-Balanced J-Subset Sum instance satisfies 8-neutrality precisely when the sum of its selected residues modulo 8 vanishes. Modelers constructing or verifying subset-sum variants in the Recognition Science setting would cite this predicate as the balance component inside the full solution check. The definition is a direct one-line abbreviation that sets the residueSum function equal to zero.
Claim. For an instance $I$ with $n$ items, integer weights $w_i$, residues $r_i$ in the cyclic group of order 8, rungs, target integer sum, and real J-cost bound, together with a witness given by a finite index subset $S$, the residue-neutrality condition is the statement that the sum of the selected residues equals zero in that group: $r_S = 0$ where $r_S = 0$ in $Z/8Z$.
background
The Balanced J-Subset Sum module defines a deliberately elementary RS-native cryptography candidate that makes no security claim. An instance consists of a finite list of items, each equipped with an integer weight, a residue in ZMod 8, a phi-rung label, a global integer target, and a real-valued J-cost bound. A witness is simply a finite subset of the item indices that is required to meet three independent conditions: exact weight sum, 8-neutrality, and J-cost bound.
proof idea
This is a one-line definition that directly equates residueNeutral to the predicate residueSum inst w = 0 in the ZMod 8 group.
why it matters
The predicate supplies the 8-neutrality clause inside the isSolution definition, which is then invoked by fromSubsetSum_isSolution to lift ordinary subset-sum solutions into the BJSS setting. The modulus 8 is chosen to match the eight-tick octave (T7) of the UnifiedForcingChain, furnishing a direct bridge between the forcing chain and the cryptographic construction. The module doc explicitly disclaims any security claim, leaving the predicate as pure verification scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.