This definition gives the library's named construction or computation for “first entry”. The first pass computes one entry of 'A_bit * E'.
noncomputable def firstEntry {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (bit : Fin 2) (a : Fin l) (j : Fin m) : Run ℝ :=
sumEntries fun b => do
let x ← StoredThinLQ.entry A a (finProdFinEquiv (bit, b))
let y ← StoredThinLQ.entry E b j
StoredGivens.mul x y
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “first pass”.
noncomputable def firstPass {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (bit : Fin 2) : Run (StoredMatrix l m) :=
materialize (firstEntry A E bit)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “first pass value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem firstPass_value {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (bit : Fin 2) :
denote (firstPass A E bit).value = slice (denoteCore A) bit * denote E := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “second entry”. The second pass reads the stored first pass and the original core.
noncomputable def secondEntry {l m : ℕ} (F : StoredMatrix l m)
(A : StoredCore l m) (bit : Fin 2) (a c : Fin l) : Run ℝ :=
sumEntries fun j => do
let x ← StoredThinLQ.entry F a j
let y ← StoredThinLQ.entry A c (finProdFinEquiv (bit, j))
StoredGivens.mul x y
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “second pass”.
noncomputable def secondPass {l m : ℕ} (F : StoredMatrix l m)
(A : StoredCore l m) (bit : Fin 2) : Run (StoredMatrix l l) :=
materialize (secondEntry F A bit)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “second pass value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem secondPass_value {l m : ℕ} (F : StoredMatrix l m)
(A : StoredCore l m) (bit : Fin 2) :
denote (secondPass F A bit).value = denote F * (slice (denoteCore A) bit).transpose := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “add matrices”.
noncomputable def addMatrices {l : ℕ} (A B : StoredMatrix l l) :
Run (StoredMatrix l l) :=
materialize fun a c => do
let x ← StoredThinLQ.entry A a c
let y ← StoredThinLQ.entry B a c
StoredGivens.add x y
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “add matrices value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem addMatrices_value {l : ℕ} (A B : StoredMatrix l l) :
denote (addMatrices A B).value = denote A + denote B := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “update”. All four contraction outputs and the sum are materialized.
noncomputable def update {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) : Run (StoredMatrix l l) := do
let F₀ ← firstPass A E 0
let G₀ ← secondPass F₀ A 0
let F₁ ← firstPass A E 1
let G₁ ← secondPass F₁ A 1
addMatrices G₀ G₁
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “update value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem update_value {l m : ℕ} (A : StoredCore l m) (E : StoredMatrix m m) :
denote (update A E).value =
∑ bit : Fin 2, slice (denoteCore A) bit * denote E *
(slice (denoteCore A) bit).transpose := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “cache node”. A fixed six-word traversal/cache-record allowance per chain node, as in the stored canonicalizer.
def cacheNode (run : Run α) : Run α := ⟨run.value, nodeBudget + run.cost⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “gram”. Streaming cached Gram environments.
noncomputable def gram : {n l r : ℕ} → StoredChain n l r → Run (StoredMatrix l l)
| _, _, _, .nil r => cacheNode (StoredRectangularGivens.identity r)
| _, _, _, .cons A C => cacheNode do
let E ← gram C
update A E
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gram value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem gram_value {n l r : ℕ} (C : StoredChain n l r) :
denote (gram C).value = TensorTrainNormEnvironment.gram (denoteChain C) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “norm”. Scalar-boundary norm with the final table lookup and square root charged.
noncomputable def norm {n : ℕ} (C : StoredChain n 1 1) : Run ℝ := do
let E ← gram C
let mass ← StoredThinLQ.entry E 0 0
StoredGivens.sqrt mass
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_value {n : ℕ} (C : StoredChain n 1 1) :
(norm C).value = TensorTrainNormEnvironment.norm (denoteChain C) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm eq sum”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_eq_sum {n : ℕ} (C : StoredChain n 1 1) :
(norm C).value = Real.sqrt (∑ x : Word n, contract (denoteChain C) x 0 0 ^ 2) :=
(norm_value C).trans (TensorTrainNormEnvironment.norm_eq (denoteChain C))
/-! ## Operation counts for the same producer -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “product budget”. Scalar-boundary norm with the final table lookup and square root charged.
def productBudget (l m r : ℕ) : Cost := fun op =>
l * r * m * (4 * tick .read op + 2 * tick .field op) +
(l * r + l) * (2 * tick .read op + 2 * tick .write op)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “addition budget”.
def additionBudget (l : ℕ) : Cost := fun op =>
l * l * (4 * tick .read op + tick .field op) +
(l * l + l) * (2 * tick .read op + 2 * tick .write op)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “update budget”.
def updateBudget (l m : ℕ) : Cost :=
productBudget l m m + productBudget l m l +
productBudget l m m + productBudget l m l + additionBudget l
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “first entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem firstEntry_cost_le {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (bit : Fin 2) (a : Fin l) (j : Fin m) (op : Op) :
(firstEntry A E bit a j).cost op ≤ m * (4 * tick .read op + 2 * tick .field op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “second entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem secondEntry_cost_le {l m : ℕ} (F : StoredMatrix l m)
(A : StoredCore l m) (bit : Fin 2) (a c : Fin l) (op : Op) :
(secondEntry F A bit a c).cost op ≤ m * (4 * tick .read op + 2 * tick .field op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “first pass cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem firstPass_cost_le {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (bit : Fin 2) (op : Op) :
(firstPass A E bit).cost op ≤ productBudget l m m op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “second pass cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem secondPass_cost_le {l m : ℕ} (F : StoredMatrix l m)
(A : StoredCore l m) (bit : Fin 2) (op : Op) :
(secondPass F A bit).cost op ≤ productBudget l m l op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “add matrices cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem addMatrices_cost_le {l : ℕ} (A B : StoredMatrix l l) (op : Op) :
(addMatrices A B).cost op ≤ additionBudget l op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “update cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem update_cost_le {l m : ℕ} (A : StoredCore l m)
(E : StoredMatrix m m) (op : Op) :
(update A E).cost op ≤ updateBudget l m op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “update total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem update_total_cost_le {l m : ℕ} (A : StoredCore l m) (E : StoredMatrix m m) :
StoredRectangularGivens.total (update A E).cost ≤
12 * l * m * m + 12 * l * l * m + 8 * l * m + 17 * l * l + 20 * l := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gram total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Total of all eight counters, including every materialization pass and the fixed node records.
theorem gram_total_cost_le {n l r : ℕ} (C : StoredChain n l r) (D : ℕ)
(bound : maxBond (denoteChain C) ≤ D) :
StoredRectangularGivens.total (gram C).cost ≤
n * (24 * D ^ 3 + 25 * D ^ 2 + 20 * D + 6) + 5 * D ^ 2 + 4 * D + 6 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem norm_cost {n : ℕ} (C : StoredChain n 1 1) (op : Op) :
(norm C).cost op = (gram C).cost op + 2 * tick .read op + tick .sqrt op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. The scalar supplier adds precisely two stored reads and one square root.
theorem norm_total_cost_le {n : ℕ} (C : StoredChain n 1 1) (D : ℕ)
(bound : maxBond (denoteChain C) ≤ D) :
StoredRectangularGivens.total (norm C).cost ≤
n * (24 * D ^ 3 + 25 * D ^ 2 + 20 * D + 6) + 5 * D ^ 2 + 4 * D + 9 := by
commit-pinned source · Verso Blueprint panel