ASPBE Lean Blueprint

6.45. QuantumBlockEncoding/TensorTrainSchedule.lean🔗

15 explicit public declarations, in source order.

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

Plain-English reading. This definition gives the library's named construction or computation for “word of basis”. Convert increasing-wire basis labels to the head-first chain 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. Convert increasing-wire basis labels to the head-first chain word.

Declaration kind. def.

Source: QuantumBlockEncoding/TensorTrainSchedule.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.45.1●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    def QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis {n : ℕ} :
  QuantumBlockEncoding.PrimitiveBasis n →
    QuantumBlockEncoding.TensorTrainCanonical.Word n
    def QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
  {n : ℕ} :
  QuantumBlockEncoding.PrimitiveBasis n →
    QuantumBlockEncoding.TensorTrainCanonical.Word
      n
    Convert increasing-wire basis labels to the head-first chain word.
Definition6.45.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “rank at”. Active rank before stage 't'; after the chain it is the terminal rank.

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. Active rank before stage 't'; after the chain it is the terminal rank.

Declaration kind. def.

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

Lean code for Definition6.45.2●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    def QuantumBlockEncoding.TensorTrainSchedule.rankAt {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r → ℕ → ℕ
    def QuantumBlockEncoding.TensorTrainSchedule.rankAt
  {n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ → ℕ
    Active rank before stage `t`; after the chain it is the terminal rank.
Theorem6.45.3
uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.45.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_zero {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt C 0 = l
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_zero
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt
      C 0 =
    l
Theorem6.45.4
uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.45.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_length {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt C n = r
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_length
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt
      C n =
    r
Definition6.45.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “padded at”. The finite schedule, zero after the final 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 finite schedule, zero after the final core. Later stages are never used by the bounded run theorem.

Declaration kind. def.

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

Lean code for Definition6.45.5●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    def QuantumBlockEncoding.TensorTrainSchedule.paddedAt {B n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain n l r →
    ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core (Fin B)
    def QuantumBlockEncoding.TensorTrainSchedule.paddedAt
  {B n l r : ℕ} :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r →
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        (Fin B)
    The finite schedule, zero after the final core. Later stages are never
used by the bounded run theorem.
Theorem6.45.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “rank at le 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/TensorTrainSchedule.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.45.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_le_maxBond {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (t : ℕ) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt C t ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond C
    theorem QuantumBlockEncoding.TensorTrainSchedule.rankAt_le_maxBond
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (t : ℕ) :
  QuantumBlockEncoding.TensorTrainSchedule.rankAt
      C t ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      C
Theorem6.45.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded at supported”; the hypotheses and conclusion in the code panel fix its exact scope. Zero amplitude outside the next actual rank, for the extracted schedule.

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. Zero amplitude outside the next actual rank, for the extracted schedule.

Declaration kind. theorem.

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

Lean code for Theorem6.45.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedAt_supported
  {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (t : ℕ)
  (bit : Fin 2) (b a : Fin B)
  (hb :
    QuantumBlockEncoding.TensorTrainSchedule.rankAt C (t + 1) ≤ ↑b) :
  QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t (bit, b) a = 0
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedAt_supported
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (t : ℕ) (bit : Fin 2) (b a : Fin B)
  (hb :
    QuantumBlockEncoding.TensorTrainSchedule.rankAt
        C (t + 1) ≤
      ↑b) :
  QuantumBlockEncoding.TensorTrainSchedule.paddedAt
      C t (bit, b) a =
    0
    Zero amplitude outside the next actual rank, for the extracted schedule.
Theorem6.45.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transfer shift”; the hypotheses and conclusion in the code panel fix its exact scope. Rewrite chronological transfer in first-bit order, matching 'Chain.cons'.

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. Rewrite chronological transfer in first-bit order, matching 'Chain.cons'. The algebra still multiplies the last emitted matrix on the left.

Declaration kind. theorem.

Source: QuantumBlockEncoding/TensorTrainSchedule.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.45.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.transfer_shift.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.transfer K (n + 1) x =
    QuantumBlockEncoding.SequentialBondPreparation.transfer
        (fun t => K (t + 1)) n (Fin.tail x) *
      QuantumBlockEncoding.SequentialBondPreparation.coreSlice (K 0)
        (x 0)
    theorem QuantumBlockEncoding.TensorTrainSchedule.transfer_shift.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.transfer
      K (n + 1) x =
    QuantumBlockEncoding.SequentialBondPreparation.transfer
        (fun t => K (t + 1)) n
        (Fin.tail x) *
      QuantumBlockEncoding.SequentialBondPreparation.coreSlice
        (K 0) (x 0)
    Rewrite chronological transfer in first-bit order, matching `Chain.cons`.
The algebra still multiplies the last emitted matrix on the left.
Theorem6.45.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded slice mul vec”; the hypotheses and conclusion in the code panel fix its exact scope. One extracted core slice acts as its exact real row-vector contraction, with zero padding on the old and new bond labels.

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 extracted core slice acts as its exact real row-vector contraction, with zero padding on the old and new bond labels.

Declaration kind. theorem.

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

Lean code for Theorem6.45.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedSlice_mulVec {l r B : ℕ}
  (hl : l ≤ B) (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (bit : Fin 2) (v : Fin l → ℝ) :
  (QuantumBlockEncoding.SequentialBondPreparation.coreSlice
          (QuantumBlockEncoding.TensorTrainCanonical.paddedCore A)
          bit).mulVec
      (QuantumBlockEncoding.TensorTrainCanonical.padVector fun a =>
        ↑(v a)) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector fun b =>
      ↑(Matrix.vecMul v
          (QuantumBlockEncoding.TensorTrainCanonical.slice A bit) b)
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedSlice_mulVec
  {l r B : ℕ} (hl : l ≤ B)
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (bit : Fin 2) (v : Fin l → ℝ) :
  (QuantumBlockEncoding.SequentialBondPreparation.coreSlice
          (QuantumBlockEncoding.TensorTrainCanonical.paddedCore
            A)
          bit).mulVec
      (QuantumBlockEncoding.TensorTrainCanonical.padVector
        fun a => ↑(v a)) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      fun b =>
      ↑(Matrix.vecMul v
          (QuantumBlockEncoding.TensorTrainCanonical.slice
            A bit)
          b)
    One extracted core slice acts as its exact real row-vector contraction,
with zero padding on the old and new bond labels.
Theorem6.45.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transfer padded”; the hypotheses and conclusion in the code panel fix its exact scope. All-length transfer equals the original chain contraction at every padded output label, not just after projection onto its active subspace.

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. All-length transfer equals the original chain contraction at every padded output label, not just after projection onto its active subspace.

Declaration kind. theorem.

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

Lean code for Theorem6.45.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.transfer_padded {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B)
  (v : Fin l → ℝ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  (QuantumBlockEncoding.SequentialBondPreparation.transfer
          (QuantumBlockEncoding.TensorTrainSchedule.paddedAt C) n
          x).mulVec
      (QuantumBlockEncoding.TensorTrainCanonical.padVector fun a =>
        ↑(v a))
      b =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c =>
        ↑(Matrix.vecMul v
            (QuantumBlockEncoding.TensorTrainCanonical.contract C
              (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis x))
            c))
      b
    theorem QuantumBlockEncoding.TensorTrainSchedule.transfer_padded
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (v : Fin l → ℝ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  (QuantumBlockEncoding.SequentialBondPreparation.transfer
          (QuantumBlockEncoding.TensorTrainSchedule.paddedAt
            C)
          n x).mulVec
      (QuantumBlockEncoding.TensorTrainCanonical.padVector
        fun a => ↑(v a))
      b =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c =>
        ↑(Matrix.vecMul v
            (QuantumBlockEncoding.TensorTrainCanonical.contract
              C
              (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                x))
            c))
      b
    All-length transfer equals the original chain contraction at every
padded output label, not just after projection onto its active subspace.
Theorem6.45.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run eq transfer bounded”; the hypotheses and conclusion in the code panel fix its exact scope. A bounded version of the sequential local-column theorem: unused later stages need not implement the zero cores after the end of the schedule.

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 bounded version of the sequential local-column theorem: unused later stages need not implement the zero cores after the end of the schedule.

Declaration kind. theorem.

Source: QuantumBlockEncoding/TensorTrainSchedule.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.45.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_eq_transfer_bounded.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (active : ℕ → B → Prop) (boundary : B → ℂ)
  (initialSupport : ∀ (b : B), ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (n : ℕ)
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : B),
        active t a → U t (bit, b) (0, a) = K t (bit, b) a)
  (x : QuantumBlockEncoding.PrimitiveBasis n) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U boundary n
      (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer K n
          x).mulVec
      boundary b
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_eq_transfer_bounded.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (active : ℕ → B → Prop)
  (boundary : B → ℂ)
  (initialSupport :
    ∀ (b : B),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (n : ℕ)
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : B),
        active t a →
          U t (bit, b) (0, a) =
            K t (bit, b) a)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U boundary n (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer
          K n x).mulVec
      boundary b
    A bounded version of the sequential local-column theorem: unused later
stages need not implement the zero cores after the end of the schedule.
Theorem6.45.12
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run padded”; the hypotheses and conclusion in the code panel fix its exact scope. Exact complete sequential action of the schedule extracted from an actual dependent 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. Exact complete sequential action of the schedule extracted from an actual dependent train. Only its first 'n' local active columns are premises.

Declaration kind. theorem.

Source: QuantumBlockEncoding/TensorTrainSchedule.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.45.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_padded {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B)
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage (Fin B))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : Fin B),
        ↑a < QuantumBlockEncoding.TensorTrainSchedule.rankAt C t →
          U t (bit, b) (0, a) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t
              (bit, b) a)
  (v : Fin l → ℝ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U
      (QuantumBlockEncoding.TensorTrainCanonical.padVector fun a =>
        ↑(v a))
      n (x, b) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c =>
        ↑(Matrix.vecMul v
            (QuantumBlockEncoding.TensorTrainCanonical.contract C
              (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis x))
            c))
      b
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_padded
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        (Fin B))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : Fin B),
        ↑a <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt
              C t →
          U t (bit, b) (0, a) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt
              C t (bit, b) a)
  (v : Fin l → ℝ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U
      (QuantumBlockEncoding.TensorTrainCanonical.padVector
        fun a => ↑(v a))
      n (x, b) =
    QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun c =>
        ↑(Matrix.vecMul v
            (QuantumBlockEncoding.TensorTrainCanonical.contract
              C
              (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                x))
            c))
      b
    Exact complete sequential action of the schedule extracted from an
