ASPBE Lean Blueprint

6.41. QuantumBlockEncoding/TensorTrainCanonical.lean🔗

33 explicit public declarations, in source order.

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

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

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/TensorTrainCanonical.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.41.1●1 definition
Definition6.41.2
uses 0used by 0✓L∃∀N

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

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/TensorTrainCanonical.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.41.2●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.slice {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (bit : Fin 2) : Matrix (Fin l) (Fin r) ℝ
    def QuantumBlockEncoding.TensorTrainCanonical.slice
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (bit : Fin 2) : Matrix (Fin l) (Fin r) ℝ
Definition6.41.3
uses 0used by 0✓L∃∀N

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

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 first core emits the first bit. The terminal bond is explicit.

Declaration kind. inductive.

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

Lean code for Definition6.41.3●1 definition
  • inductive(2 constructors, 3 parameters)defined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    inductive QuantumBlockEncoding.TensorTrainCanonical.Chain : ℕ → ℕ → ℕ → Type
    inductive QuantumBlockEncoding.TensorTrainCanonical.Chain :
  ℕ → ℕ → ℕ → Type
    The first core emits the first bit. The terminal bond is explicit.

    Constructors

    nil (r : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain 0 r r
    cons {n l m r : ℕ}
  (head :
    QuantumBlockEncoding.TensorTrainCanonical.Core l m)
  (tail :
    QuantumBlockEncoding.TensorTrainCanonical.Chain n m r) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l
    r
Definition6.41.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “word”. Bit words indexed recursively in the same order as the 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. Bit words indexed recursively in the same order as the cores.

Declaration kind. def.

Source: QuantumBlockEncoding/TensorTrainCanonical.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.41.4●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.Word : ℕ → Type
    def QuantumBlockEncoding.TensorTrainCanonical.Word :
  ℕ → Type
    Bit words indexed recursively in the same order as the cores.
Definition6.41.5
uses 0used by 0✓L∃∀N

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

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. Matrix of bond-to-bond amplitudes for one fixed emitted word.

Declaration kind. def.

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

Lean code for Definition6.41.5●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.contract {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Word n →
      Matrix (Fin l) (Fin r) ℝ
    def QuantumBlockEncoding.TensorTrainCanonical.contract
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Word
        n →
      Matrix (Fin l) (Fin r) ℝ
    Matrix of bond-to-bond amplitudes for one fixed emitted word.
Definition6.41.6
uses 0used by 0✓L∃∀N

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

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. Right-canonical means orthonormal rows at every individual core.

Declaration kind. def.

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

Lean code for Definition6.41.6●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.RightCanonical {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → Prop
    def QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    Prop
    Right-canonical means orthonormal rows at every individual core.
Definition6.41.7
uses 0used by 0✓L∃∀N

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

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 active ranks satisfy the exact backward 'min' recurrence, with an unchanged terminal bond. This is a relation on actual core chains.

Declaration kind. inductive.

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

Lean code for Definition6.41.7●1 definition
  • inductive(2 constructors, Prop, 6 parameters)defined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    inductive QuantumBlockEncoding.TensorTrainCanonical.RankReduced {n l l' r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain n l' r → Prop
    inductive QuantumBlockEncoding.TensorTrainCanonical.RankReduced
  {n l l' r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain
        n l' r →
      Prop
    The active ranks satisfy the exact backward `min` recurrence, with an
unchanged terminal bond. This is a relation on actual core chains.

    Constructors

    nil (r : ℕ) :
  QuantumBlockEncoding.TensorTrainCanonical.RankReduced
    (QuantumBlockEncoding.TensorTrainCanonical.Chain.nil r)
    (QuantumBlockEncoding.TensorTrainCanonical.Chain.nil r)
    cons {n l m r m' : ℕ}
  {A : QuantumBlockEncoding.TensorTrainCanonical.Core l m}
  {C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain n m r}
  {Q :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      (min l (2 * m')) m'}
  {D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain n m' r}
  (tail :
    QuantumBlockEncoding.TensorTrainCanonical.RankReduced C
      D) :
  QuantumBlockEncoding.TensorTrainCanonical.RankReduced
    (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons A
      C)
    (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons Q
      D)
Definition6.41.8
uses 0used by 0✓L∃∀N

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

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. Multiply a residual into the right bond without mixing the emitted bit.

Declaration kind. def.

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

Lean code for Definition6.41.8●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.absorb {l m r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l m)
  (R : Matrix (Fin m) (Fin r) ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Core l r
    def QuantumBlockEncoding.TensorTrainCanonical.absorb
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l m)
  (R : Matrix (Fin m) (Fin r) ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Core
    l r
    Multiply a residual into the right bond without mixing the emitted bit.
Theorem6.41.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorb slice”; 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/TensorTrainCanonical.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.41.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.absorb_slice {l m r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l m)
  (R : Matrix (Fin m) (Fin r) ℝ) (bit : Fin 2) :
  QuantumBlockEncoding.TensorTrainCanonical.slice
      (QuantumBlockEncoding.TensorTrainCanonical.absorb A R) bit =
    QuantumBlockEncoding.TensorTrainCanonical.slice A bit * R
    theorem QuantumBlockEncoding.TensorTrainCanonical.absorb_slice
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l m)
  (R : Matrix (Fin m) (Fin r) ℝ)
  (bit : Fin 2) :
  QuantumBlockEncoding.TensorTrainCanonical.slice
      (QuantumBlockEncoding.TensorTrainCanonical.absorb
        A R)
      bit =
    QuantumBlockEncoding.TensorTrainCanonical.slice
        A bit *
      R
Theorem6.41.10
uses 0used by 0✓L∃∀N

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

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. Thin LQ with the physical bit/right-bond product index made explicit.

Declaration kind. theorem.

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

Lean code for Theorem6.41.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_core_lq {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r) :
  ∃ R Q, A = R * Q ∧ Q * Matrix.transpose Q = 1
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_core_lq
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r) :
  ∃ R Q,
    A = R * Q ∧ Q * Matrix.transpose Q = 1
    Thin LQ with the physical bit/right-bond product index made explicit.
Theorem6.41.11
uses 0used by 0✓L∃∀N

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

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. Exact all-length right-canonicalization, preserving every amplitude. No full-rank assumption or global state-action hypothesis is used.

Declaration kind. theorem.

Source: QuantumBlockEncoding/TensorTrainCanonical.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.41.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_rightCanonical
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  ∃ l' R D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D ∧
        ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
          QuantumBlockEncoding.TensorTrainCanonical.contract C x =
            R * QuantumBlockEncoding.TensorTrainCanonical.contract D x
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_rightCanonical
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  ∃ l' R D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
        D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced
          C D ∧
        ∀
          (x :
            QuantumBlockEncoding.TensorTrainCanonical.Word
              n),
          QuantumBlockEncoding.TensorTrainCanonical.contract
              C x =
            R *
              QuantumBlockEncoding.TensorTrainCanonical.contract
                D x
    Exact all-length right-canonicalization, preserving every amplitude.
No full-rank assumption or global state-action hypothesis is used.
Theorem6.41.12
uses 0used by 0✓L∃∀N

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

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. Every nonempty canonicalized train has a left rank bounded by the original left rank and by twice its next active rank.

Declaration kind. theorem.

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

Lean code for Theorem6.41.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.head_bound
  {n l l' r : ℕ}
  {C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l r}
  {D : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l' r}
  (h : QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D) :
  l' ≤ l ∧
    ∃ m' Q tail,
      D = QuantumBlockEncoding.TensorTrainCanonical.Chain.cons Q tail ∧
        l' ≤ 2 * m'
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.head_bound
  {n l l' r : ℕ}
  {C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l r}
  {D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l' r}
  (h :
    QuantumBlockEncoding.TensorTrainCanonical.RankReduced
      C D) :
  l' ≤ l ∧
    ∃ m' Q tail,
      D =
          QuantumBlockEncoding.TensorTrainCanonical.Chain.cons
            Q tail ∧
        l' ≤ 2 * m'
    Every nonempty canonicalized train has a left rank bounded by the
original left rank and by twice its next active rank.
Theorem6.41.13
uses 0used by 0✓L∃∀N

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

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. In particular, the penultimate active bond has dimension at most two.

Declaration kind. theorem.

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

Lean code for Theorem6.41.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.last_bond_le_two
  {l l' : ℕ} {C : QuantumBlockEncoding.TensorTrainCanonical.Chain 1 l 1}
  {D : QuantumBlockEncoding.TensorTrainCanonical.Chain 1 l' 1}
  (h : QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D) :
  l' ≤ 2
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.last_bond_le_two
  {l l' : ℕ}
  {C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      1 l 1}
  {D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      1 l' 1}
  (h :
    QuantumBlockEncoding.TensorTrainCanonical.RankReduced
      C D) :
  l' ≤ 2
    In particular, the penultimate active bond has dimension at most two.
Definition6.41.14
uses 0used by 0✓L∃∀N

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

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. Squared Euclidean mass for an arbitrary finite real boundary.

Declaration kind. def.

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

Lean code for Definition6.41.14●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.mass.{u_1} {I : Type u_1}
  [Fintype I] (v : I → ℝ) : ℝ
    def QuantumBlockEncoding.TensorTrainCanonical.mass.{u_1}
  {I : Type u_1} [Fintype I] (v : I → ℝ) :
  ℝ
    Squared Euclidean mass for an arbitrary finite real boundary.
Theorem6.41.15
uses 0used by 0✓L∃∀N

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

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. An orthonormal-row matrix acts isometrically on row-vector boundaries.

Declaration kind. theorem.

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

Lean code for Theorem6.41.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.mass_vecMul.{u_1, u_2}
  {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [DecidableEq I]
  (A : Matrix I J ℝ) (hA : A * A.transpose = 1) (v : I → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.mass (Matrix.vecMul v A) =
    QuantumBlockEncoding.TensorTrainCanonical.mass v
    theorem QuantumBlockEncoding.TensorTrainCanonical.mass_vecMul.{u_1,
    u_2}
  {I : Type u_1} {J : Type u_2}
  [Fintype I] [Fintype J] [DecidableEq I]
  (A : Matrix I J ℝ)
  (hA : A * A.transpose = 1) (v : I → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.mass
      (Matrix.vecMul v A) =
    QuantumBlockEncoding.TensorTrainCanonical.mass
      v
    An orthonormal-row matrix acts isometrically on row-vector boundaries.
Definition6.41.16
uses 0used by 0✓L∃∀N

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

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. Total mass of all emitted amplitudes, including the terminal bond.

Declaration kind. def.

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

Lean code for Definition6.41.16●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.chainMass {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (v : Fin l → ℝ) : ℝ
    def QuantumBlockEncoding.TensorTrainCanonical.chainMass
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (v : Fin l → ℝ) : ℝ
    Total mass of all emitted amplitudes, including the terminal bond.
Theorem6.41.17
uses 0used by 0✓L∃∀N

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

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. Local row-isometries compose to an all-length mass-preserving state map.

Declaration kind. theorem.

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

Lean code for Theorem6.41.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.chainMass_eq {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hC : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical C)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass v
    theorem QuantumBlockEncoding.TensorTrainCanonical.chainMass_eq
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hC :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      C)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass
      C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass
      v
    Local row-isometries compose to an all-length mass-preserving state map.
Theorem6.41.18
uses 0used by 0✓L∃∀N

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

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. Factorization preserves total mass, and canonicality identifies it with the mass of the new initial boundary.

Declaration kind. theorem.

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

Lean code for Theorem6.41.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.residual_mass {n l l' r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n l' r)
  (R : Matrix (Fin l) (Fin l') ℝ)
  (hD : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D)
  (h :
    ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
      QuantumBlockEncoding.TensorTrainCanonical.contract C x =
        R * QuantumBlockEncoding.TensorTrainCanonical.contract D x)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass (Matrix.vecMul v R)
    theorem QuantumBlockEncoding.TensorTrainCanonical.residual_mass
  {n l l' r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l' r)
  (R : Matrix (Fin l) (Fin l') ℝ)
  (hD :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      D)
  (h :
    ∀
      (x :
        QuantumBlockEncoding.TensorTrainCanonical.Word
          n),
      QuantumBlockEncoding.TensorTrainCanonical.contract
          C x =
        R *
          QuantumBlockEncoding.TensorTrainCanonical.contract
            D x)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass
      C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass
      (Matrix.vecMul v R)
    Factorization preserves total mass, and canonicality identifies it with
the mass of the new initial boundary.
Theorem6.41.19
uses 0used by 0✓L∃∀N

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

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. A normalized input train has a normalized residual initial boundary. The terminal bond remains exactly dimension one.

Declaration kind. theorem.

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

Lean code for Theorem6.41.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_rightCanonical_normalized
  {n l : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l 1)
  (v : Fin l → ℝ)
  (hv : QuantumBlockEncoding.TensorTrainCanonical.chainMass C v = 1) :
  ∃ l' R D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D ∧
        (∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
            QuantumBlockEncoding.TensorTrainCanonical.contract C x =
              R *
                QuantumBlockEncoding.TensorTrainCanonical.contract D
                  x) ∧
          QuantumBlockEncoding.TensorTrainCanonical.mass
              (Matrix.vecMul v R) =
            1
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_rightCanonical_normalized
  {n l : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l 1)
  (v : Fin l → ℝ)
  (hv :
    QuantumBlockEncoding.TensorTrainCanonical.chainMass
        C v =
      1) :
  ∃ l' R D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
        D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced
          C D ∧
        (∀
            (x :
              QuantumBlockEncoding.TensorTrainCanonical.Word
                n),
            QuantumBlockEncoding.TensorTrainCanonical.contract
                C x =
              R *
                QuantumBlockEncoding.TensorTrainCanonical.contract
                  D x) ∧
          QuantumBlockEncoding.TensorTrainCanonical.mass
              (Matrix.vecMul v R) =
            1
    A normalized input train has a normalized residual initial boundary.
The terminal bond remains exactly dimension one.
Theorem6.41.20
uses 0used by 0✓L∃∀N

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

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. 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. No target-state equality is a hypothesis.

Declaration kind. theorem.

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

Lean code for Theorem6.41.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_normalized_state
  {n : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (hC :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2 =
      1) :
  ∃ l' u D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D ∧
        QuantumBlockEncoding.TensorTrainCanonical.mass u = 1 ∧
          ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
            QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 =
              ∑ a,
                u a *
                  QuantumBlockEncoding.TensorTrainCanonical.contract D x
                    a 0
    theorem QuantumBlockEncoding.TensorTrainCanonical.exists_normalized_state
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (hC :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2 =
      1) :
  ∃ l' u D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
        D ∧
      QuantumBlockEncoding.TensorTrainCanonical.RankReduced
          C D ∧
        QuantumBlockEncoding.TensorTrainCanonical.mass
              u =
            1 ∧
          ∀
            (x :
              QuantumBlockEncoding.TensorTrainCanonical.Word
                n),
            QuantumBlockEncoding.TensorTrainCanonical.contract
                C x 0 0 =
              ∑ a,
                u a *
                  QuantumBlockEncoding.TensorTrainCanonical.contract
                    D x a 0
    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. No target-state equality is a hypothesis.
Definition6.41.21
uses 0used by 0✓L∃∀N

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

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. Largest actual bond in a chain, including both boundaries.

Declaration kind. def.

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

Lean code for Definition6.41.21●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.maxBond {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → ℕ
    def QuantumBlockEncoding.TensorTrainCanonical.maxBond
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ
    Largest actual bond in a chain, including both boundaries.
Theorem6.41.22
uses 0used by 0✓L∃∀N

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

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. Backward canonicalization never enlarges any maximal bond dimension.

Declaration kind. theorem.

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

Lean code for Theorem6.41.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.maxBond_le
  {n l l' r : ℕ}
  {C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r}
  {D : QuantumBlockEncoding.TensorTrainCanonical.Chain n l' r}
  (h : QuantumBlockEncoding.TensorTrainCanonical.RankReduced C D) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond C
    theorem QuantumBlockEncoding.TensorTrainCanonical.RankReduced.maxBond_le
  {n l l' r : ℕ}
  {C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r}
  {D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l' r}
  (h :
    QuantumBlockEncoding.TensorTrainCanonical.RankReduced
      C D) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      D ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      C
    Backward canonicalization never enlarges any maximal bond dimension.
Definition6.41.23
uses 0used by 0✓L∃∀N

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

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. In circuit convention the emitted bit/new bond are output rows, and the old bond is the input column. Real amplitudes embed into complex ones.

Declaration kind. def.

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

Lean code for Definition6.41.23●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.complexCore {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r) :
  Matrix (Fin 2 × Fin r) (Fin l) ℂ
    def QuantumBlockEncoding.TensorTrainCanonical.complexCore
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r) :
  Matrix (Fin 2 × Fin r) (Fin l) ℂ
    In circuit convention the emitted bit/new bond are output rows, and
the old bond is the input column. Real amplitudes embed into complex ones.
Theorem6.41.24
uses 0used by 0✓L∃∀N

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

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. Right-canonical rows are exactly orthonormal circuit input columns.

Declaration kind. theorem.

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

Lean code for Theorem6.41.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.complexCore_isometry {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (hA : A * Matrix.transpose A = 1) :
  (QuantumBlockEncoding.TensorTrainCanonical.complexCore
          A).conjTranspose *
      QuantumBlockEncoding.TensorTrainCanonical.complexCore A =
    1
    theorem QuantumBlockEncoding.TensorTrainCanonical.complexCore_isometry
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (hA : A * Matrix.transpose A = 1) :
  (QuantumBlockEncoding.TensorTrainCanonical.complexCore
          A).conjTranspose *
      QuantumBlockEncoding.TensorTrainCanonical.complexCore
        A =
    1
    Right-canonical rows are exactly orthonormal circuit input columns.
Definition6.41.25
uses 0used by 0✓L∃∀N

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

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. Equal-rank specialization lands literally in the existing sequential preparation core type; padding varying ranks is a separate register embedding.

Declaration kind. def.

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

Lean code for Definition6.41.25●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.sequentialCore {r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core r r) :
  QuantumBlockEncoding.SequentialBondPreparation.Core (Fin r)
    def QuantumBlockEncoding.TensorTrainCanonical.sequentialCore
  {r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      r r) :
  QuantumBlockEncoding.SequentialBondPreparation.Core
    (Fin r)
    Equal-rank specialization lands literally in the existing sequential
preparation core type; padding varying ranks is a separate register embedding.
Theorem6.41.26
uses 0used by 0✓L∃∀N

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

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. Exact clean-column semantic adapter, in output-row/input-column order. This premise concerns one local stage, not the target state or full run.

Declaration kind. theorem.

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

Lean code for Theorem6.41.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.sequential_step {n r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core r r)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage (Fin r))
  (hU :
    ∀ (bit : Fin 2) (b a : Fin r),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.TensorTrainCanonical.complexCore A (bit, b)
          a)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState n (Fin r))
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : Fin r) :
  QuantumBlockEncoding.SequentialBondPreparation.step U v (x, b) =
    ∑ a, ↑(A a (x (Fin.last n), b)) * v (Fin.init x, a)
    theorem QuantumBlockEncoding.TensorTrainCanonical.sequential_step
  {n r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      r r)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      (Fin r))
  (hU :
    ∀ (bit : Fin 2) (b a : Fin r),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.TensorTrainCanonical.complexCore
          A (bit, b) a)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n (Fin r))
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : Fin r) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U v (x, b) =
    ∑ a,
      ↑(A a (x (Fin.last n), b)) *
        v (Fin.init x, 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.
Definition6.41.27
uses 0used by 0✓L∃∀N

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

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. Embed a varying active bond into a fixed physical register by zero fill.

Declaration kind. def.

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

Lean code for Definition6.41.27●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.padVector {d B : ℕ}
  (v : Fin d → ℂ) (b : Fin B) : ℂ
    def QuantumBlockEncoding.TensorTrainCanonical.padVector
  {d B : ℕ} (v : Fin d → ℂ) (b : Fin B) :
  ℂ
    Embed a varying active bond into a fixed physical register by zero fill.
Theorem6.41.28
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pad vector active”; 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/TensorTrainCanonical.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.41.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.padVector_active {d B : ℕ}
  (hd : d ≤ B) (v : Fin d → ℂ) (a : Fin d) :
  QuantumBlockEncoding.TensorTrainCanonical.padVector v
      (Fin.castLE hd a) =
    v a
    theorem QuantumBlockEncoding.TensorTrainCanonical.padVector_active
  {d B : ℕ} (hd : d ≤ B) (v : Fin d → ℂ)
  (a : Fin d) :
  QuantumBlockEncoding.TensorTrainCanonical.padVector
      v (Fin.castLE hd a) =
    v a
Definition6.41.29
uses 0used by 0✓L∃∀N

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

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. Padded matrix has zero output outside the next active rank and specifies only the active clean-input columns; other completion columns stay free.

Declaration kind. def.

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

Lean code for Definition6.41.29●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    def QuantumBlockEncoding.TensorTrainCanonical.paddedCore {l r B : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r) :
  QuantumBlockEncoding.SequentialBondPreparation.Core (Fin B)
    def QuantumBlockEncoding.TensorTrainCanonical.paddedCore
  {l r B : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r) :
  QuantumBlockEncoding.SequentialBondPreparation.Core
    (Fin B)
    Padded matrix has zero output outside the next active rank and specifies
only the active clean-input columns; other completion columns stay free.
Theorem6.41.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded core inactive output”; 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/TensorTrainCanonical.lean:260. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.41.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.paddedCore_inactive_output
  {l r B : ℕ} (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (bit : Fin 2) (b a : Fin B) (hb : r ≤ ↑b) :
  QuantumBlockEncoding.TensorTrainCanonical.paddedCore A (bit, b) a = 0
    theorem QuantumBlockEncoding.TensorTrainCanonical.paddedCore_inactive_output
  {l r B : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (bit : Fin 2) (b a : Fin B)
  (hb : r ≤ ↑b) :
  QuantumBlockEncoding.TensorTrainCanonical.paddedCore
      A (bit, b) a =
    0
Theorem6.41.31
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sum pad vector”; 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/TensorTrainCanonical.lean:264. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.41.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.sum_padVector {d B : ℕ}
  (hd : d ≤ B) (f : Fin B → ℂ) (v : Fin d → ℂ) :
  ∑ a, f a * QuantumBlockEncoding.TensorTrainCanonical.padVector v a =
    ∑ a, f (Fin.castLE hd a) * v a
    theorem QuantumBlockEncoding.TensorTrainCanonical.sum_padVector
  {d B : ℕ} (hd : d ≤ B) (f : Fin B → ℂ)
  (v : Fin d → ℂ) :
  ∑ a,
      f a *
        QuantumBlockEncoding.TensorTrainCanonical.padVector
          v a =
    ∑ a, f (Fin.castLE hd a) * v a
Theorem6.41.32
uses 0used by 0✓L∃∀N

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

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. Rank-changing local action in the existing sequential semantics. The only circuit premise is equality on active clean-input columns. The output is the zero-padded exact core contraction, including every inactive label.

Declaration kind. theorem.

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

Lean code for Theorem6.41.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.sequential_step_padded
  {n l r B : ℕ} (hl : l ≤ B)
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage (Fin B))
  (columns :
    ∀ (bit : Fin 2) (b : Fin B) (a : Fin l),
      U (bit, b) (0, Fin.castLE hl a) =
        QuantumBlockEncoding.TensorTrainCanonical.paddedCore A (bit, b)
          (Fin.castLE hl a))
  (v : QuantumBlockEncoding.PrimitiveBasis n × Fin l → ℂ)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.step U
      (fun z =>
        QuantumBlockEncoding.TensorTrainCanonical.padVector
          (fun a => v (z.1, a)) z.2)
      (x, b) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c => ∑ a, ↑(A a (x (Fin.last n), c)) * v (Fin.init x, a)) b
    theorem QuantumBlockEncoding.TensorTrainCanonical.sequential_step_padded
  {n l r B : ℕ} (hl : l ≤ B)
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      (Fin B))
  (columns :
    ∀ (bit : Fin 2) (b : Fin B)
      (a : Fin l),
      U (bit, b) (0, Fin.castLE hl a) =
        QuantumBlockEncoding.TensorTrainCanonical.paddedCore
          A (bit, b) (Fin.castLE hl a))
  (v :
    QuantumBlockEncoding.PrimitiveBasis
          n ×
        Fin l →
      ℂ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U
      (fun z =>
        QuantumBlockEncoding.TensorTrainCanonical.padVector
          (fun a => v (z.1, a)) z.2)
      (x, b) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c =>
        ∑ a,
          ↑(A a (x (Fin.last n), c)) *
            v (Fin.init x, a))
      b
    Rank-changing local action in the existing sequential semantics. The
only circuit premise is equality on active clean-input columns. The output
is the zero-padded exact core contraction, including every inactive label.
Theorem6.41.33
uses 0used by 0✓L∃∀N

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

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. Active columns of a right-canonical core remain orthonormal after embedding the output into a larger physical register.

Declaration kind. theorem.

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

Lean code for Theorem6.41.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainCanonical.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainCanonical.paddedCore_active_isometry
  {l r B : ℕ} (hl : l ≤ B) (hr : r ≤ B)
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (hA : A * Matrix.transpose A = 1) (a c : Fin l) :
  ∑ out,
      star
          (QuantumBlockEncoding.TensorTrainCanonical.paddedCore A out
            (Fin.castLE hl a)) *
        QuantumBlockEncoding.TensorTrainCanonical.paddedCore A out
          (Fin.castLE hl c) =
    if a = c then 1 else 0
    theorem QuantumBlockEncoding.TensorTrainCanonical.paddedCore_active_isometry
  {l r B : ℕ} (hl : l ≤ B) (hr : r ≤ B)
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (hA : A * Matrix.transpose A = 1)
  (a c : Fin l) :
  ∑ out,
      star
          (QuantumBlockEncoding.TensorTrainCanonical.paddedCore
            A out (Fin.castLE hl a)) *
        QuantumBlockEncoding.TensorTrainCanonical.paddedCore
          A out (Fin.castLE hl c) =
    if a = c then 1 else 0
    Active columns of a right-canonical core remain orthonormal after
embedding the output into a larger physical register.