6.44. QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean🔗

15 explicit public declarations, in source order.

Definition6.44.1

uses 0used by 0✓L∃∀N

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

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/TensorTrainPrimitivePreparation.lean:22. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.44.1●1 definition

defdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

def QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow {l : ℕ}
  (u : Fin l → ℝ) : Matrix (Fin 1) (Fin l) ℝ

def QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
  {l : ℕ} (u : Fin l → ℝ) :
  Matrix (Fin 1) (Fin l) ℝ

Theorem6.44.2

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.2●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow_isometry
  {l : ℕ} (u : Fin l → ℝ)
  (hu : QuantumBlockEncoding.TensorTrainCanonical.mass u = 1) :
  QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow u *
      (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
          u).transpose =
    1

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow_isometry
  {l : ℕ} (u : Fin l → ℝ)
  (hu :
    QuantumBlockEncoding.TensorTrainCanonical.mass
        u =
      1) :
  QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
        u *
      (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
          u).transpose =
    1

Theorem6.44.3

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.3●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryCore_isometry
  {l r : ℕ} (u : Fin l → ℝ)
  (hu : QuantumBlockEncoding.TensorTrainCanonical.mass u = 1)
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r)
  (hA : A * Matrix.transpose A = 1) :
  QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow u *
        A *
      (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
            u *
          A).transpose =
    1

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryCore_isometry
  {l r : ℕ} (u : Fin l → ℝ)
  (hu :
    QuantumBlockEncoding.TensorTrainCanonical.mass
        u =
      1)
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r)
  (hA : A * Matrix.transpose A = 1) :
  QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
          u *
        A *
      (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
            u *
          A).transpose =
    1

Theorem6.44.4

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.4●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryCore_contract
  {n l m r : ℕ} (u : Fin l → ℝ)
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l m)
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n m r)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons
        (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
            u *
          A)
        C)
      x =
    QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow u *
      QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons A C) x

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryCore_contract
  {n l m r : ℕ} (u : Fin l → ℝ)
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l m)
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n m r)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons
        (QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
            u *
          A)
        C)
      x =
    QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
        u *
      QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.TensorTrainCanonical.Chain.cons
          A C)
        x

Theorem6.44.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists unit boundary canonical”; the hypotheses and conclusion in the code panel fix its exact scope. Eliminate the signed initial residual by absorbing it into the first row-isometric core.

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

Technical source note. Eliminate the signed initial residual by absorbing it into the first row-isometric core. This is not a free state-initialization assumption.

Declaration kind. theorem.

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

Lean code for Theorem6.44.5●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.exists_unitBoundary_canonical
  {n B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ B)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2 =
      1) :
  ∃ D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D ∧
      QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ B ∧
        ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)),
          QuantumBlockEncoding.TensorTrainCanonical.contract D x 0 0 =
            QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.exists_unitBoundary_canonical
  {n B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      B)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2 =
      1) :
  ∃ D,
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
        D ∧
      QuantumBlockEncoding.TensorTrainCanonical.maxBond
            D ≤
          B ∧
        ∀
          (x :
            QuantumBlockEncoding.TensorTrainCanonical.Word
              (n + 1)),
          QuantumBlockEncoding.TensorTrainCanonical.contract
              D x 0 0 =
            QuantumBlockEncoding.TensorTrainCanonical.contract
              C x 0 0

Eliminate the signed initial residual by absorbing it into the first
row-isometric core. This is not a free state-initialization assumption.

Definition6.44.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “transport stage”. Reindex only the finite bond labels of a local stage.

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

Technical source note. Reindex only the finite bond labels of a local stage.

Declaration kind. def.

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

Lean code for Definition6.44.6●1 definition

defdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

def QuantumBlockEncoding.TensorTrainPrimitivePreparation.transportStage.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2} (e : B ≃ C)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage C) :
  QuantumBlockEncoding.SequentialBondPreparation.Stage B

def QuantumBlockEncoding.TensorTrainPrimitivePreparation.transportStage.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  (e : B ≃ C)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      C) :
  QuantumBlockEncoding.SequentialBondPreparation.Stage
    B

Reindex only the finite bond labels of a local stage.