actual dependent train. Only its first `n` local active columns are premises.
Theorem6.45.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run terminal clean”; the hypotheses and conclusion in the code panel fix its exact scope. Terminal dimension one gives whole-state cleanup at physical label zero.

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. Terminal dimension one gives whole-state cleanup at physical label zero. The amplitude at every other padded label is exactly zero.

Declaration kind. theorem.

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

Lean code for Theorem6.45.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_terminal_clean {n l B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B)
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage (Fin B))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : Fin B),
        ↑a < QuantumBlockEncoding.TensorTrainSchedule.rankAt C t →
          U t (bit, b) (0, a) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t
              (bit, b) a)
  (v : Fin l → ℝ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U
      (QuantumBlockEncoding.TensorTrainCanonical.padVector fun a =>
        ↑(v a))
      n (x, b) =
    if ↑b = 0 then
      ↑(Matrix.vecMul v
          (QuantumBlockEncoding.TensorTrainCanonical.contract C
            (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis x))
          0)
    else 0
    theorem QuantumBlockEncoding.TensorTrainSchedule.run_terminal_clean
  {n l B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        (Fin B))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : Fin B),
        ↑a <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt
              C t →
          U t (bit, b) (0, a) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt
              C t (bit, b) a)
  (v : Fin l → ℝ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : Fin B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U
      (QuantumBlockEncoding.TensorTrainCanonical.padVector
        fun a => ↑(v a))
      n (x, b) =
    if ↑b = 0 then
      ↑(Matrix.vecMul v
          (QuantumBlockEncoding.TensorTrainCanonical.contract
            C
            (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
              x))
          0)
    else 0
    Terminal dimension one gives whole-state cleanup at physical label zero.
The amplitude at every other padded label is exactly zero.
Theorem6.45.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded at active isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Every extracted stage of a canonical chain has orthonormal occupied columns in the one fixed 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. Every extracted stage of a canonical chain has orthonormal occupied columns in the one fixed physical register.

Declaration kind. theorem.

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

Lean code for Theorem6.45.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedAt_active_isometry
  {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hC : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical C)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B) (t : ℕ)
  (ht : t < n)
  (a c : Fin (QuantumBlockEncoding.TensorTrainSchedule.rankAt C t)) :
  ∑ out,
      star
          (QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t out
            (Fin.castLE ⋯ a)) *
        QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t out
          (Fin.castLE ⋯ c) =
    if a = c then 1 else 0
    theorem QuantumBlockEncoding.TensorTrainSchedule.paddedAt_active_isometry
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hC :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      C)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (t : ℕ) (ht : t < n)
  (a c :
    Fin
      (QuantumBlockEncoding.TensorTrainSchedule.rankAt
        C t)) :
  ∑ out,
      star
          (QuantumBlockEncoding.TensorTrainSchedule.paddedAt
            C t out (Fin.castLE ⋯ a)) *
        QuantumBlockEncoding.TensorTrainSchedule.paddedAt
          C t out (Fin.castLE ⋯ c) =
    if a = c then 1 else 0
    Every extracted stage of a canonical chain has orthonormal occupied
