6.11. QuantumBlockEncoding/MatrixProductChain.lean🔗

13 explicit public declarations, in source order.

Definition6.11.1

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/MatrixProductChain.lean:11. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.1●1 definition

abbrevdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

abbrev QuantumBlockEncoding.MatrixProductChain.Kernel (D : ℕ) : Type

abbrev QuantumBlockEncoding.MatrixProductChain.Kernel
  (D : ℕ) : Type

Definition6.11.2

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Chronological finite matrix contraction, read from the first emitted bit.

Declaration kind. def.

Source: QuantumBlockEncoding/MatrixProductChain.lean:14. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.2●1 definition

defdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

def QuantumBlockEncoding.MatrixProductChain.readout {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (right : Fin D → ℝ) (start : ℕ) {n : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Word n → Fin D → ℝ

def QuantumBlockEncoding.MatrixProductChain.readout
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (right : Fin D → ℝ) (start : ℕ)
  {n : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Word
      n →
    Fin D → ℝ

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

Definition6.11.3

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Absorb the terminal vector into the last core, leaving terminal rank one.

Declaration kind. def.

Source: QuantumBlockEncoding/MatrixProductChain.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.3●1 definition

defdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

def QuantumBlockEncoding.MatrixProductChain.tailChain {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) D 1

def QuantumBlockEncoding.MatrixProductChain.tailChain
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) D 1

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

Theorem6.11.4

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:26. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.4●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.tailChain_contract {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (right : Fin D → ℝ) (start n : ℕ)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1))
  (a : Fin D) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.MatrixProductChain.tailChain K right start
        n)
      x a 0 =
    QuantumBlockEncoding.MatrixProductChain.readout K right start x a

theorem QuantumBlockEncoding.MatrixProductChain.tailChain_contract
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (right : Fin D → ℝ) (start n : ℕ)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1))
  (a : Fin D) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.MatrixProductChain.tailChain
        K right start n)
      x a 0 =
    QuantumBlockEncoding.MatrixProductChain.readout
      K right start x a

Definition6.11.5

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Contract an explicit left boundary into the first core only.

Declaration kind. def.

Source: QuantumBlockEncoding/MatrixProductChain.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.5●1 definition

defdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

def QuantumBlockEncoding.MatrixProductChain.closeLeft {n D : ℕ}
  (left : Fin D → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) D 1 →
    QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.MatrixProductChain.closeLeft
  {n D : ℕ} (left : Fin D → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) D 1 →
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1

Contract an explicit left boundary into the first core only.

Theorem6.11.6

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:42. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.6●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.closeLeft_contract {n D : ℕ}
  (left : Fin D → ℝ)
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) D 1)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.MatrixProductChain.closeLeft left C) x 0 0 =
    ∑ a,
      left a *
        QuantumBlockEncoding.TensorTrainCanonical.contract C x a 0

theorem QuantumBlockEncoding.MatrixProductChain.closeLeft_contract
  {n D : ℕ} (left : Fin D → ℝ)
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) D 1)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.MatrixProductChain.closeLeft
        left C)
      x 0 0 =
    ∑ a,
      left a *
        QuantumBlockEncoding.TensorTrainCanonical.contract
          C x a 0

Definition6.11.7

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. A scalar-boundary train whose coefficients are built from small matrices.

Declaration kind. def.

Source: QuantumBlockEncoding/MatrixProductChain.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.7●1 definition

defdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

def QuantumBlockEncoding.MatrixProductChain.ofKernel {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.MatrixProductChain.ofKernel
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

A scalar-boundary train whose coefficients are built from small matrices.

Theorem6.11.8

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:55. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.8●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

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

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

Theorem6.11.9

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:62. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.9●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.tailChain_maxBond {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.MatrixProductChain.tailChain K right start
        n) ≤
    max D 1

theorem QuantumBlockEncoding.MatrixProductChain.tailChain_maxBond
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.MatrixProductChain.tailChain
        K right start n) ≤
    max D 1

Theorem6.11.10

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:68. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.10●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.ofKernel_maxBond {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.MatrixProductChain.ofKernel K left right
        start n) ≤
    max D 1

theorem QuantumBlockEncoding.MatrixProductChain.ofKernel_maxBond
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.MatrixProductChain.ofKernel
        K left right start n) ≤
    max D 1

Definition6.11.11

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Number of entries in the explicit dense *local* cores.

Declaration kind. def.

Source: QuantumBlockEncoding/MatrixProductChain.lean:75. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.11.11●1 definition

defdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

def QuantumBlockEncoding.MatrixProductChain.storedScalars {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → ℕ

def QuantumBlockEncoding.MatrixProductChain.storedScalars
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ

Number of entries in the explicit dense *local* cores.

Theorem6.11.12

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:79. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.12●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.storedScalars_le {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (D : ℕ)
  (h : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ D) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars C ≤
    2 * n * D ^ 2

theorem QuantumBlockEncoding.MatrixProductChain.storedScalars_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (D : ℕ)
  (h :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      D) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      C ≤
    2 * n * D ^ 2

Theorem6.11.13

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/MatrixProductChain.lean:95. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.13●1 theorem

theoremdefined in QuantumBlockEncoding/MatrixProductChain.lean

complete

theorem QuantumBlockEncoding.MatrixProductChain.ofKernel_storedScalars {D : ℕ}
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.MatrixProductChain.ofKernel K left right
        start n) ≤
    2 * (n + 1) * max D 1 ^ 2

theorem QuantumBlockEncoding.MatrixProductChain.ofKernel_storedScalars
  {D : ℕ}
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (left right : Fin D → ℝ) (start n : ℕ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.MatrixProductChain.ofKernel
        K left right start n) ≤
    2 * (n + 1) * max D 1 ^ 2