QuantumBlockEncoding/StoredTensorTrain.lean

This abbreviation gives a shorter name to the type or expression used for “stored core”.

abbrev StoredCore (l r : ℕ) := StoredMatrix l (2 * r)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “denote core”.

def denoteCore {l r : ℕ} (A : StoredCore l r) : Core l r :=
  fun a out => denote A a (finProdFinEquiv out)

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “stored chain”; its constructors are the cases that downstream code must handle.

inductive StoredChain : ℕ → ℕ → ℕ → Type
  | nil (r : ℕ) : StoredChain 0 r r
  | cons {n l m r : ℕ} (head : StoredCore l m) (tail : StoredChain n m r) :
      StoredChain (n + 1) l r

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “denote chain”.

def denoteChain : {n l r : ℕ} → StoredChain n l r → Chain n l r
  | _, _, _, .nil r => .nil r
  | _, _, _, .cons A C => .cons (denoteCore A) (denoteChain C)

/-- Each callback is invoked once; its arithmetic cost remains charged. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sum entries”. Each callback is invoked once; its arithmetic cost remains charged.

noncomputable def sumEntries : {k : ℕ} → (Fin k → Run ℝ) → Run ℝ
  | 0, _ => pure 0
  | k + 1, f => do
      let first ← f 0
      let rest ← sumEntries (fun i : Fin k => f i.succ)
      StoredGivens.add first rest

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sum entries value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sumEntries_value {k : ℕ} (f : Fin k → Run ℝ) :
    (sumEntries f).value = ∑ i, (f i).value := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sum entries cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sumEntries_cost_le {k : ℕ} (f : Fin k → Run ℝ) (op : Op) (B : ℕ)
    (bound : ∀ i, (f i).cost op ≤ B) :
    (sumEntries f).cost op ≤ k * (B + tick .field op) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “absorption entry”. Multiply the residual into a single bit-preserving output entry.

noncomputable def absorptionEntry {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) (a : Fin l) (out : Fin 2 × Fin r) : Run ℝ :=
  sumEntries fun b => do
    let x ← StoredThinLQ.entry A a (finProdFinEquiv (out.1, b))
    let y ← StoredThinLQ.entry R b out.2
    StoredGivens.mul x y

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “absorption entry value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem absorptionEntry_value {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) (a : Fin l) (out : Fin 2 × Fin r) :
    (absorptionEntry A R a out).value = absorb (denoteCore A) (denote R) a out := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “absorption entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem absorptionEntry_cost_le {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) (a : Fin l) (out : Fin 2 × Fin r) (op : Op) :
    (absorptionEntry A R a out).cost op ≤ m * (4 * tick .read op + 2 * tick .field op) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “absorption”.

noncomputable def absorption {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) : Run (StoredCore l r) :=
  materialize (fun a j => absorptionEntry A R a (finProdFinEquiv.symm j))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “absorption value”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem absorption_value {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) :
    denoteCore (absorption A R).value = absorb (denoteCore A) (denote R) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “absorption budget”.

def absorptionBudget (l m r : ℕ) : Cost := fun op =>
  l * (2 * r) * m * (4 * tick .read op + 2 * tick .field op) +
    (l * (2 * r) + l) * (2 * tick .read op + 2 * tick .write op)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “absorption cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem absorption_cost_le {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) (op : Op) :
    (absorption A R).cost op ≤ absorptionBudget l m r op := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “core result”. A proposition-valued field is a requirement until a constructor supplies it.

structure CoreResult {l r : ℕ} (A : StoredCore l r) where
  R : StoredMatrix l (min l (2 * r))
  Q : StoredCore (min l (2 * r)) r
  factorization : denoteCore A = denote R * denoteCore Q
  orthogonal : denoteCore Q * (denoteCore Q).transpose = 1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “factor core”.

