`weightSum`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.BalancedJSubsetSum on GitHub at line 50.

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

  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
  68def residueNeutral (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  69  residueSum inst w = 0
  70
  71def jCostBound (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  72  totalJCost inst w ≤ inst.bound
  73
  74/-- Full solution predicate for the finite BJSS problem. -/
  75def isSolution (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  76  weightTarget inst w ∧ residueNeutral inst w ∧ jCostBound inst w
  77
  78theorem rungCost_nonneg (inst : BJSSInstance) (i : Fin inst.n) :
  79    0 ≤ rungCost inst i := by
  80  unfold rungCost

papers checked against this theorem

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