ASPBE Lean Blueprint

6.42. QuantumBlockEncoding/TensorTrainLocalCompiler.lean🔗

10 explicit public declarations, in source order.

Theorem6.42.1
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists so named”; the hypotheses and conclusion in the code panel fix its exact scope. Coordinate adapter for special-orthogonal completion on any finite named basis, with prescribed columns at arbitrary physical 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. Coordinate adapter for special-orthogonal completion on any finite named basis, with prescribed columns at arbitrary physical labels.

Declaration kind. theorem.

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

Lean code for Theorem6.42.1●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_SO_named.{u_1}
  {I : Type u_1} [Fintype I] [DecidableEq I] {r : ℕ}
  (hr : r < Fintype.card I) (V : Matrix I (Fin r) ℝ) (e : Fin r ↪ I)
  (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧ ∀ (i : I) (a : Fin r), U i (e a) = V i a
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_SO_named.{u_1}
  {I : Type u_1} [Fintype I]
  [DecidableEq I] {r : ℕ}
  (hr : r < Fintype.card I)
  (V : Matrix I (Fin r) ℝ) (e : Fin r ↪ I)
  (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧
        ∀ (i : I) (a : Fin r),
          U i (e a) = V i a
    Coordinate adapter for special-orthogonal completion on any finite
named basis, with prescribed columns at arbitrary physical labels.
Definition6.42.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “local index”. The bit is the highest local physical wire; the bond uses low wires.

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 bit is the highest local physical wire; the bond uses low wires.

Declaration kind. def.

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

Lean code for Definition6.42.2●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    def QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis (q + 1) ≃ Fin 2 × Fin (2 ^ q)
    def QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex
  (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis
      (q + 1) ≃
    Fin 2 × Fin (2 ^ q)
    The bit is the highest local physical wire; the bond uses low wires.
Theorem6.42.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “local index snoc”; 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/TensorTrainLocalCompiler.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.42.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex_snoc (q : ℕ)
  (b : QuantumBlockEncoding.PrimitiveBasis q) (bit : Fin 2) :
  (QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex q)
      (Fin.snoc b bit) =
    (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex_snoc
  (q : ℕ)
  (b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (bit : Fin 2) :
  (QuantumBlockEncoding.TensorTrainLocalCompiler.localIndex
        q)
      (Fin.snoc b bit) =
    (bit,
      (QuantumBlockEncoding.primitiveBasisLEEquiv
          q)
        b)
Theorem6.42.4
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded at real”; 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/TensorTrainLocalCompiler.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.42.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.paddedAt_real
  {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (t : ℕ)
  (out : Fin 2 × Fin B) (a : Fin B) :
  ↑(QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t out a).re =
    QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t out a
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.paddedAt_real
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (t : ℕ) (out : Fin 2 × Fin B)
  (a : Fin B) :
  ↑(QuantumBlockEncoding.TensorTrainSchedule.paddedAt
          C t out a).re =
    QuantumBlockEncoding.TensorTrainSchedule.paddedAt
      C t out a
Theorem6.42.5
uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.42.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.paddedAt_im_zero
  {n l r B : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (t : ℕ)
  (out : Fin 2 × Fin B) (a : Fin B) :
  (QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t out a).im = 0
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.paddedAt_im_zero
  {n l r B : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (t : ℕ) (out : Fin 2 × Fin B)
  (a : Fin B) :
  (QuantumBlockEncoding.TensorTrainSchedule.paddedAt
        C t out a).im =
    0
Definition6.42.6
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.42.6●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    def QuantumBlockEncoding.TensorTrainLocalCompiler.activePositions {q l : ℕ}
  (hl : l ≤ 2 ^ q) : Fin l ↪ QuantumBlockEncoding.PrimitiveBasis (q + 1)
    def QuantumBlockEncoding.TensorTrainLocalCompiler.activePositions
  {q l : ℕ} (hl : l ≤ 2 ^ q) :
  Fin l ↪
    QuantumBlockEncoding.PrimitiveBasis
      (q + 1)
Definition6.42.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “active columns”. The occupied real columns of a padded core, in physical named-wire order.

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 occupied real columns of a padded core, in physical named-wire order.

Declaration kind. def.

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

Lean code for Definition6.42.7●1 definition
  • defdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    def QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns
  {n l r q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) (t : ℕ)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
    (Fin (QuantumBlockEncoding.TensorTrainSchedule.rankAt C t)) ℝ
    def QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns
  {n l r q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (t : ℕ)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      (q + 1))
    (Fin
      (QuantumBlockEncoding.TensorTrainSchedule.rankAt
        C t))
    ℝ
    The occupied real columns of a padded core, in physical named-wire order.
Theorem6.42.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “active columns isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Exact real orthonormality is extracted from the proved complex padded-core semantics; no ambient matrix or desired circuit action is assumed.

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 real orthonormality is extracted from the proved complex padded-core semantics; no ambient matrix or desired circuit action is assumed.

Declaration kind. theorem.

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

Lean code for Theorem6.42.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns_isometry
  {n l r q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hC : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical C)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q)
  (t : ℕ) (ht : t < n) :
  (QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns C t
          hB).transpose *
      QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns C t
        hB =
    1
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns_isometry
  {n l r q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hC :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      C)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q)
  (t : ℕ) (ht : t < n) :
  (QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns
          C t hB).transpose *
      QuantumBlockEncoding.TensorTrainLocalCompiler.activeColumns
        C t hB =
    1
    Exact real orthonormality is extracted from the proved complex padded-core
semantics; no ambient matrix or desired circuit action is assumed.
Theorem6.42.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists local circuit with resources”; the hypotheses and conclusion in the code panel fix its exact scope. Every actual canonical stage has an exact primitive implementation on the 'q' low bond wires and one highest output wire.

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 actual canonical stage has an exact primitive implementation on the 'q' low bond wires and one highest output wire. Completion has a spare column because the active rank is at most half the physical dimension. The existence proof uses exact real choices and is not a classical preprocessing-cost bound.

Declaration kind. theorem.

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

Lean code for Theorem6.42.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_local_circuit_with_resources
  {n l r q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hC : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical C)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q)
  (t : ℕ) (ht : t < n) :
  ∃ c,
    c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
      c.resource.oracleCalls = 0 ∧
        ∀ (bit : Fin 2) (b a : QuantumBlockEncoding.PrimitiveBasis q),
          ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) a) <
              QuantumBlockEncoding.TensorTrainSchedule.rankAt C t →
            QuantumBlockEncoding.evalPrimitiveCircuit c (Fin.snoc b bit)
                (Fin.snoc a 0) =
              QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t
                (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
                ((QuantumBlockEncoding.primitiveBasisLEEquiv q) a)
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_local_circuit_with_resources
  {n l r q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hC :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      C)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q)
  (t : ℕ) (ht : t < n) :
  ∃ c,
    c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
      c.resource.oracleCalls = 0 ∧
        ∀ (bit : Fin 2)
          (b a :
            QuantumBlockEncoding.PrimitiveBasis
              q),
          ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
                    q)
                  a) <
              QuantumBlockEncoding.TensorTrainSchedule.rankAt
                C t →
            QuantumBlockEncoding.evalPrimitiveCircuit
                c (Fin.snoc b bit)
                (Fin.snoc a 0) =
              QuantumBlockEncoding.TensorTrainSchedule.paddedAt
                C t
                (bit,
                  (QuantumBlockEncoding.primitiveBasisLEEquiv
                      q)
                    b)
                ((QuantumBlockEncoding.primitiveBasisLEEquiv
                    q)
                  a)
    Every actual canonical stage has an exact primitive implementation on the
`q` low bond wires and one highest output wire. Completion has a spare column
because the active rank is at most half the physical dimension. The existence
proof uses exact real choices and is not a classical preprocessing-cost bound.
Theorem6.42.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists local circuit”; the hypotheses and conclusion in the code panel fix its exact scope. Minimal local-column interface for sequential tensor-train assembly.

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. Minimal local-column interface for sequential tensor-train assembly.

Declaration kind. theorem.

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

Lean code for Theorem6.42.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/TensorTrainLocalCompiler.lean
    complete
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_local_circuit
  {n l r q : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (hC : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical C)
  (hB : QuantumBlockEncoding.TensorTrainCanonical.maxBond C ≤ 2 ^ q)
  (t : ℕ) (ht : t < n) :
  ∃ c,
    c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
      ∀ (bit : Fin 2) (b a : QuantumBlockEncoding.PrimitiveBasis q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv q) a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt C t →
          QuantumBlockEncoding.evalPrimitiveCircuit c (Fin.snoc b bit)
              (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt C t
              (bit, (QuantumBlockEncoding.primitiveBasisLEEquiv q) b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv q) a)
    theorem QuantumBlockEncoding.TensorTrainLocalCompiler.exists_local_circuit
  {n l r q : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (hC :
    QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
      C)
  (hB :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        C ≤
      2 ^ q)
  (t : ℕ) (ht : t < n) :
  ∃ c,
    c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
      ∀ (bit : Fin 2)
        (b a :
          QuantumBlockEncoding.PrimitiveBasis
            q),
        ↑((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a) <
            QuantumBlockEncoding.TensorTrainSchedule.rankAt
              C t →
          QuantumBlockEncoding.evalPrimitiveCircuit
              c (Fin.snoc b bit)
              (Fin.snoc a 0) =
            QuantumBlockEncoding.TensorTrainSchedule.paddedAt
              C t
              (bit,
                (QuantumBlockEncoding.primitiveBasisLEEquiv
                    q)
                  b)
              ((QuantumBlockEncoding.primitiveBasisLEEquiv
                  q)
                a)
    Minimal local-column interface for sequential tensor-train assembly.