noncomputable def factorCore {l r : ℕ} (A : StoredCore l r) : Run (CoreResult A) :=
  let result := StoredThinLQ.compile A
  ⟨{ R := result.value.R, Q := result.value.Q,
     factorization := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “result”. A proposition-valued field is a requirement until a constructor supplies it.

structure Result {n l r : ℕ} (C : StoredChain n l r) where
  rank : ℕ
  residual : StoredMatrix l rank
  canonical : StoredChain n rank r
  rightCanonical : RightCanonical (denoteChain canonical)
  rankReduced : RankReduced (denoteChain C) (denoteChain canonical)
  action : ∀ x, contract (denoteChain C) x = denote residual * contract (denoteChain canonical) x
  rank_le : rank ≤ l

/-- Read the input tag/payload and allocate the output chain node. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “node budget”. Read the input tag/payload and allocate the output chain node.

def nodeBudget : Cost := 3 • tick .read + 3 • tick .write

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “canonicalize”.

noncomputable def canonicalize : {n l r : ℕ} → (C : StoredChain n l r) → Run (Result C)
  | _, _, _, .nil r =>
      let I := StoredRectangularGivens.identity r
      ⟨{ rank := r, residual := I.value, canonical := .nil r,
         rightCanonical := trivial, rankReduced := .nil r,
         action := fun _ => by simp [denoteChain, contract, I, StoredRectangularGivens.identity_value],
         rank_le := le_rfl }, nodeBudget + I.cost⟩
  | _, l, _, .cons A C =>
      let tailResult := canonicalize C
      let absorbed := absorption A tailResult.value.residual
      let headResult := factorCore absorbed.value

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “canonicalize max bond le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem canonicalize_maxBond_le {n l r : ℕ} (C : StoredChain n l r) :
    maxBond (denoteChain (canonicalize C).value.canonical) ≤ maxBond (denoteChain C) :=
  (canonicalize C).value.rankReduced.maxBond_le

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “absorption total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem absorption_total_cost_le {l m r : ℕ} (A : StoredCore l m)
    (R : StoredMatrix m r) :
    StoredRectangularGivens.total (absorption A R).cost ≤
      12 * l * m * r + 8 * l * r + 4 * l := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “factor core total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem factorCore_total_cost_le {l r : ℕ} (A : StoredCore l r) (D : ℕ)
    (hl : l ≤ D) (hr : r ≤ D) :
    StoredRectangularGivens.total (factorCore A).cost ≤
      164 * D ^ 3 + 108 * D ^ 2 + 25 * D + 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “canonicalize total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. The actual stored producer uses linear-in-length, cubic-in-bond work in the declared exact-real model, including absorption, storage, and node costs.

theorem canonicalize_total_cost_le {n l r : ℕ} (C : StoredChain n l r) (D : ℕ)
    (bound : maxBond (denoteChain C) ≤ D) :
    StoredRectangularGivens.total (canonicalize C).cost ≤
      n * (176 * D ^ 3 + 116 * D ^ 2 + 29 * D + 8) + 5 * D ^ 2 + 4 * D + 6 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “boundary”. The output's semantic boundary is obtained from its stored residual.

noncomputable def boundary {n l r : ℕ} (C : StoredChain n l r) (v : Fin l → ℝ) :
    Fin (canonicalize C).value.rank → ℝ := _root_.Matrix.vecMul v (denote (canonicalize C).value.residual)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary mass”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundary_mass {n l r : ℕ} (C : StoredChain n l r) (v : Fin l → ℝ) :
    chainMass (denoteChain C) v = mass (boundary C v) :=
  residual_mass (denoteChain C) (denoteChain (canonicalize C).value.canonical)
    (denote (canonicalize C).value.residual) (canonicalize C).value.rightCanonical
    (canonicalize C).value.action v

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundary_normalized {n l r : ℕ} (C : StoredChain n l r) (v : Fin l → ℝ)
    (normalized : chainMass (denoteChain C) v = 1) : mass (boundary C v) = 1 :=
  (boundary_mass C v).symm.trans normalized

/-- Forget storage, retaining the actual concrete canonicalization data. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “to semantic”. Forget storage, retaining the actual concrete canonicalization data.

def Result.toSemantic {n l r : ℕ} {C : StoredChain n l r} (result : Result C) :
    ConstructiveTensorTrain.Result (denoteChain C) where
  rank := result.rank
  residual := denote result.residual
  canonical := denoteChain result.canonical
  rightCanonical := result.rightCanonical
  rankReduced := result.rankReduced
  action := result.action

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “factor core r”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem factorCore_R {l r : ℕ} (A : StoredCore l r) :
    denote (factorCore A).value.R = (ConstructiveTensorTrain.factorCore (denoteCore A)).R := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “factor core q”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem factorCore_Q {l r : ℕ} (A : StoredCore l r) :
    denoteCore (factorCore A).value.Q = (ConstructiveTensorTrain.factorCore (denoteCore A)).Q := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “canonicalize refines”; the hypotheses and conclusion in the code panel fix its exact scope. Exact data refinement, not just another witness of the same contract.

theorem canonicalize_refines {n l r : ℕ} (C : StoredChain n l r) :
    (canonicalize C).value.toSemantic = ConstructiveTensorTrain.canonicalize (denoteChain C) := by

commit-pinned source · Verso Blueprint panel