ASPBE Lean Blueprint

6.34. QuantumBlockEncoding/StoredMatrixProductChain.lean🔗

29 explicit public declarations, in source order.

Definition6.34.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “terminal entry”.

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. def.

Source: QuantumBlockEncoding/StoredMatrixProductChain.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.34.1●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry {D : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) (a : Fin D) (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D) (a : Fin D)
  (bit : Fin 2) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
Definition6.34.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “terminal”.

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. def.

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

Lean code for Definition6.34.2●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.terminal {D : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore D 1)
    def QuantumBlockEncoding.StoredMatrixProductChain.terminal
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D 1)
Definition6.34.3
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “initial entry”.

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. def.

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

Lean code for Definition6.34.3●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.initialEntry {D r : ℕ}
  (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r)
  (j : Fin (2 * r)) : QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredMatrixProductChain.initialEntry
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r)
  (j : Fin (2 * r)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
Definition6.34.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “initial”.

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. def.

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

Lean code for Definition6.34.4●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.initial {D r : ℕ}
  (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore 1 r)
    def QuantumBlockEncoding.StoredMatrixProductChain.initial
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore
      1 r)
Definition6.34.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tail table”. Copy only references to already materialized local cores.

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. Copy only references to already materialized local cores.

Declaration kind. def.

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

Lean code for Definition6.34.5●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.tailTable {α : Type}
  {n : ℕ} (xs : Vector α (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run (Vector α n)
    def QuantumBlockEncoding.StoredMatrixProductChain.tailTable
  {α : Type} {n : ℕ}
  (xs : Vector α (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector α n)
    Copy only references to already materialized local cores.
Definition6.34.6
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tail chain”.

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. def.

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

Lean code for Definition6.34.6●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.tailChain {D n : ℕ} :
  Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1) →
    Vector ℝ D →
      QuantumBlockEncoding.StoredGivens.Run
        (QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) D 1)
    def QuantumBlockEncoding.StoredMatrixProductChain.tailChain
  {D n : ℕ} :
  Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1) →
    Vector ℝ D →
      QuantumBlockEncoding.StoredGivens.Run
        (QuantumBlockEncoding.StoredTensorTrain.StoredChain
          (n + 1) D 1)
Definition6.34.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “close left”.

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. def.

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

Lean code for Definition6.34.7●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.closeLeft {n D : ℕ}
  (left : Vector ℝ D) :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) D 1 →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) 1 1)
    def QuantumBlockEncoding.StoredMatrixProductChain.closeLeft
  {n D : ℕ} (left : Vector ℝ D) :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain
      (n + 1) D 1 →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredTensorTrain.StoredChain
        (n + 1) 1 1)
Definition6.34.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “of table”.

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. def.

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

Lean code for Definition6.34.8●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.ofTable {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) 1 1)
    def QuantumBlockEncoding.StoredMatrixProductChain.ofTable
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredChain
      (n + 1) 1 1)
Theorem6.34.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal value”; 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.

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. theorem.

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

Lean code for Theorem6.34.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_value {D : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredMatrixProductChain.terminal A
          right).value =
    fun a out =>
    ∑ b,
      QuantumBlockEncoding.StoredTensorTrain.denoteCore A a (out.1, b) *
        right[↑b]
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_value
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredMatrixProductChain.terminal
          A right).value =
    fun a out =>
    ∑ b,
      QuantumBlockEncoding.StoredTensorTrain.denoteCore
          A a (out.1, b) *
        right[↑b]
Theorem6.34.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial value”; 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.

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. theorem.

Source: QuantumBlockEncoding/StoredMatrixProductChain.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.34.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_value {D r : ℕ}
  (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredMatrixProductChain.initial left
          A).value =
    fun x out =>
    ∑ a,
      left[↑a] *
        QuantumBlockEncoding.StoredTensorTrain.denoteCore A a out
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_value
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredMatrixProductChain.initial
          left A).value =
    fun x out =>
    ∑ a,
      left[↑a] *
        QuantumBlockEncoding.StoredTensorTrain.denoteCore
          A a out
Theorem6.34.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail table value”; 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.

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. theorem.

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

Lean code for Theorem6.34.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_value {α : Type}
  {n : ℕ} (xs : Vector α (n + 1)) (i : Fin n) :
  (QuantumBlockEncoding.StoredMatrixProductChain.tailTable
          xs).value[↑i] =
    xs[↑i.succ]
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_value
  {α : Type} {n : ℕ}
  (xs : Vector α (n + 1)) (i : Fin n) :
  (QuantumBlockEncoding.StoredMatrixProductChain.tailTable
          xs).value[↑i] =
    xs[↑i.succ]
Definition6.34.12
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “window”. Kernel appears only in this finite-window specification, never production.

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. Kernel appears only in this finite-window specification, never production.

Declaration kind. def.

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

Lean code for Definition6.34.12●1 definition
  • defdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    def QuantumBlockEncoding.StoredMatrixProductChain.Window {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ) :
  Prop
    def QuantumBlockEncoding.StoredMatrixProductChain.Window
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ) : Prop
    Kernel appears only in this finite-window specification, never production.
