`BJSSInstance`

definition

show as: view math explainer →

module: IndisputableMonolith.Cryptography.BalancedJSubsetSum
domain: Cryptography
line: 37 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.BalancedJSubsetSum on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  34  norm_num
  35
  36/-- One finite 8-Balanced J-Subset Sum instance. -/
  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. -/
  46structure BJSSWitness (inst : BJSSInstance) where
  47  support : Finset (Fin inst.n)
  48
  49/-- Integer target sum. -/
  50def weightSum (inst : BJSSInstance) (w : BJSSWitness inst) : ℤ :=
  51  ∑ i ∈ w.support, inst.weight i
  52
  53/-- Mod-8 residue sum. -/
  54def residueSum (inst : BJSSInstance) (w : BJSSWitness inst) : ZMod 8 :=
  55  ∑ i ∈ w.support, inst.residue i
  56
  57/-- J-cost contribution of a selected item. -/
  58def rungCost (inst : BJSSInstance) (i : Fin inst.n) : ℝ :=
  59  Cost.Jcost (rungValue (inst.rung i))
  60
  61/-- Total J-cost of a witness support. -/
  62def totalJCost (inst : BJSSInstance) (w : BJSSWitness inst) : ℝ :=
  63  ∑ i ∈ w.support, rungCost inst i
  64
  65def weightTarget (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  66  weightSum inst w = inst.target
  67

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.