`fromSubsetSum_isSolution`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cryptography.BalancedJSubsetSum on GitHub at line 111.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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

papers checked against this theorem

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