fromSubsetSum_isSolution
plain-language theorem explainer
Ordinary subset-sum solutions embed directly as solutions to the balanced J-subset-sum instance obtained by setting all residues and rungs to zero. Recognition Science users working on the cryptography module would cite this to record the classical reduction. The proof is a direct verification that splits the isSolution conjunction and invokes the zero total J-cost lemma for the embedded instance.
Claim. Let $w : [n] → ℤ$ and $t ∈ ℤ$. If a finite subset $S ⊆ [n]$ satisfies $∑_{i∈S} w_i = t$, then the witness corresponding to $S$ satisfies the weight-target equation, the residue-neutrality condition (sum of residues ≡ 0 mod 8), and the J-cost bound for the BJSS instance built from $w$ and $t$ by assigning zero residues and zero rungs to every index.
background
The module defines the 8-Balanced J-Subset Sum problem as the first RS-native cryptography candidate, deliberately without security claims. An instance carries integer weights, residues in ℤ/8ℤ, phi-rungs, a target integer, and a J-cost bound; a witness is a finite subset of indices whose selected weights sum to the target, whose residues sum to zero modulo 8, and whose total J-cost stays within the bound.
proof idea
The proof applies constructor to split the three conjuncts of isSolution. The weightTarget conjunct follows by simpa from the hypothesis together with the definitions of weightSum and fromSubsetSum. The residueNeutral conjunct is discharged by simp, since fromSubsetSum sets every residue to zero. The jCostBound conjunct is obtained by rewriting with the lemma fromSubsetSum_totalJCost_zero and applying le_of_eq.
why it matters
This theorem records the embedding of ordinary subset-sum into the RS-native BJSS setting, supplying the degenerate base case for the cryptography module. It sits inside the larger Recognition Science program that derives structures from the J-functional equation and the eight-tick octave, yet no downstream results currently depend on it. The open question is whether this reduction will later be used to import hardness statements or to construct explicit phi-ladder instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.