6.7. QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean🔗

18 explicit public declarations, in source order.

Definition6.7.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “absorb boundary”. Absorb the signed residual boundary into the actual first 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. Absorb the signed residual boundary into the actual first core.

Declaration kind. def.

Source: QuantumBlockEncoding/ConstructiveTensorTrainCompiler.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.7.1●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
  {n l r : ℕ} (u : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 r

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
  {n l r : ℕ} (u : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 r

Absorb the signed residual boundary into the actual first core.

Theorem6.7.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.2●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_canonical
  {n l r : ℕ} (u : Fin l → ℝ)
  (hu : QuantumBlockEncoding.TensorTrainCanonical.mass u = 1)
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l r)
  (hD : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
      u D)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_canonical
  {n l r : ℕ} (u : Fin l → ℝ)
  (hu :
    QuantumBlockEncoding.TensorTrainCanonical.mass
        u =
      1)
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l r)
  (hD :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      D) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
      u D)

Theorem6.7.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.3●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_contract
  {n l r : ℕ} (u : Fin l → ℝ)
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l r)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
        u D)
      x =
    QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow u *
      QuantumBlockEncoding.TensorTrainCanonical.contract D x

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_contract
  {n l r : ℕ} (u : Fin l → ℝ)
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l r)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
        u D)
      x =
    QuantumBlockEncoding.TensorTrainPrimitivePreparation.boundaryRow
        u *
      QuantumBlockEncoding.TensorTrainCanonical.contract
        D x

Theorem6.7.4

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.7.4●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_maxBond
  {n l r : ℕ} (u : Fin l → ℝ)
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
        u D) ≤
    max 1 (QuantumBlockEncoding.TensorTrainCanonical.maxBond D)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary_maxBond
  {n l r : ℕ} (u : Fin l → ℝ)
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.absorbBoundary
        u D) ≤
    max 1
      (QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D)

Definition6.7.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “unit boundary”. Concrete scalar-boundary canonical train, with no separate initialization circuit.

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. Concrete scalar-boundary canonical train, with no separate initialization circuit.

Declaration kind. def.

Source: QuantumBlockEncoding/ConstructiveTensorTrainCompiler.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.7.5●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
  {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

Concrete scalar-boundary canonical train, with no separate initialization circuit.

Theorem6.7.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.6●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_canonical
  {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2 =
      1) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
      C)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_canonical
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hNorm :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2 =
      1) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
      C)

Theorem6.7.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.7●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_contract
  {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
        C)
      x 0 0 =
    QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_contract
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
        C)
      x 0 0 =
    QuantumBlockEncoding.TensorTrainCanonical.contract
      C x 0 0

Theorem6.7.8

uses 0used by 0✓L∃∀N

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem6.7.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_maxBond_le
  {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
        C) ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond C

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary_maxBond_le
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.unitBoundary
        C) ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      C

Definition6.7.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “stage”. Every local primitive list is computed from its actual completed SO matrix.

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. Every local primitive list is computed from its actual completed SO matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/ConstructiveTensorTrainCompiler.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.7.9●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage {n l r q : ℕ}
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ 2 ^ q)
  (t : ℕ) : QuantumBlockEncoding.PrimitiveCircuit (q + 1)

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage
  {n l r q : ℕ}
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D ≤
      2 ^ q)
  (t : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + 1)

Every local primitive list is computed from its actual completed SO matrix.

Theorem6.7.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.10●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage_gateCount
  {n l r q : ℕ}
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ 2 ^ q)
  (t : ℕ) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage D hB
        t).gateCount ≤
    6 * (2 ^ q) ^ 3

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage_gateCount
  {n l r q : ℕ}
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D ≤
      2 ^ q)
  (t : ℕ) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage
        D hB t).gateCount ≤
    6 * (2 ^ q) ^ 3

Theorem6.7.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.11●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage_columns
  {n l r q : ℕ}
  (D : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hD : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical D)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond D ≤ 2 ^ q)
  (t : ℕ) (ht : t < n) (bit : Fin 2)
  (b a : QuantumBlockEncoding.PrimitiveBasis q)
  (ha :
    ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) a) <
      QuantumBlockEncoding.TensorTrainSchedule.rankAt D t) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage D hB
        t)
      (Fin.snoc b bit) (Fin.snoc a 0) =
    QuantumBlockEncoding.TensorTrainSchedule.paddedAt D t
      (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
      ((QuantumBlockEncoding.primitiveBasisLEEquiv q) a)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage_columns
  {n l r q : ℕ}
  (D :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hD :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      D)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        D ≤
      2 ^ q)
  (t : ℕ) (ht : t < n) (bit : Fin 2)
  (b a :
    QuantumBlockEncoding.PrimitiveBasis q)
  (ha :
    ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
            q)
          a) <
      QuantumBlockEncoding.TensorTrainSchedule.rankAt
        D t) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.stage
        D hB t)
      (Fin.snoc b bit) (Fin.snoc a 0) =
    QuantumBlockEncoding.TensorTrainSchedule.paddedAt
      D t
      (bit,
        (QuantumBlockEncoding.primitiveBasisLEEquiv
            q)
          b)
      ((QuantumBlockEncoding.primitiveBasisLEEquiv
          q)
        a)

