solutionDecidable

formal source

  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
 114  constructor
 115  · simpa [weightTarget, weightSum, fromSubsetSum] using h
 116  constructor
 117  · simp [residueNeutral, residueSum, fromSubsetSum]
 118  · have hcost := fromSubsetSum_totalJCost_zero weight target S
 119    change totalJCost (fromSubsetSum weight target) ⟨S⟩ ≤ 0
 120    exact le_of_eq hcost