`rungValue_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Cryptography.BalancedJSubsetSum
domain: Cryptography
line: 32 · 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 32.

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

rungValue IndisputableMonolith.Cryptography.BalancedJSubsetSum

formal source

  29  unfold rungValue
  30  exact Real.exp_pos _
  31
  32@[simp] theorem rungValue_zero : rungValue 0 = 1 := by
  33  unfold rungValue
  34  norm_num
  35
  36/-- One finite 8-Balanced J-Subset Sum instance. -/
  37structure BJSSInstance where
  38  n : ℕ
  39  weight : Fin n → ℤ
  40  residue : Fin n → ZMod 8
  41  rung : Fin n → ℤ
  42  target : ℤ
  43  bound : ℝ
  44
  45/-- A candidate witness is just a selected support. -/
  46structure BJSSWitness (inst : BJSSInstance) where
  47  support : Finset (Fin inst.n)
  48
  49/-- Integer target sum. -/
  50def weightSum (inst : BJSSInstance) (w : BJSSWitness inst) : ℤ :=
  51  ∑ i ∈ w.support, inst.weight i
  52
  53/-- Mod-8 residue sum. -/
  54def residueSum (inst : BJSSInstance) (w : BJSSWitness inst) : ZMod 8 :=
  55  ∑ i ∈ w.support, inst.residue i
  56
  57/-- J-cost contribution of a selected item. -/
  58def rungCost (inst : BJSSInstance) (i : Fin inst.n) : ℝ :=
  59  Cost.Jcost (rungValue (inst.rung i))
  60
  61/-- Total J-cost of a witness support. -/
  62def totalJCost (inst : BJSSInstance) (w : BJSSWitness inst) : ℝ :=

papers checked against this theorem

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