BJSSWitness
plain-language theorem explainer
A witness for a balanced J-subset sum instance is a finite subset of indices that can be checked against target weight sum, mod-8 residue neutrality, and J-cost bound. Modelers working on Recognition Science cryptography candidates cite this structure when defining solution predicates for the finite 8-balanced problem. The declaration is a one-field structure definition that simply packages the support set.
Claim. For an instance $I$ with $n$ items, integer weights $w_i$, residues $r_i$ in $ZMod 8$, rungs, target $T$, and bound $B$, a witness is a finset $S$ of indices from $0$ to $n-1$.
background
The module defines the 8-Balanced J-Subset Sum problem as an RS-native cryptography candidate in deliberately elementary form. An instance records a finite collection of items, each carrying an integer weight, a residue modulo 8, a rung index for J-cost computation, together with a target integer sum and a real-valued J-cost bound. The witness structure supplies the support set that downstream predicates will test for exact weight target, residue sum zero, and cost not exceeding the bound.
proof idea
This is a structure definition with a single field. It directly introduces the type of candidate supports for a given BJSSInstance; no lemmas or tactics are applied.
why it matters
The structure is the input type for isSolution, residueNeutral, jCostBound, totalJCost, and residueSum. It supplies the basic data object for the cryptography module, which explores an RS-native subset-sum formulation without security claims. The construction sits inside the broader Recognition framework that derives constants and mass ladders from the J-functional equation and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.