Theorem6.44.7

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.7●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.run_transport.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2} [Fintype B] [Fintype C] [DecidableEq B]
  [DecidableEq C] (e : B ≃ C)
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage C)
  (boundary : B → ℂ) (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : C) :
  QuantumBlockEncoding.SequentialBondPreparation.run U
      (fun c => boundary (e.symm c)) n (x, b) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.TensorTrainPrimitivePreparation.transportStage
          e (U t))
      boundary n (x, e.symm b)

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.run_transport.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  [Fintype B] [Fintype C] [DecidableEq B]
  [DecidableEq C] (e : B ≃ C)
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        C)
  (boundary : B → ℂ) (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : C) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U (fun c => boundary (e.symm c)) n
      (x, b) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.TensorTrainPrimitivePreparation.transportStage
          e (U t))
      boundary n (x, e.symm b)

Theorem6.44.8

uses 0used by 0✓L∃∀N

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

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/TensorTrainPrimitivePreparation.lean:87. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.44.8●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.bondIndex_zero
  (q : ℕ) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) fun x => 0) = 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.bondIndex_zero
  (q : ℕ) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
          q)
        fun x => 0) =
    0

Theorem6.44.9

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.9●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.bondIndex_zero_iff
  {q : ℕ} (b : QuantumBlockEncoding.PrimitiveBasis q) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) b) = 0 ↔
    b = fun x => 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.bondIndex_zero_iff
  {q : ℕ}
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
            q)
          b) =
      0 ↔
    b = fun x => 0

Theorem6.44.10

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

Source: QuantumBlockEncoding/TensorTrainPrimitivePreparation.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.44.10●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.initial_padding
  {q : ℕ} (b : QuantumBlockEncoding.PrimitiveBasis q) :
  QuantumBlockEncoding.TensorTrainCanonical.padVector (fun x => 1)
      ((QuantumBlockEncoding.primitiveBasisLEEquiv q) b) =
    QuantumBlockEncoding.evalPrimitiveCircuit [] b fun x => 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.initial_padding
  {q : ℕ}
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  QuantumBlockEncoding.TensorTrainCanonical.padVector
      (fun x => 1)
      ((QuantumBlockEncoding.primitiveBasisLEEquiv
          q)
        b) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      [] b fun x => 0

Theorem6.44.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run circuits clean”; the hypotheses and conclusion in the code panel fix its exact scope. Actual local circuit columns imply the complete sequential source state from an empty initial circuit, including terminal cleanup.

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

Technical source note. Actual local circuit columns imply the complete sequential source state from an empty initial circuit, including terminal cleanup.

Declaration kind. theorem.

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

Lean code for Theorem6.44.11●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.run_circuits_clean
  {n q : ℕ} (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ 2 ^ q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : QuantumBlockEncoding.PrimitiveBasis q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt D t →
          QuantumBlockEncoding.evalPrimitiveCircuit (stages t)
              (Fin.snoc b bit) (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt D t
              (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv q) a))
  (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c =>
        QuantumBlockEncoding.evalPrimitiveCircuit [] c fun x => 0)
      n (x, b) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract D
          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis x) 0 0)
    else 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.run_circuits_clean
  {n q : ℕ}
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D ≤
      2 ^ q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2)
        (b a :
          QuantumBlockEncoding.PrimitiveBasis
            q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt
              D t →
          QuantumBlockEncoding.evalPrimitiveCircuit
              (stages t) (Fin.snoc b bit)
              (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt
              D t
              (bit,
                (QuantumBlockEncoding.primitiveBasisLEEquiv
                    q)
                  b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a))
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c =>
        QuantumBlockEncoding.evalPrimitiveCircuit
          [] c fun x => 0)
      n (x, b) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
          D
          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
            x)
          0 0)
    else 0

Actual local circuit columns imply the complete sequential source state
from an empty initial circuit, including terminal cleanup.

Theorem6.44.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “public circuit clean”; the hypotheses and conclusion in the code panel fix its exact scope. The published data-low/bond-high circuit realizes the chain in the corresponding most-significant-bit-first word order.

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

Technical source note. The published data-low/bond-high circuit realizes the chain in the corresponding most-significant-bit-first word order.

Declaration kind. theorem.

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

