def
definition
jCostBound
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cryptography.BalancedJSubsetSum on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
68def residueNeutral (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
69 residueSum inst w = 0
70
71def jCostBound (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
72 totalJCost inst w ≤ inst.bound
73
74/-- Full solution predicate for the finite BJSS problem. -/
75def isSolution (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
76 weightTarget inst w ∧ residueNeutral inst w ∧ jCostBound inst w
77
78theorem rungCost_nonneg (inst : BJSSInstance) (i : Fin inst.n) :
79 0 ≤ rungCost inst i := by
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