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

BJSSInstance

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  37structure BJSSInstance where
  38  n : ℕ
  39  weight : Fin n → ℤ
  40  residue : Fin n → ZMod 8
  41  rung : Fin n → ℤ
  42  target : ℤ
  43  bound : ℝ
  44
  45/-- A candidate witness is just a selected support. -/

used by (13)

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

depends on (12)

Lean names referenced from this declaration's body.