BJSSWitness
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim that finding a witness is computationally tractable.
- Does not assert any cryptographic security property.
- Does not handle infinite collections of items.
- Does not encode the full solution predicate; only the support data.
formal statement (Lean)
46structure BJSSWitness (inst : BJSSInstance) where
47 support : Finset (Fin inst.n)
48
49/-- Integer target sum. -/