isSolution
plain-language theorem explainer
The predicate declares a witness subset to solve a finite 8-balanced J-subset sum instance precisely when its weights sum to the target integer, its residues sum to zero modulo 8, and its total J-cost stays below the given bound. Researchers constructing discrete optimization analogs or identification hypotheses in Recognition Science would cite it as the basic solution concept for this module. It is realized as the direct conjunction of the three component predicates weightTarget, residueNeutral, and jCostBound.
Claim. Let $I$ be an instance with $n$ elements, integer weights $w_i$, residues $r_i$ in $Z/8Z$, rungs, target integer $T$, and real bound $B$. For a witness subset $S$, the predicate holds if and only if the sum of $w_i$ over $i$ in $S$ equals $T$, the sum of $r_i$ over $i$ in $S$ equals 0 in $Z/8Z$, and the total J-cost of $S$ is at most $B$.
background
The module presents the 8-Balanced J-Subset Sum as an initial RS-native cryptography candidate in deliberately minimal form, with no security claims attached. A BJSSInstance packages a finite $n$, a function assigning integer weights, residues in ZMod 8, phi-rungs, an integer target, and a real J-cost bound. A BJSSWitness supplies only the Finset support selecting which elements participate.
proof idea
This is a one-line definition that directly conjoins the three predicates weightTarget, residueNeutral, and jCostBound applied to the supplied instance and witness.
why it matters
The predicate supplies the concrete solution notion for the balanced J-subset sum problem and is referenced when building identification hypotheses in the 2D continuum limit, including coeffBound, divFreeCoeffBound, and continuum_limit_exists. It parallels the isSolution predicate from the ECDLPWatch module and connects to the J-cost and rung structures of the Recognition framework, though the module itself leaves cryptographic analysis open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.