isSolution
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert cryptographic hardness or security for the BJSS problem.
- Does not treat infinite instances or continuous relaxations.
- Does not incorporate rung or phi-ladder structure beyond the cost bound.
- Does not supply an algorithm for finding or deciding solutions.
formal statement (Lean)
75def isSolution (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
proof body
Definition body.
76 weightTarget inst w ∧ residueNeutral inst w ∧ jCostBound inst w
77