BJSSInstance
plain-language theorem explainer
A structure that packages the data for one finite instance of the 8-balanced J-subset-sum problem: an integer n, a weight map from Fin n to integers, a residue map into ZMod 8, a rung map into integers, a target integer, and a real cost bound. Researchers building RS-native combinatorial primitives would cite this as the input type for witness and solution predicates. The declaration is a plain structure with six fields and no proof obligations.
Claim. An 8-balanced J-subset-sum instance consists of a natural number $n$, a weight function $w : [n] → ℤ$, a residue function $r : [n] → ℤ/8ℤ$, a rung function $ρ : [n] → ℤ$, a target integer $t$, and a real bound $b$.
background
The module presents 8-Balanced J-Subset Sum as the first RS-native cryptography candidate in deliberately elementary form, making no security claims. An instance carries integer weights, residues in ZMod 8, phi-rungs, a target, and a J-cost bound; a witness is a finite subset that meets the target equation, 8-neutrality, and the cost bound. The rung field draws on the same integer-valued rung concept appearing in upstream constants and mass-anchor modules, while the residue field directly encodes the eight-tick periodicity of the forcing chain.
proof idea
The declaration is a structure definition that simply enumerates the six data fields; no lemmas or tactics are applied.
why it matters
BJSSInstance supplies the input type for every subsequent predicate and witness in the same module, including isSolution, residueNeutral, jCostBound, and fromSubsetSum. It therefore anchors the first explicit combinatorial object that incorporates both the eight-tick octave (via ZMod 8 residues) and the phi-ladder (via rungs) inside a cryptography setting. No open questions are closed by the definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.