This definition gives the library's named construction or computation for “terminal entry”.
noncomputable def terminalEntry {D : ℕ} (A : StoredCore D D)
(right : Vector ℝ D) (a : Fin D) (bit : Fin 2) : Run ℝ :=
sumEntries fun b => do
let x ← StoredThinLQ.entry A a (finProdFinEquiv (bit, b))
let y ← read right b
StoredGivens.mul x y
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “terminal”.
noncomputable def terminal {D : ℕ} (A : StoredCore D D)
(right : Vector ℝ D) : Run (StoredCore D 1) :=
materialize fun a j => terminalEntry A right a (finProdFinEquiv.symm j).1
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “initial entry”.
noncomputable def initialEntry {D r : ℕ} (left : Vector ℝ D)
(A : StoredCore D r) (j : Fin (2 * r)) : Run ℝ :=
sumEntries fun a => do
let x ← read left a
let y ← StoredThinLQ.entry A a j
StoredGivens.mul x y
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “initial”.
noncomputable def initial {D r : ℕ} (left : Vector ℝ D)
(A : StoredCore D r) : Run (StoredCore 1 r) :=
materialize fun _ j => initialEntry left A j
/-- Copy only references to already materialized local cores. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “tail table”. Copy only references to already materialized local cores.
def tailTable {α : Type} {n : ℕ} (xs : Vector α (n + 1)) : Run (Vector α n) :=
collect fun i => read xs i.succ
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “tail chain”.
noncomputable def tailChain {D : ℕ} : {n : ℕ} →
Vector (StoredCore D D) (n + 1) → Vector ℝ D → Run (StoredChain (n + 1) D 1)
| 0, tables, right => do
let A ← read tables 0
let B ← terminal A right
(⟨.cons B (.nil 1), 2 • nodeBudget⟩ : Run _)
| _n + 1, tables, right => do
let A ← read tables 0
let ts ← tailTable tables
let C ← tailChain ts right
(⟨.cons A C, nodeBudget⟩ : Run _)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “close left”.
noncomputable def closeLeft {n D : ℕ} (left : Vector ℝ D) :
StoredChain (n + 1) D 1 → Run (StoredChain (n + 1) 1 1)
| .cons A C => do
let B ← initial left A
(⟨.cons B C, nodeBudget⟩ : Run _)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “of table”.
noncomputable def ofTable {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) : Run (StoredChain (n + 1) 1 1) := do
let C ← tailChain tables right
closeLeft left C
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_value {D : ℕ} (A : StoredCore D D) (right : Vector ℝ D) :
denoteCore (terminal A right).value =
fun a out => ∑ b, denoteCore A a (out.1, b) * right[b.val] := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_value {D r : ℕ} (left : Vector ℝ D) (A : StoredCore D r) :
denoteCore (initial left A).value = fun _ out => ∑ a, left[a.val] * denoteCore A a out := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “tail table value”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem tailTable_value {α : Type} {n : ℕ} (xs : Vector α (n + 1)) (i : Fin n) :
(tailTable xs).value[i.val] = xs[i.succ.val] := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “window”. Kernel appears only in this finite-window specification, never production.
def Window {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(K : MatrixProductChain.Kernel D) (start : ℕ) : Prop :=
∀ i : Fin (n + 1), denoteCore tables[i.val] = fun a out => K (start + i.val) out.1 a out.2
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “tail chain value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem tailChain_value {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(right : Vector ℝ D) (K : MatrixProductChain.Kernel D) (start : ℕ)
(h : Window tables K start) :
denoteChain (tailChain tables right).value =
MatrixProductChain.tailChain K (fun i => right[i.val]) start n := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “close left value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem closeLeft_value {n D : ℕ} (left : Vector ℝ D) (C : StoredChain (n + 1) D 1) :
denoteChain (closeLeft left C).value =
MatrixProductChain.closeLeft (fun i => left[i.val]) (denoteChain C) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “of table refines”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem ofTable_refines {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) (K : MatrixProductChain.Kernel D) (start : ℕ)
(h : Window tables K start) :
denoteChain (ofTable tables left right).value =
MatrixProductChain.ofKernel K (fun i => left[i.val]) (fun i => right[i.val]) start n := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal entry cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminalEntry_cost {D : ℕ} (A : StoredCore D D) (right : Vector ℝ D)
(a : Fin D) (bit : Fin 2) (op : Op) :
(terminalEntry A right a bit).cost op = D * (3 * tick .read op + 2 * tick .field op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial entry cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initialEntry_cost {D r : ℕ} (left : Vector ℝ D) (A : StoredCore D r)
(j : Fin (2 * r)) (op : Op) :
(initialEntry left A j).cost op = D * (3 * tick .read op + 2 * tick .field op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_cost {D : ℕ} (A : StoredCore D D) (right : Vector ℝ D) (op : Op) :
(terminal A right).cost op =
2 * D ^ 2 * (3 * tick .read op + 2 * tick .field op) +
6 * D * (tick .read op + tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_cost {D r : ℕ} (left : Vector ℝ D) (A : StoredCore D r) (op : Op) :
(initial left A).cost op =
2 * r * D * (3 * tick .read op + 2 * tick .field op) +
(4 * r + 2) * (tick .read op + tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “tail table cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem tailTable_cost {α : Type} {n : ℕ} (xs : Vector α (n + 1)) (op : Op) :
(tailTable xs).cost op = n * (3 * tick .read op + 2 * tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_total_cost {D : ℕ} (A : StoredCore D D) (right : Vector ℝ D) :
StoredRectangularGivens.total (terminal A right).cost = 10 * D ^ 2 + 12 * D := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_total_cost {D r : ℕ} (left : Vector ℝ D) (A : StoredCore D r) :
StoredRectangularGivens.total (initial left A).cost = 10 * r * D + 8 * r + 4 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “tail table total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem tailTable_total_cost {α : Type} {n : ℕ} (xs : Vector α (n + 1)) :
StoredRectangularGivens.total (tailTable xs).cost = 5 * n := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “tail chain total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem tailChain_total_cost_le {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(right : Vector ℝ D) :
StoredRectangularGivens.total (tailChain tables right).cost ≤
10 * D ^ 2 + 12 * D + 5 * n ^ 2 + 7 * n + 13 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “close left tail total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem closeLeft_tail_total_cost_le {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) :
StoredRectangularGivens.total (closeLeft left (tailChain tables right).value).cost ≤
10 * D ^ 2 + 18 * D + 18 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “of table total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Bound for the very same run whose value refines 'ofKernel'; includes terminal/initial arithmetic, materialization, copied references, and nodes.
theorem ofTable_total_cost_le {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) :
StoredRectangularGivens.total (ofTable tables left right).cost ≤
20 * D ^ 2 + 30 * D + 5 * n ^ 2 + 7 * n + 31 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “window of entries”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise supplier adapter; only the stored finite window is constrained.
theorem window_of_entries {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(K : MatrixProductChain.Kernel D) (start : ℕ)
(h : ∀ (i : Fin (n + 1)) (a b : Fin D) (bit : Fin 2),
denoteCore tables[i.val] a (bit, b) = K (start + i.val) bit a b) :
Window tables K start := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “of table max bond”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem ofTable_maxBond {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) (K : MatrixProductChain.Kernel D) (start : ℕ)
(h : Window tables K start) :
maxBond (denoteChain (ofTable tables left right).value) ≤ max D 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “of table certified”; the hypotheses and conclusion in the code panel fix its exact scope. One producer, with both exact returned data and polynomial charged work.
theorem ofTable_certified {n D : ℕ} (tables : Vector (StoredCore D D) (n + 1))
(left right : Vector ℝ D) (K : MatrixProductChain.Kernel D) (start : ℕ)
(h : Window tables K start) :
let result := ofTable tables left right
denoteChain result.value =
MatrixProductChain.ofKernel K (fun i => left[i.val]) (fun i => right[i.val]) start n ∧
StoredRectangularGivens.total result.cost ≤
20 * D ^ 2 + 30 * D + 5 * n ^ 2 + 7 * n + 31 :=
⟨ofTable_refines tables left right K start h, ofTable_total_cost_le tables left right⟩
commit-pinned source · Verso Blueprint panel