columns in the one fixed physical register.
Theorem6.45.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists normalized preparation schedule”; the hypotheses and conclusion in the code panel fix its exact scope. A normalized scalar-boundary source train has a bounded canonical schedule with exact whole-state source action whenever its *local occupied columns* are implemented.

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 scalar-boundary source train has a bounded canonical schedule with exact whole-state source action whenever its *local occupied columns* are implemented. No source-state oracle or global-action hypothesis occurs in the premises.

Declaration kind. theorem.

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

Lean code for Theorem6.45.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainSchedule.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainSchedule.exists_normalized_preparation_schedule
  {n B : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B)
  (hNorm :
    ∑ 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 ∧
          QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ B ∧
            ∀
              (U :
                ℕ →
                  QuantumBlockEncoding.SequentialBondPreparation.Stage
                    (Fin B)),
              (∀ t < n,
                  ∀ (bit : Fin 2) (b a : Fin B),
                    ↑a <
                        QuantumBlockEncoding.TensorTrainSchedule.rankAt
                          D t →
                      U t (bit, b) (0, a) =
                        QuantumBlockEncoding.TensorTrainSchedule.paddedAt
                          D t (bit, b) a) →
                ∀ (x : QuantumBlockEncoding.PrimitiveBasis n)
                  (b : Fin B),
                  QuantumBlockEncoding.SequentialBondPreparation.run U
                      (QuantumBlockEncoding.TensorTrainCanonical.padVector
                        fun a => ↑(u a))
                      n (x, b) =
                    if ↑b = 0 then
                      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
                          C
                          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                            x)
                          0 0)
                    else 0
    theorem QuantumBlockEncoding.TensorTrainSchedule.exists_normalized_preparation_schedule
  {n B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (hNorm :
    ∑ 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 ∧
          QuantumBlockEncoding.TensorTrainCanonical.maxBond
                D ≤
              B ∧
            ∀
              (U :
                ℕ →
                  QuantumBlockEncoding.SequentialBondPreparation.Stage
                    (Fin B)),
              (∀ t < n,
                  ∀ (bit : Fin 2)
                    (b a : Fin B),
                    ↑a <
                        QuantumBlockEncoding.TensorTrainSchedule.rankAt
                          D t →
                      U t (bit, b)
                          (0, a) =
                        QuantumBlockEncoding.TensorTrainSchedule.paddedAt
                          D t (bit, b)
                          a) →
                ∀
                  (x :
                    QuantumBlockEncoding.PrimitiveBasis
                      n)
                  (b : Fin B),
                  QuantumBlockEncoding.SequentialBondPreparation.run
                      U
                      (QuantumBlockEncoding.TensorTrainCanonical.padVector
                        fun a => ↑(u a))
                      n (x, b) =
                    if ↑b = 0 then
                      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
                          C
                          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                            x)
                          0 0)
                    else 0
    A normalized scalar-boundary source train has a bounded canonical
schedule with exact whole-state source action whenever its *local occupied
columns* are implemented. No source-state oracle or global-action hypothesis
occurs in the premises.