pith. machine review for the scientific record. sign in
def definition def or abbrev high

fromSubsetSum

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  97def fromSubsetSum {n : ℕ} (weight : Fin n → ℤ) (target : ℤ) : BJSSInstance where
  98  n := n

proof body

Definition body.

  99  weight := weight
 100  residue := fun _ => 0
 101  rung := fun _ => 0
 102  target := target
 103  bound := 0
 104

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.