This definition gives the library's named construction or computation for “inverse powers”. Cache '1 / 2^j' by one real division per extension, with full-copy writes.
noncomputable def inversePowers : (d : ℕ) → Run (Vector ℝ (d + 1))
| 0 => collect (fun _ : Fin 1 => pure (1 : ℝ))
| d + 1 => do
let previous ← inversePowers d
let last ← StoredGivens.read previous (Fin.last d)
let next ← StoredGivens.div last 2
StoredHermiteCoefficients.extend previous next
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “inverse powers value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem inversePowers_value (d : ℕ) (i : Fin (d + 1)) :
(inversePowers d).value[i.val] = 1 / (2 : ℝ) ^ i.val := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “tables”. A proposition-valued field is a requirement until a constructor supplies it.
structure Tables (d : ℕ) where
falseTable : StoredMatrix (d + 1) (d + 1)
trueTable : StoredMatrix (d + 1) (d + 1)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “false entry”.
noncomputable def falseEntry {d : ℕ} (F H : Vector ℝ (d + 1))
(i j : Fin (d + 1)) : Run ℝ := do
let _ ← charge .compare ()
if h : i.val ≤ j.val then do
let binomial ← StoredHermiteCoefficients.chooseFrom F j.val i.val h (by omega)
let power ← StoredGivens.read H j
StoredGivens.mul binomial power
else pure 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “true entry”.
noncomputable def trueEntry {d : ℕ} (F H : Vector ℝ (d + 1))
(i j : Fin (d + 1)) : Run ℝ := do
let _ ← charge .compare ()
if h : j.val ≤ i.val then do
let binomial ← StoredHermiteCoefficients.chooseFrom F (d - j.val)
(i.val - j.val) (by omega) (by omega)
let power ← StoredGivens.read H ⟨d - j.val, by omega⟩
StoredGivens.mul binomial power
else pure 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “false entry value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem falseEntry_value {d : ℕ} (F H : Vector ℝ (d + 1))
(hF : ∀ i : Fin (d + 1), F[i.val] = (i.val.factorial : ℝ))
(hH : ∀ i : Fin (d + 1), H[i.val] = 1 / (2 : ℝ) ^ i.val)
(i j : Fin (d + 1)) : (falseEntry F H i j).value = sharedCore d false i j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “true entry value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem trueEntry_value {d : ℕ} (F H : Vector ℝ (d + 1))
(hF : ∀ i : Fin (d + 1), F[i.val] = (i.val.factorial : ℝ))
(hH : ∀ i : Fin (d + 1), H[i.val] = 1 / (2 : ℝ) ^ i.val)
(i j : Fin (d + 1)) : (trueEntry F H i j).value = sharedCore d true i j := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile”. Both tables share a single factorial table and a single inverse-power table.
noncomputable def compile (d : ℕ) : Run (Tables d) := do
let F ← StoredHermiteCoefficients.factorials d
let H ← inversePowers d
let left ← materialize (falseEntry F.values H)
let right ← materialize (trueEntry F.values H)
pure ⟨left, right⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile false”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_false (d : ℕ) :
denote (compile d).value.falseTable = sharedCore d false := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile true”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_true (d : ℕ) :
denote (compile d).value.trueTable = sharedCore d true := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “with cost”.
def withCost (extra : Cost) (result : Run α) : Run α :=
⟨result.value, extra + result.cost⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “with cost value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem withCost_value (extra : Cost) (result : Run α) :
(withCost extra result).value = result.value := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “with cost cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem withCost_cost (extra : Cost) (result : Run α) (op : Op) :
(withCost extra result).cost op = extra op + result.cost op := rfl
/-- Parameter arithmetic is an explicit, separately reusable supplier. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “shifted restriction”. Parameter arithmetic is an explicit, separately reusable supplier.
noncomputable def shiftedRestriction {d : ℕ} (xs : Vector ℝ (d + 1))
(childLower childUpper : ℝ) : Run (Vector ℝ (d + 1)) :=
let u := StoredGivens.add 1 childLower
let v := StoredGivens.add 1 childUpper
withCost (u.cost + v.cost) (StoredBernstein.restrict xs u.value v.value)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “shifted restriction value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem shiftedRestriction_value {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
(hx : ∀ i : Fin (d + 1), xs[i.val] = c i.val)
(a b : ℝ) (i : Fin (d + 1)) :
(shiftedRestriction xs a b).value[i.val] =
HermiteBernstein.restrictCoefficients d (1 + a) (1 + b) c i.val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “shifted restriction cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem shiftedRestriction_cost {d : ℕ} (xs : Vector ℝ (d + 1)) (a b : ℝ) (op : Op) :
(shiftedRestriction xs a b).cost op =
2 * tick .field op + (StoredBernstein.restrict xs (1 + a) (1 + b)).cost op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “injection row”. Cached coordinates are real inputs.
noncomputable def injectionRow {d : ℕ} (xs : Vector ℝ (d + 1))
(childLower childUpper : ℝ) (enabled : Bool) : Run (Vector ℝ (d + 1)) :=
withCost (tick .compare) (if enabled then shiftedRestriction xs childLower childUpper
else collect (fun _ => pure 0))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “injection row value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem injectionRow_value {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
(hx : ∀ i : Fin (d + 1), xs[i.val] = c i.val)
(childLower childUpper : ℝ) (enabled : Bool) (i : Fin (d + 1)) :
(injectionRow xs childLower childUpper enabled).value[i.val] =
if enabled then HermiteBernstein.restrictCoefficients d
(1 + childLower) (1 + childUpper) c i.val else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “injection row eq injection core”; the hypotheses and conclusion in the code panel fix its exact scope. Strong row refinement, with a previously stored source coefficient vector.
theorem injectionRow_eq_injectionCore (k : ℕ) (xs : Vector ℝ (2 * k + 1 + 1))
(hx : ∀ i : Fin (2 * k + 1 + 1),
xs[i.val] = HermiteBernstein.sourceBernsteinCoefficient k i.val)
(origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ) (r : ℕ) (bit : Bool)
(childLower childUpper : ℝ) (enabled : Bool)
(hl : childLower = affinePoint origin step (selectedChild schedule r bit))
(hu : childUpper = affinePoint origin step (selectedChild schedule r bit + 2 ^ r))
(he : enabled = true ↔ Full lower upper (selectedChild schedule r bit) (2 ^ r))
(i : Fin (2 * k + 1 + 1)) :
(injectionRow xs childLower childUpper enabled).value[i.val] =
injectionCore k origin step lower upper schedule r bit none (some i) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “inverse powers cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem inversePowers_cost_le (d : ℕ) (op : Op) :
(inversePowers d).cost op ≤ 8 * (d + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “false entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem falseEntry_cost_le {d : ℕ} (F H : Vector ℝ (d + 1))
(i j : Fin (d + 1)) (op : Op) : (falseEntry F H i j).cost op ≤ 8 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “true entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem trueEntry_cost_le {d : ℕ} (F H : Vector ℝ (d + 1))
(i j : Fin (d + 1)) (op : Op) : (trueEntry F H i j).cost op ≤ 8 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Quadratic per-counter bound of the actual two-table producer.
theorem compile_cost_le (d : ℕ) (op : Op) :
(compile d).cost op ≤ 50 * (d + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_total_cost_le (d : ℕ) :
StoredRectangularGivens.total (compile d).cost ≤ 400 * (d + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “injection row cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem injectionRow_cost_le {d : ℕ} (xs : Vector ℝ (d + 1))
(childLower childUpper : ℝ) (enabled : Bool) (op : Op) :
(injectionRow xs childLower childUpper enabled).cost op ≤
2 * StoredBernstein.edgeBudget d op + 5 * tick .field op +
tick .compare op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “injection row total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem injectionRow_total_cost_le {d : ℕ} (xs : Vector ℝ (d + 1))
(childLower childUpper : ℝ) (enabled : Bool) :
StoredRectangularGivens.total (injectionRow xs childLower childUpper enabled).cost ≤
20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 16 := by
commit-pinned source · Verso Blueprint panel