`weightTarget`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.BalancedJSubsetSum on GitHub at line 65.

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

  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
  81  exact Cost.Jcost_nonneg (rungValue_pos (inst.rung i))
  82
  83theorem totalJCost_nonneg (inst : BJSSInstance) (w : BJSSWitness inst) :
  84    0 ≤ totalJCost inst w := by
  85  unfold totalJCost
  86  exact Finset.sum_nonneg (fun i _hi => rungCost_nonneg inst i)
  87
  88/-- Classical decidability of the finite solution predicate. This is only a
  89finite search statement, not an efficiency claim. -/
  90noncomputable def solutionDecidable (inst : BJSSInstance) (w : BJSSWitness inst) :
  91    Decidable (isSolution inst w) := by
  92  classical
  93  exact inferInstance
  94
  95/-- Ordinary subset-sum embeds by using zero residues, zero rungs, and zero

papers checked against this theorem

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