  25details in the first definition module. -/
  26def rungValue (k : ℤ) : ℝ := Real.exp ((k : ℝ) * Real.log phi)
  27
  28theorem rungValue_pos (k : ℤ) : 0 < rungValue k := by
  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) : ℝ :=

papers checked against this theorem

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