QuantumBlockEncoding/TensorTrainCanonical.lean

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

abbrev Core (l r : ℕ) := _root_.Matrix (Fin l) (Fin 2 × Fin r) ℝ

commit-pinned source · Verso Blueprint panel

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

def slice {l r : ℕ} (A : Core l r) (bit : Fin 2) :
    _root_.Matrix (Fin l) (Fin r) ℝ := fun a b => A a (bit, b)

/-- The first core emits the first bit. The terminal bond is explicit. -/

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “chain”; its constructors are the cases that downstream code must handle. The first core emits the first bit.

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

/-- Bit words indexed recursively in the same order as the cores. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “word”. Bit words indexed recursively in the same order as the cores.

def Word : ℕ → Type
  | 0 => Unit
  | n + 1 => Fin 2 × Word n

instance wordFintype (n : ℕ) : Fintype (Word n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “contract”. Matrix of bond-to-bond amplitudes for one fixed emitted word.

noncomputable def contract : {n l r : ℕ} → Chain n l r → Word n →
    _root_.Matrix (Fin l) (Fin r) ℝ
  | _, _, _, .nil _, _ => 1
  | _, _, _, .cons A C, x => slice A x.1 * contract C x.2

/-- Right-canonical means orthonormal rows at every individual core. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right canonical”. Right-canonical means orthonormal rows at every individual core.

def RightCanonical : {n l r : ℕ} → Chain n l r → Prop
  | _, _, _, .nil _ => True
  | _, _, _, .cons A C => A * A.transpose = 1 ∧ RightCanonical C

/-- The active ranks satisfy the exact backward `min` recurrence, with an
unchanged terminal bond. This is a relation on actual core chains. -/

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “rank reduced”; its constructors are the cases that downstream code must handle. The active ranks satisfy the exact backward 'min' recurrence, with an unchanged terminal bond.

inductive RankReduced : {n l l' r : ℕ} → Chain n l r → Chain n l' r → Prop
  | nil (r : ℕ) : RankReduced (.nil r) (.nil r)
  | cons {n l m r m' : ℕ} {A : Core l m} {C : Chain n m r}
      {Q : Core (min l (2 * m')) m'} {D : Chain n m' r}
      (tail : RankReduced C D) : RankReduced (.cons A C) (.cons Q D)

/-- Multiply a residual into the right bond without mixing the emitted bit. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “absorb”. Multiply a residual into the right bond without mixing the emitted bit.

noncomputable def absorb {l m r : ℕ} (A : Core l m)
    (R : _root_.Matrix (Fin m) (Fin r) ℝ) : Core l r :=
  fun a x => ∑ b, A a (x.1, b) * R b x.2

commit-pinned source · Verso Blueprint panel

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

theorem absorb_slice {l m r : ℕ} (A : Core l m)
    (R : _root_.Matrix (Fin m) (Fin r) ℝ) (bit : Fin 2) :
    slice (absorb A R) bit = slice A bit * R := rfl

/-- Thin LQ with the physical bit/right-bond product index made explicit. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists core lq”; the hypotheses and conclusion in the code panel fix its exact scope. Thin LQ with the physical bit/right-bond product index made explicit.

theorem exists_core_lq {l r : ℕ} (A : Core l r) :
    ∃ (R : _root_.Matrix (Fin l) (Fin (min l (2 * r))) ℝ)
      (Q : Core (min l (2 * r)) r), A = R * Q ∧ Q * Q.transpose = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists right canonical”; the hypotheses and conclusion in the code panel fix its exact scope. Exact all-length right-canonicalization, preserving every amplitude.

theorem exists_rightCanonical {n l r : ℕ} (C : Chain n l r) :
    ∃ (l' : ℕ) (R : _root_.Matrix (Fin l) (Fin l') ℝ) (D : Chain n l' r),
      RightCanonical D ∧ RankReduced C D ∧ ∀ x, contract C x = R * contract D x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “head bound”; the hypotheses and conclusion in the code panel fix its exact scope. Every nonempty canonicalized train has a left rank bounded by the original left rank and by twice its next active rank.

theorem RankReduced.head_bound {n l l' r : ℕ} {C : Chain (n + 1) l r}
    {D : Chain (n + 1) l' r} (h : RankReduced C D) :
    l' ≤ l ∧ ∃ m', ∃ (Q : Core l' m') (tail : Chain n m' r),
      D = .cons Q tail ∧ l' ≤ 2 * m' := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “last bond le two”; the hypotheses and conclusion in the code panel fix its exact scope. In particular, the penultimate active bond has dimension at most two.

theorem RankReduced.last_bond_le_two {l l' : ℕ} {C : Chain 1 l 1}
    {D : Chain 1 l' 1} (h : RankReduced C D) : l' ≤ 2 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mass”. Squared Euclidean mass for an arbitrary finite real boundary.

noncomputable def mass {I : Type*} [Fintype I] (v : I → ℝ) : ℝ := ∑ i, v i ^ 2

/-- An orthonormal-row matrix acts isometrically on row-vector boundaries. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mass vec mul”; the hypotheses and conclusion in the code panel fix its exact scope. An orthonormal-row matrix acts isometrically on row-vector boundaries.

theorem mass_vecMul {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I]
    (A : _root_.Matrix I J ℝ) (hA : A * A.transpose = 1) (v : I → ℝ) :
    mass (_root_.Matrix.vecMul v A) = mass v := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “chain mass”. Total mass of all emitted amplitudes, including the terminal bond.

noncomputable def chainMass {n l r : ℕ} (C : Chain n l r) (v : Fin l → ℝ) : ℝ :=
  ∑ x : Word n, mass (_root_.Matrix.vecMul v (contract C x))

/-- Local row-isometries compose to an all-length mass-preserving state map. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “chain mass eq”; the hypotheses and conclusion in the code panel fix its exact scope. Local row-isometries compose to an all-length mass-preserving state map.

theorem chainMass_eq {n l r : ℕ} (C : Chain n l r) (hC : RightCanonical C)
    (v : Fin l → ℝ) : chainMass C v = mass v := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “residual mass”; the hypotheses and conclusion in the code panel fix its exact scope. Factorization preserves total mass, and canonicality identifies it with the mass of the new initial boundary.

theorem residual_mass {n l l' r : ℕ} (C : Chain n l r) (D : Chain n l' r)
    (R : _root_.Matrix (Fin l) (Fin l') ℝ) (hD : RightCanonical D)
    (h : ∀ x, contract C x = R * contract D x) (v : Fin l → ℝ) :
    chainMass C v = mass (_root_.Matrix.vecMul v R) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists right canonical normalized”; the hypotheses and conclusion in the code panel fix its exact scope. A normalized input train has a normalized residual initial boundary.

theorem exists_rightCanonical_normalized {n l : ℕ} (C : Chain n l 1)
    (v : Fin l → ℝ) (hv : chainMass C v = 1) :
    ∃ (l' : ℕ) (R : _root_.Matrix (Fin l) (Fin l') ℝ) (D : Chain n l' 1),
      RightCanonical D ∧ RankReduced C D ∧
      (∀ x, contract C x = R * contract D x) ∧ mass (_root_.Matrix.vecMul v R) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists normalized state”; the hypotheses and conclusion in the code panel fix its exact scope. Scalar-boundary state version: the new initial vector is normalized and every individual target amplitude is recovered by contracting it with the right-canonical train.

theorem exists_normalized_state {n : ℕ} (C : Chain n 1 1)
    (hC : (∑ x : Word n, (contract C x 0 0) ^ 2) = 1) :
    ∃ (l' : ℕ) (u : Fin l' → ℝ) (D : Chain n l' 1),
      RightCanonical D ∧ RankReduced C D ∧ mass u = 1 ∧
      ∀ x, contract C x 0 0 = ∑ a, u a * contract D x a 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “max bond”. Largest actual bond in a chain, including both boundaries.

def maxBond : {n l r : ℕ} → Chain n l r → ℕ
  | _, _, _, .nil r => r
  | _, l, _, .cons _ C => max l (maxBond C)

/-- Backward canonicalization never enlarges any maximal bond dimension. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “max bond le”; the hypotheses and conclusion in the code panel fix its exact scope. Backward canonicalization never enlarges any maximal bond dimension.

theorem RankReduced.maxBond_le {n l l' r : ℕ} {C : Chain n l r}
    {D : Chain n l' r} (h : RankReduced C D) : maxBond D ≤ maxBond C := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “complex core”. In circuit convention the emitted bit/new bond are output rows, and the old bond is the input column.

def complexCore {l r : ℕ} (A : Core l r) :
    _root_.Matrix (Fin 2 × Fin r) (Fin l) ℂ := fun out a => (A a out : ℂ)

/-- Right-canonical rows are exactly orthonormal circuit input columns. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “complex core isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Right-canonical rows are exactly orthonormal circuit input columns.

theorem complexCore_isometry {l r : ℕ} (A : Core l r)
    (hA : A * A.transpose = 1) :
    (complexCore A).conjTranspose * complexCore A = 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sequential core”. Equal-rank specialization lands literally in the existing sequential preparation core type; padding varying ranks is a separate register embedding.

def sequentialCore {r : ℕ} (A : Core r r) : SequentialBondPreparation.Core (Fin r) :=
  complexCore A

/-- Exact clean-column semantic adapter, in output-row/input-column order.
This premise concerns one local stage, not the target state or full run. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sequential step”; the hypotheses and conclusion in the code panel fix its exact scope. Exact clean-column semantic adapter, in output-row/input-column order.

theorem sequential_step {n r : ℕ} (A : Core r r)
    (U : SequentialBondPreparation.Stage (Fin r))
    (hU : ∀ bit b a, U (bit, b) (0, a) = complexCore A (bit, b) a)
    (v : SequentialBondPreparation.BondState n (Fin r))
    (x : PrimitiveBasis (n + 1)) (b : Fin r) :
    SequentialBondPreparation.step U v (x, b) =
      ∑ a, (A a (x (Fin.last n), b) : ℂ) * v (Fin.init x, a) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “pad vector”. Embed a varying active bond into a fixed physical register by zero fill.

def padVector {d B : ℕ} (v : Fin d → ℂ) (b : Fin B) : ℂ :=
  if h : b.val < d then v ⟨b.val, h⟩ else 0

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem padVector_active {d B : ℕ} (hd : d ≤ B) (v : Fin d → ℂ)
    (a : Fin d) : padVector v (Fin.castLE hd a) = v a := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “padded core”. Padded matrix has zero output outside the next active rank and specifies only the active clean-input columns; other completion columns stay free.

def paddedCore {l r B : ℕ} (A : Core l r) : SequentialBondPreparation.Core (Fin B) :=
  fun out a => if ha : a.val < l then
    if hb : out.2.val < r then (A ⟨a.val, ha⟩ (out.1, ⟨out.2.val, hb⟩) : ℂ) else 0
    else 0

commit-pinned source · Verso Blueprint panel

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

theorem paddedCore_inactive_output {l r B : ℕ} (A : Core l r)
    (bit : Fin 2) (b a : Fin B) (hb : r ≤ b.val) : paddedCore A (bit, b) a = 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem sum_padVector {d B : ℕ} (hd : d ≤ B) (f : Fin B → ℂ) (v : Fin d → ℂ) :
    (∑ a : Fin B, f a * padVector v a) =
      ∑ a : Fin d, f (Fin.castLE hd a) * v a := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sequential step padded”; the hypotheses and conclusion in the code panel fix its exact scope. Rank-changing local action in the existing sequential semantics.

theorem sequential_step_padded {n l r B : ℕ} (hl : l ≤ B) (A : Core l r)
    (U : SequentialBondPreparation.Stage (Fin B))
    (columns : ∀ bit b (a : Fin l),
      U (bit, b) (0, Fin.castLE hl a) = paddedCore A (bit, b) (Fin.castLE hl a))
    (v : PrimitiveBasis n × Fin l → ℂ) (x : PrimitiveBasis (n + 1)) (b : Fin B) :
    SequentialBondPreparation.step U
      (fun z => padVector (fun a => v (z.1, a)) z.2) (x, b) =
      padVector (fun c : Fin r =>
        ∑ a : Fin l, (A a (x (Fin.last n), c) : ℂ) * v (Fin.init x, a)) b := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “padded core active isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Active columns of a right-canonical core remain orthonormal after embedding the output into a larger physical register.

theorem paddedCore_active_isometry {l r B : ℕ} (hl : l ≤ B) (hr : r ≤ B)
    (A : Core l r) (hA : A * A.transpose = 1) (a c : Fin l) :
    (∑ out : Fin 2 × Fin B,
      star (paddedCore A out (Fin.castLE hl a)) *
        paddedCore A out (Fin.castLE hl c)) = if a = c then 1 else 0 := by

commit-pinned source · Verso Blueprint panel