fromSubsetSum

formal source

  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
 121
 122end
 123
 124end BalancedJSubsetSum
 125end Cryptography
 126end IndisputableMonolith