Theorem6.34.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail chain value”; 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.

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. theorem.

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

Lean code for Theorem6.34.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailChain_value {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (right : Vector ℝ D)
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window tables K
      start) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.tailChain tables
          right).value =
    QuantumBlockEncoding.MatrixProductChain.tailChain K
      (fun i => right[↑i]) start n
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailChain_value
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (right : Vector ℝ D)
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window
      tables K start) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.tailChain
          tables right).value =
    QuantumBlockEncoding.MatrixProductChain.tailChain
      K (fun i => right[↑i]) start n
Theorem6.34.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “close left value”; 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.

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. theorem.

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

Lean code for Theorem6.34.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.closeLeft_value {n D : ℕ}
  (left : Vector ℝ D)
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1) D 1) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.closeLeft left
          C).value =
    QuantumBlockEncoding.MatrixProductChain.closeLeft
      (fun i => left[↑i])
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.closeLeft_value
  {n D : ℕ} (left : Vector ℝ D)
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      (n + 1) D 1) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.closeLeft
          left C).value =
    QuantumBlockEncoding.MatrixProductChain.closeLeft
      (fun i => left[↑i])
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        C)
Theorem6.34.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “of table refines”; 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.

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. theorem.

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

Lean code for Theorem6.34.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_refines {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window tables K
      start) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.ofTable tables left
          right).value =
    QuantumBlockEncoding.MatrixProductChain.ofKernel K
      (fun i => left[↑i]) (fun i => right[↑i]) start n
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_refines
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window
      tables K start) :
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
      (QuantumBlockEncoding.StoredMatrixProductChain.ofTable
          tables left right).value =
    QuantumBlockEncoding.MatrixProductChain.ofKernel
      K (fun i => left[↑i])
      (fun i => right[↑i]) start n
Theorem6.34.16
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal entry cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry_cost {D : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) (a : Fin D) (bit : Fin 2)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry A right a
          bit).cost
      op =
    D *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry_cost
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D) (a : Fin D)
  (bit : Fin 2)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.terminalEntry
          A right a bit).cost
      op =
    D *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op)
Theorem6.34.17
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial entry cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initialEntry_cost
  {D r : ℕ} (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r)
  (j : Fin (2 * r)) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.initialEntry left A
          j).cost
      op =
    D *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initialEntry_cost
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r)
  (j : Fin (2 * r))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.initialEntry
          left A j).cost
      op =
    D *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op)
Theorem6.34.18
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_cost {D : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.terminal A right).cost
      op =
    2 * D ^ 2 *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field op) +
      6 * D *
        (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_cost
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.terminal
          A right).cost
      op =
    2 * D ^ 2 *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field
              op) +
      6 * D *
        (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Theorem6.34.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_cost {D r : ℕ}
  (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.initial left A).cost
      op =
    2 * r * D *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field op) +
      (4 * r + 2) *
        (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_cost
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.initial
          left A).cost
      op =
    2 * r * D *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field
              op) +
      (4 * r + 2) *
        (QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Theorem6.34.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail table cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_cost {α : Type}
  {n : ℕ} (xs : Vector α (n + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.tailTable xs).cost op =
    n *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_cost
  {α : Type} {n : ℕ}
  (xs : Vector α (n + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredMatrixProductChain.tailTable
          xs).cost
      op =
    n *
      (3 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)
Theorem6.34.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal total cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_total_cost
  {D : ℕ} (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.terminal A
          right).cost =
    10 * D ^ 2 + 12 * D
    theorem QuantumBlockEncoding.StoredMatrixProductChain.terminal_total_cost
  {D : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D D)
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.terminal
          A right).cost =
    10 * D ^ 2 + 12 * D
Theorem6.34.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial total cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_total_cost
  {D r : ℕ} (left : Vector ℝ D)
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore D r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.initial left
          A).cost =
    10 * r * D + 8 * r + 4
    theorem QuantumBlockEncoding.StoredMatrixProductChain.initial_total_cost
  {D r : ℕ} (left : Vector ℝ D)
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      D r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.initial
          left A).cost =
    10 * r * D + 8 * r + 4
Theorem6.34.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail table total cost”; 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.

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. theorem.

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

Lean code for Theorem6.34.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_total_cost
  {α : Type} {n : ℕ} (xs : Vector α (n + 1)) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.tailTable
          xs).cost =
    5 * n
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailTable_total_cost
  {α : Type} {n : ℕ}
  (xs : Vector α (n + 1)) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.tailTable
          xs).cost =
    5 * n
Theorem6.34.24
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail chain total cost 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.

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. theorem.

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

Lean code for Theorem6.34.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailChain_total_cost_le
  {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.tailChain tables
          right).cost ≤
    10 * D ^ 2 + 12 * D + 5 * n ^ 2 + 7 * n + 13
    theorem QuantumBlockEncoding.StoredMatrixProductChain.tailChain_total_cost_le
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.tailChain
          tables right).cost ≤
    10 * D ^ 2 + 12 * D + 5 * n ^ 2 +
        7 * n +
      13
