theorem proved term proof

`fromSubsetSum_totalJCost_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 105theorem fromSubsetSum_totalJCost_zero {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 106    (S : Finset (Fin n)) :
 107    totalJCost (fromSubsetSum weight target) ⟨S⟩ = 0 := by

proof body

Term-mode proof.

 108  simp [totalJCost, rungCost, fromSubsetSum, Cost.Jcost_unit0]
 109
 110/-- Any ordinary subset-sum solution gives a degenerate BJSS solution. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

fromSubsetSum_isSolution in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use

depends on (9)

Lean names referenced from this declaration's body.

Jcost_unit0 in IndisputableMonolith.Cost decl_use
Jcost_unit0 in IndisputableMonolith.Cost.JcostCore decl_use
fromSubsetSum in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
rungCost in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
totalJCost in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
totalJCost in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
totalJCost in IndisputableMonolith.Information.ShannonEntropy decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use