BJSSInstance
plain-language theorem explainer
The BJSSInstance structure encodes a finite 8-balanced J-subset-sum problem via a size n, integer weights, ZMod 8 residues, rung labels, an integer target, and a real J-cost bound. Cryptographers testing Recognition Science primitives would cite it as the base data type for the module's deliberately non-cryptographic candidate. The declaration is a direct structure with six fields and no proof content.
Claim. A BJSSInstance consists of a natural number $n$, a function weight from Fin $n$ to integers, a function residue from Fin $n$ to the integers modulo 8, a function rung from Fin $n$ to integers, an integer target, and a real bound.
background
The module presents 8-Balanced J-Subset Sum as the first RS-native cryptography candidate in deliberately boring form, making no security claim. An instance carries integer weights, residues in ZMod 8, phi-rungs, a target, and a J-cost bound; a witness is then any finite subset meeting the target equation, 8-neutrality, and the cost bound. The rung field re-uses the integer label pattern seen in upstream rung definitions (constant 1 in Compat.Constants; OreClass mapping in AsteroidOreSpectroscopy), while residues exploit the eight-tick period native to the framework.
proof idea
The declaration is a plain structure definition that introduces the six fields with no computational body or proof obligations.
why it matters
BJSSInstance is the root type for every later definition in the module, including BJSSWitness, isSolution, residueNeutral, jCostBound, and fromSubsetSum. It supplies the first RS-native cryptography candidate without security assertions. The ZMod 8 residues tie directly to the eight-tick octave (T7) while the J-cost bound references J-uniqueness (T5) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.