fromSubsetSum_isSolution
plain-language theorem explainer
Ordinary subset-sum solutions embed as degenerate cases into the balanced J-subset-sum problem by setting residues and rungs to zero. Researchers formalizing RS-native search problems would cite this when reducing classical subset-sum instances. The term proof constructs the three conjuncts of isSolution directly from the embedding definition and a zero-cost lemma.
Claim. Let $n$ be a natural number, let $w : [n] → ℤ$ be weights, let $t ∈ ℤ$ be a target, and let $S ⊆ [n]$ satisfy $∑_{i∈S} w(i) = t$. Then the witness induced by $S$ satisfies the solution predicate for the embedded instance: the weight sum equals the target, the mod-8 residue sum is zero, and the total J-cost is at most zero.
background
The module introduces 8-balanced J-subset-sum as an RS-native search problem with no security claims. An instance consists of integer weights, residues in ℤ/8ℤ, phi-rungs, a target, and a J-cost bound. A witness is a finite subset meeting three conditions: weight sum equals target, residue sum is neutral (zero mod 8), and total J-cost respects the bound. The predicate isSolution packages these three conjuncts. The embedding fromSubsetSum constructs an instance by copying the weights and target while forcing all residues and rungs to zero and the cost bound to zero. The upstream lemma fromSubsetSum_totalJCost_zero shows that any witness for such an embedded instance has J-cost exactly zero.
proof idea
The term proof opens with constructor to split the three conjuncts of isSolution. The first conjunct is discharged by simpa using the definitions of weightTarget, weightSum, and fromSubsetSum together with the hypothesis that the subset sums to the target. The second conjunct is discharged by simp on residueNeutral, residueSum, and fromSubsetSum. The third conjunct rewrites the cost bound to totalJCost ≤ 0 and applies the upstream lemma fromSubsetSum_totalJCost_zero to obtain equality to zero.
why it matters
This theorem supplies the explicit embedding that lets any classical subset-sum solution serve as a degenerate BJSS solution. It sits inside the cryptography module whose module doc states the construction is deliberately boring and makes no security claim. The result closes the reduction direction from ordinary subset-sum into the RS-native formulation; downstream use would appear in any later argument that treats the balanced problem as a generalization of subset-sum. No open scaffolding remains for this direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.