QuantumBlockEncoding/MatrixProductChain.lean

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

abbrev Kernel (D : Nat) := Nat → Fin 2 → _root_.Matrix (Fin D) (Fin D) ℝ

/-- Chronological finite matrix contraction, read from the first emitted bit. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “readout”. Chronological finite matrix contraction, read from the first emitted bit.

noncomputable def readout {D : Nat} (K : Kernel D) (right : Fin D → ℝ)
    (start : Nat) : {n : Nat} → Word n → Fin D → ℝ
  | 0, _ => right
  | _ + 1, x => (K start x.1).mulVec (readout K right (start + 1) x.2)

/-- Absorb the terminal vector into the last core, leaving terminal rank one. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tail chain”. Absorb the terminal vector into the last core, leaving terminal rank one.

noncomputable def tailChain {D : Nat} (K : Kernel D) (right : Fin D → ℝ)
    (start : Nat) : (n : Nat) → Chain (n + 1) D 1
  | 0 => .cons (fun a out => (K start out.1).mulVec right a) (.nil 1)
  | n + 1 => .cons (fun a out => K start out.1 a out.2)
      (tailChain K right (start + 1) n)

commit-pinned source · Verso Blueprint panel

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

theorem tailChain_contract {D : Nat} (K : Kernel D) (right : Fin D → ℝ)
    (start n : Nat) (x : Word (n + 1)) (a : Fin D) :
    contract (tailChain K right start n) x a 0 = readout K right start x a := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “close left”. Contract an explicit left boundary into the first core only.

noncomputable def closeLeft {n D : Nat} (left : Fin D → ℝ) :
    Chain (n + 1) D 1 → Chain (n + 1) 1 1
  | .cons A C => .cons (fun _ out => ∑ a, left a * A a out) C

commit-pinned source · Verso Blueprint panel

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

theorem closeLeft_contract {n D : Nat} (left : Fin D → ℝ)
    (C : Chain (n + 1) D 1) (x : Word (n + 1)) :
    contract (closeLeft left C) x 0 0 = ∑ a, left a * contract C x a 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “of kernel”. A scalar-boundary train whose coefficients are built from small matrices.

noncomputable def ofKernel {D : Nat} (K : Kernel D) (left right : Fin D → ℝ)
    (start n : Nat) : Chain (n + 1) 1 1 := closeLeft left (tailChain K right start n)

commit-pinned source · Verso Blueprint panel

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

theorem ofKernel_contract {D : Nat} (K : Kernel D) (left right : Fin D → ℝ)
    (start n : Nat) (x : Word (n + 1)) :
    contract (ofKernel K left right start n) x 0 0 =
      ∑ a, left a * readout K right start x a := by

commit-pinned source · Verso Blueprint panel

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

theorem tailChain_maxBond {D : Nat} (K : Kernel D) (right : Fin D → ℝ)
    (start n : Nat) : maxBond (tailChain K right start n) ≤ max D 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem ofKernel_maxBond {D : Nat} (K : Kernel D) (left right : Fin D → ℝ)
    (start n : Nat) : maxBond (ofKernel K left right start n) ≤ max D 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “stored scalars”. Number of entries in the explicit dense *local* cores.

def storedScalars : {n l r : Nat} → Chain n l r → Nat
  | _, _, _, .nil _ => 0
  | _, l, _, @Chain.cons _ _ m _ _ C => 2 * l * m + storedScalars C

commit-pinned source · Verso Blueprint panel

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

theorem storedScalars_le {n l r : Nat} (C : Chain n l r) (D : Nat)
    (h : maxBond C ≤ D) : storedScalars C ≤ 2 * n * D ^ 2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “of kernel stored scalars”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem ofKernel_storedScalars {D : Nat} (K : Kernel D) (left right : Fin D → ℝ)
    (start n : Nat) : storedScalars (ofKernel K left right start n) ≤
      2 * (n + 1) * (max D 1) ^ 2 :=
  storedScalars_le _ _ (ofKernel_maxBond K left right start n)

commit-pinned source · Verso Blueprint panel