Theorem6.34.25
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “close left tail total cost 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.

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. theorem.

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

Lean code for Theorem6.34.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.closeLeft_tail_total_cost_le
  {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.closeLeft left
          (QuantumBlockEncoding.StoredMatrixProductChain.tailChain
              tables right).value).cost ≤
    10 * D ^ 2 + 18 * D + 18
    theorem QuantumBlockEncoding.StoredMatrixProductChain.closeLeft_tail_total_cost_le
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.closeLeft
          left
          (QuantumBlockEncoding.StoredMatrixProductChain.tailChain
              tables right).value).cost ≤
    10 * D ^ 2 + 18 * D + 18
Theorem6.34.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “of table total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Bound for the very same run whose value refines 'ofKernel'; includes terminal/initial arithmetic, materialization, copied references, and nodes.

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

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. Bound for the very same run whose value refines 'ofKernel'; includes terminal/initial arithmetic, materialization, copied references, and nodes.

Declaration kind. theorem.

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

Lean code for Theorem6.34.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_total_cost_le
  {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.ofTable tables left
          right).cost ≤
    20 * D ^ 2 + 30 * D + 5 * n ^ 2 + 7 * n + 31
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_total_cost_le
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredMatrixProductChain.ofTable
          tables left right).cost ≤
    20 * D ^ 2 + 30 * D + 5 * n ^ 2 +
        7 * n +
      31
    Bound for the very same run whose value refines `ofKernel`; includes
terminal/initial arithmetic, materialization, copied references, and nodes.
Theorem6.34.27
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “window of entries”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise supplier adapter; only the stored finite window is constrained.

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

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. Entrywise supplier adapter; only the stored finite window is constrained.

Declaration kind. theorem.

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

Lean code for Theorem6.34.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.window_of_entries
  {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ)
  (h :
    ∀ (i : Fin (n + 1)) (a b : Fin D) (bit : Fin 2),
      QuantumBlockEncoding.StoredTensorTrain.denoteCore tables[↑i] a
          (bit, b) =
        K (start + ↑i) bit a b) :
  QuantumBlockEncoding.StoredMatrixProductChain.Window tables K start
    theorem QuantumBlockEncoding.StoredMatrixProductChain.window_of_entries
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ)
  (h :
    ∀ (i : Fin (n + 1)) (a b : Fin D)
      (bit : Fin 2),
      QuantumBlockEncoding.StoredTensorTrain.denoteCore
          tables[↑i] a (bit, b) =
        K (start + ↑i) bit a b) :
  QuantumBlockEncoding.StoredMatrixProductChain.Window
    tables K start
    Entrywise supplier adapter; only the stored finite window is constrained.
Theorem6.34.28
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “of table 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.

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. theorem.

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

Lean code for Theorem6.34.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_maxBond {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window tables K
      start) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredMatrixProductChain.ofTable tables
            left right).value) ≤
    max D 1
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_maxBond
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window
      tables K start) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredMatrixProductChain.ofTable
            tables left right).value) ≤
    max D 1
Theorem6.34.29
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “of table certified”; the hypotheses and conclusion in the code panel fix its exact scope. One producer, with both exact returned data and polynomial charged work.

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

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. One producer, with both exact returned data and polynomial charged work.

Declaration kind. theorem.

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

Lean code for Theorem6.34.29●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredMatrixProductChain.lean
    complete
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_certified
  {n D : ℕ}
  (tables :
    Vector (QuantumBlockEncoding.StoredTensorTrain.StoredCore D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K : QuantumBlockEncoding.MatrixProductChain.Kernel D) (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window tables K
      start) :
  have result :=
    QuantumBlockEncoding.StoredMatrixProductChain.ofTable tables left
      right;
  QuantumBlockEncoding.StoredTensorTrain.denoteChain result.value =
      QuantumBlockEncoding.MatrixProductChain.ofKernel K
        (fun i => left[↑i]) (fun i => right[↑i]) start n ∧
    QuantumBlockEncoding.StoredRectangularGivens.total result.cost ≤
      20 * D ^ 2 + 30 * D + 5 * n ^ 2 + 7 * n + 31
    theorem QuantumBlockEncoding.StoredMatrixProductChain.ofTable_certified
  {n D : ℕ}
  (tables :
    Vector
      (QuantumBlockEncoding.StoredTensorTrain.StoredCore
        D D)
      (n + 1))
  (left right : Vector ℝ D)
  (K :
    QuantumBlockEncoding.MatrixProductChain.Kernel
      D)
  (start : ℕ)
  (h :
    QuantumBlockEncoding.StoredMatrixProductChain.Window
      tables K start) :
  have result :=
    QuantumBlockEncoding.StoredMatrixProductChain.ofTable
      tables left right;
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
        result.value =
      QuantumBlockEncoding.MatrixProductChain.ofKernel
        K (fun i => left[↑i])
        (fun i => right[↑i]) start n ∧
    QuantumBlockEncoding.StoredRectangularGivens.total
        result.cost ≤
      20 * D ^ 2 + 30 * D + 5 * n ^ 2 +
          7 * n +
        31
    One producer, with both exact returned data and polynomial charged work.