Lean code for Theorem6.44.12●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.publicCircuit_clean
  {n q : ℕ} (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ 2 ^ q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2) (b a : QuantumBlockEncoding.PrimitiveBasis q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt D t →
          QuantumBlockEncoding.evalPrimitiveCircuit (stages t)
              (Fin.snoc b bit) (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt D t
              (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv q) a))
  (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit []
        stages n)
      (Fin.append x b) fun x => 0) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract D
          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis fun i =>
            x i.rev)
          0 0)
    else 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.publicCircuit_clean
  {n q : ℕ}
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D ≤
      2 ^ q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (columns :
    ∀ t < n,
      ∀ (bit : Fin 2)
        (b a :
          QuantumBlockEncoding.PrimitiveBasis
            q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt
              D t →
          QuantumBlockEncoding.evalPrimitiveCircuit
              (stages t) (Fin.snoc b bit)
              (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt
              D t
              (bit,
                (QuantumBlockEncoding.primitiveBasisLEEquiv
                    q)
                  b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a))
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
        [] stages n)
      (Fin.append x b) fun x => 0) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
          D
          (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
            fun i => x i.rev)
          0 0)
    else 0

The published data-low/bond-high circuit realizes the chain in the
corresponding most-significant-bit-first word order.

Theorem6.44.13

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.44.13●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.assemble_gateCount
  (q : ℕ) (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble q stages
        n).gateCount =
    ∑ t ∈ Finset.range n, (stages t).gateCount

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.assemble_gateCount
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble
        q stages n).gateCount =
    ∑ t ∈ Finset.range n,
      (stages t).gateCount

Theorem6.44.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “public circuit gate count bound”; the hypotheses and conclusion in the code panel fix its exact scope. Gate-list length, not only an arithmetic count proxy, is bounded.

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

Technical source note. Gate-list length, not only an arithmetic count proxy, is bounded.

Declaration kind. theorem.

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

Lean code for Theorem6.44.14●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.publicCircuit_gateCount_bound
  {q : ℕ} (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n bound : ℕ) (h : ∀ t < n, (stages t).gateCount ≤ bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit []
        stages n).gateCount ≤
    n * bound

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.publicCircuit_gateCount_bound
  {q : ℕ}
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n bound : ℕ)
  (h :
    ∀ t < n,
      (stages t).gateCount ≤ bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
        [] stages n).gateCount ≤
    n * bound

Gate-list length, not only an arithmetic count proxy, is bounded.

Theorem6.44.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists primitive preparation”; the hypotheses and conclusion in the code panel fix its exact scope. Any bounded normalized nonempty real scalar-boundary tensor train has an actual clean primitive preparation.

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

Technical source note. Any bounded normalized nonempty real scalar-boundary tensor train has an actual clean primitive preparation. The bound counts every instruction in the circuit list; initialization uses zero gates after exact boundary absorption. This theorem makes no claim about classical computation of its exact angles.

Declaration kind. theorem.

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

Lean code for Theorem6.44.15●1 theorem

theoremdefined in QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

complete

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.exists_primitive_preparation
  {n q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2 =
      1) :
  ∃ circuit,
    circuit.gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧
      circuit.resource.oracleCalls = 0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit circuit ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis (n + 1 + q)) ℂ ∧
          ∀ (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
            (b : QuantumBlockEncoding.PrimitiveBasis q),
            (QuantumBlockEncoding.evalPrimitiveCircuit circuit
                (Fin.append x b) fun x => 0) =
              if b = fun x => 0 then
                ↑(QuantumBlockEncoding.TensorTrainCanonical.contract C
                    (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                      fun i => x i.rev)
                    0 0)
              else 0

theorem QuantumBlockEncoding.TensorTrainPrimitivePreparation.exists_primitive_preparation
  {n q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2 =
      1) :
  ∃ circuit,
    circuit.gateCount ≤
        (n + 1) * (6 * (2 ^ q) ^ 3) ∧
      circuit.resource.oracleCalls = 0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              circuit ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 + q))
              ℂ ∧
          ∀
            (x :
              QuantumBlockEncoding.PrimitiveBasis
                (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                q),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                circuit (Fin.append x b)
                fun x => 0) =
              if b = fun x => 0 then
                ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
                    C
                    (QuantumBlockEncoding.TensorTrainSchedule.wordOfBasis
                      fun i => x i.rev)
                    0 0)
              else 0

Any bounded normalized nonempty real scalar-boundary tensor train has
an actual clean primitive preparation. The bound counts every instruction in
the circuit list; initialization uses zero gates after exact boundary absorption.
This theorem makes no claim about classical computation of its exact angles.