Definition6.7.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. Final physical circuit: data occupy the low wires, and the clean bond the high wires.

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. Final physical circuit: data occupy the low wires, and the clean bond the high wires.

Declaration kind. def.

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

Lean code for Definition6.7.12●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile {n q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q) :
  QuantumBlockEncoding.PrimitiveCircuit (n + 1 + q)

def QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
  {n q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q) :
  QuantumBlockEncoding.PrimitiveCircuit
    (n + 1 + q)

Final physical circuit: data occupy the low wires, and the clean bond the high wires.

Theorem6.7.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.13●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_gateCount
  {n q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
        hB).gateCount ≤
    (n + 1) * (6 * (2 ^ q) ^ 3)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_gateCount
  {n q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
        C hB).gateCount ≤
    (n + 1) * (6 * (2 ^ q) ^ 3)

Theorem6.7.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.14●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_depth
  {n q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
          hB).resource.depth ≤
    (n + 1) * (6 * (2 ^ q) ^ 3)

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_depth
  {n q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
          C hB).resource.depth ≤
    (n + 1) * (6 * (2 ^ q) ^ 3)

Theorem6.7.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.7.15●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_unitary
  {n q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
        hB) ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis (n + 1 + q)) ℂ

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_unitary
  {n q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      (n + 1) 1 1)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
        C hB) ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        (n + 1 + q))
      ℂ

Theorem6.7.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile columns”; the hypotheses and conclusion in the code panel fix its exact scope. All data words and all bond sectors, including every non-clean output.

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

Technical source note. All data words and all bond sectors, including every non-clean output.

Declaration kind. theorem.

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

Lean code for Theorem6.7.16●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_columns
  {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)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
        hB)
      (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.ConstructiveTensorTrainCompiler.compile_columns
  {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)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
        C hB)
      (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

All data words and all bond sectors, including every non-clean output.

Theorem6.7.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile word”; 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/ConstructiveTensorTrainCompiler.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.7.17●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_word
  {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)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1))
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
        hB)
      (Fin.append
        (fun i => QuantumBlockEncoding.TensorTrainWord.toBasis x i.rev)
        b)
      fun x => 0) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0)
    else 0

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_word
  {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)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1))
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  (QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
        C hB)
      (Fin.append
        (fun i =>
          QuantumBlockEncoding.TensorTrainWord.toBasis
            x i.rev)
        b)
      fun x => 0) =
    if b = fun x => 0 then
      ↑(QuantumBlockEncoding.TensorTrainCanonical.contract
          C x 0 0)
    else 0

Theorem6.7.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile spec”; the hypotheses and conclusion in the code panel fix its exact scope. Complete quantum correctness and resource certificate for the actual producer.

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

Technical source note. Complete quantum correctness and resource certificate for the actual producer.

Declaration kind. theorem.

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

Lean code for Theorem6.7.18●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrainCompiler.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile_spec
  {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) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
          hB).gateCount ≤
      (n + 1) * (6 * (2 ^ q) ^ 3) ∧
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
              hB).resource.depth ≤
        (n + 1) * (6 * (2 ^ q) ^ 3) ∧
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile C
                hB).resource.oracleCalls =
          0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
                C hB) ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis (n + 1 + q)) ℂ ∧
          ∀ (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
            (b : QuantumBlockEncoding.PrimitiveBasis q),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
                  C hB)
                (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.ConstructiveTensorTrainCompiler.compile_spec
  {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) :
  (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
          C hB).gateCount ≤
      (n + 1) * (6 * (2 ^ q) ^ 3) ∧
    (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
              C hB).resource.depth ≤
        (n + 1) * (6 * (2 ^ q) ^ 3) ∧
      (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
                C
                hB).resource.oracleCalls =
          0 ∧
        QuantumBlockEncoding.evalPrimitiveCircuit
              (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
                C hB) ∈
            Matrix.unitaryGroup
              (QuantumBlockEncoding.PrimitiveBasis
                (n + 1 + q))
              ℂ ∧
          ∀
            (x :
              QuantumBlockEncoding.PrimitiveBasis
                (n + 1))
            (b :
              QuantumBlockEncoding.PrimitiveBasis
                q),
            (QuantumBlockEncoding.evalPrimitiveCircuit
                (QuantumBlockEncoding.ConstructiveTensorTrainCompiler.compile
                  C hB)
                (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

Complete quantum correctness and resource certificate for the actual producer.