totalJCost_nonneg

formal source

  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
  96cost bound. -/
  97def fromSubsetSum {n : ℕ} (weight : Fin n → ℤ) (target : ℤ) : BJSSInstance where
  98  n := n
  99  weight := weight
 100  residue := fun _ => 0
 101  rung := fun _ => 0
 102  target := target
 103  bound := 0
 104
 105theorem fromSubsetSum_totalJCost_zero {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 106    (S : Finset (Fin n)) :
 107    totalJCost (fromSubsetSum weight target) ⟨S⟩ = 0 := by
 108  simp [totalJCost, rungCost, fromSubsetSum, Cost.Jcost_unit0]
 109
 110/-- Any ordinary subset-sum solution gives a degenerate BJSS solution. -/
 111theorem fromSubsetSum_isSolution {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 112    (S : Finset (Fin n)) (h : (∑ i ∈ S, weight i) = target) :
 113    isSolution (fromSubsetSum weight target) ⟨S⟩ := by