fromSubsetSum
plain-language theorem explainer
Ordinary subset-sum problems embed into 8-balanced J-subset-sum instances by zeroing all residues modulo 8, all rungs, and the J-cost bound. Researchers examining degenerate cases of the balanced subset-sum construction in the Recognition Science cryptography module would cite this embedding. The definition proceeds by direct record construction of the BJSSInstance structure, copying the supplied weights and target while forcing the extra fields to zero.
Claim. Let $n$ be a natural number, $w :$ Fin $n$ to integers, and $t$ an integer. The map produces the BJSSInstance with $n$ elements, weights given by $w$, residues identically zero in the cyclic group of order 8, rungs identically zero, target $t$, and bound zero.
background
The module introduces 8-Balanced J-Subset Sum as an RS-native cryptography candidate in deliberately simple form with no security claims. An instance consists of a natural number $n$, integer weights on Fin $n$, residues in ZMod 8, integer rungs, an integer target, and a real bound on J-cost; a witness is a subset satisfying the target sum, 8-neutrality on residues, and the cost bound. The structure BJSSInstance is the core data type that packages these fields.
proof idea
This is a definition that constructs the BJSSInstance record by copying the input parameters $n$, weight, and target while setting residue to the constant zero function, rung to the constant zero function, and bound to zero.
why it matters
It supplies the canonical embedding that lets ordinary subset-sum solutions count as degenerate BJSS solutions, directly feeding the downstream theorems fromSubsetSum_isSolution and fromSubsetSum_totalJCost_zero. In the Recognition framework this provides the trivial case for J-cost and 8-neutrality before non-zero rungs or residues are considered; it touches the question of how subset-sum relates to the phi-ladder but asserts no cryptographic properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.