fromSubsetSum
plain-language theorem explainer
The definition embeds an ordinary subset-sum problem into the 8-balanced J-subset-sum structure by forcing residues to the zero element of ZMod 8, rungs to zero, and the J-cost bound to zero. Researchers examining Recognition Science cryptography candidates cite it as the base embedding step. It is realized by a direct record constructor that copies the input weight map and target while setting the remaining fields to constants.
Claim. Let $n$ be a natural number, let $w : [n] → ℤ$ be a weight function, and let $t ∈ ℤ$ be a target. The map $(w, t) ↦ I$ yields a BJSSInstance $I$ whose weight field is $w$, whose target is $t$, whose residues are identically zero in ℤ/8ℤ, whose rungs are identically zero, and whose bound is zero.
background
The module defines 8-Balanced J-Subset Sum as the first RS-native cryptography candidate, presented in deliberately simple form with no security claims. A BJSSInstance consists of a size $n$, integer weights on Fin $n$, residues valued in ZMod 8, integer rungs, an integer target, and a real J-cost bound; a witness is a subset whose weights sum to the target, residues sum to zero modulo 8, and total J-cost respects the bound. BJSSInstance is the corresponding structure type.
proof idea
The definition is a direct record constructor for BJSSInstance. It copies the supplied $n$, weight, and target fields, then installs the constant-zero function for residue, the constant-zero function for rung, and the constant 0 for bound.
why it matters
This definition supplies the base embedding that reduces ordinary subset-sum to the balanced J-subset-sum problem. It is invoked by the theorems fromSubsetSum_isSolution and fromSubsetSum_totalJCost_zero, which show that subset-sum solutions produce degenerate BJSS solutions whose total J-cost is zero. Within the Recognition framework it realizes the module's stated 'boring form' of the cryptography candidate before any non-trivial residue or rung structure is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.