6.29. QuantumBlockEncoding/SequentialPrimitiveAssembly.lean🔗

37 explicit public declarations, in source order.

Definition6.29.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.29.1●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.pad {m : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit m) (extra : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit (m + extra)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.pad
  {m : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m)
  (extra : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (m + extra)

Definition6.29.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pad 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. 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/SequentialPrimitiveAssembly.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.29.2●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix {m : ℕ}
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis m)
      (QuantumBlockEncoding.PrimitiveBasis m) ℂ)
  (extra : ℕ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis (m + extra))
    (QuantumBlockEncoding.PrimitiveBasis (m + extra)) ℂ

def QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix
  {m : ℕ}
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      ℂ)
  (extra : ℕ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      (m + extra))
    (QuantumBlockEncoding.PrimitiveBasis
      (m + extra))
    ℂ

Theorem6.29.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval pad”; 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/SequentialPrimitiveAssembly.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.29.3●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_pad {m : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit m) (extra : ℕ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad c extra) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix
      (QuantumBlockEncoding.evalPrimitiveCircuit c) extra

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_pad
  {m : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m)
  (extra : ℕ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad
        c extra) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix
      (QuantumBlockEncoding.evalPrimitiveCircuit
        c)
      extra

Theorem6.29.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.4●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix_append
  {m : ℕ}
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis m)
      (QuantumBlockEncoding.PrimitiveBasis m) ℂ)
  (t : ℕ) (a b : QuantumBlockEncoding.PrimitiveBasis m)
  (x y : QuantumBlockEncoding.PrimitiveBasis t) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix M t
      (Fin.append a x) (Fin.append b y) =
    if x = y then M a b else 0

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix_append
  {m : ℕ}
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      ℂ)
  (t : ℕ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis m)
  (x y :
    QuantumBlockEncoding.PrimitiveBasis
      t) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.padMatrix
      M t (Fin.append a x)
      (Fin.append b y) =
    if x = y then M a b else 0

Theorem6.29.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pad ry 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/SequentialPrimitiveAssembly.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.29.5●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_ryCount {m : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit m) (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad c
        extra).ryCount =
    c.ryCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_ryCount
  {m : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m)
  (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad
        c extra).ryCount =
    c.ryCount

Theorem6.29.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.6●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_cxCount {m : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit m) (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad c
        extra).cxCount =
    c.cxCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_cxCount
  {m : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m)
  (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad
        c extra).cxCount =
    c.cxCount

Theorem6.29.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.7●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_gateCount {m : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit m) (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad c
        extra).gateCount =
    c.gateCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.pad_gateCount
  {m : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m)
  (extra : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.pad
        c extra).gateCount =
    c.gateCount

Definition6.29.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “stage wires”. Preserve bond indices and send the local fresh bit to the new highest wire.

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. Preserve bond indices and send the local fresh bit to the new highest wire.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires (q t : ℕ) :
  Fin (q + 1 + t) ≃ Fin (q + t + 1)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires
  (q t : ℕ) :
  Fin (q + 1 + t) ≃ Fin (q + t + 1)

Preserve bond indices and send the local fresh bit to the new highest wire.

Theorem6.29.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.9●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_fresh
  (q t : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires q t)
      (Fin.castAdd t (Fin.last q)) =
    Fin.last (q + t)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_fresh
  (q t : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires
        q t)
      (Fin.castAdd t (Fin.last q)) =
    Fin.last (q + t)

Theorem6.29.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.10●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_bond
  (q t : ℕ) (i : Fin q) :
  ↑((QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires q t)
        (Fin.castAdd t i.castSucc)) =
    ↑i

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_bond
  (q t : ℕ) (i : Fin q) :
  ↑((QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires
          q t)
        (Fin.castAdd t i.castSucc)) =
    ↑i

Theorem6.29.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.11●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_basis
  (q t : ℕ) (b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis t) (bit : Fin 2) :
  (fun w =>
      Fin.snoc (Fin.append b x) bit
        ((QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires q
            t)
          w)) =
    Fin.append (Fin.snoc b bit) x

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires_basis
  (q t : ℕ)
  (b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis t)
  (bit : Fin 2) :
  (fun w =>
      Fin.snoc (Fin.append b x) bit
        ((QuantumBlockEncoding.SequentialPrimitiveAssembly.stageWires
            q t)
          w)) =
    Fin.append (Fin.snoc b bit) x

Definition6.29.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “place 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. 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/SequentialPrimitiveAssembly.lean:108. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.29.12●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage {q : ℕ}
  (t : ℕ) (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  QuantumBlockEncoding.PrimitiveCircuit (q + t + 1)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage
  {q : ℕ} (t : ℕ)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + t + 1)

Definition6.29.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “placed 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. 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/SequentialPrimitiveAssembly.lean:112. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.29.13●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix {q : ℕ}
  (t : ℕ)
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℂ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis (q + t + 1))
    (QuantumBlockEncoding.PrimitiveBasis (q + t + 1)) ℂ

def QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix
  {q : ℕ} (t : ℕ)
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℂ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      (q + t + 1))
    (QuantumBlockEncoding.PrimitiveBasis
      (q + t + 1))
    ℂ

Theorem6.29.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval place stage”; 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/SequentialPrimitiveAssembly.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.29.14●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_placeStage {q : ℕ}
  (t : ℕ) (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage t
        c) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix t
      (QuantumBlockEncoding.evalPrimitiveCircuit c)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_placeStage
  {q : ℕ} (t : ℕ)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage
        t c) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix
      t
      (QuantumBlockEncoding.evalPrimitiveCircuit
        c)

Theorem6.29.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.15●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix_apply
  {q : ℕ} (t : ℕ)
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis (q + 1)) ℂ)
  (a b : QuantumBlockEncoding.PrimitiveBasis q)
  (x y : QuantumBlockEncoding.PrimitiveBasis t) (u v : Fin 2) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix t M
      (Fin.snoc (Fin.append a x) u) (Fin.snoc (Fin.append b y) v) =
    if x = y then M (Fin.snoc a u) (Fin.snoc b v) else 0

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix_apply
  {q : ℕ} (t : ℕ)
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      (QuantumBlockEncoding.PrimitiveBasis
        (q + 1))
      ℂ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x y :
    QuantumBlockEncoding.PrimitiveBasis t)
  (u v : Fin 2) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.placedMatrix
      t M (Fin.snoc (Fin.append a x) u)
      (Fin.snoc (Fin.append b y) v) =
    if x = y then
      M (Fin.snoc a u) (Fin.snoc b v)
    else 0

Theorem6.29.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.16●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_ryCount
  {q : ℕ} (t : ℕ) (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage t
        c).ryCount =
    c.ryCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_ryCount
  {q : ℕ} (t : ℕ)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage
        t c).ryCount =
    c.ryCount

Theorem6.29.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.17●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_cxCount
  {q : ℕ} (t : ℕ) (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage t
        c).cxCount =
    c.cxCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_cxCount
  {q : ℕ} (t : ℕ)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage
        t c).cxCount =
    c.cxCount

Theorem6.29.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “place 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/SequentialPrimitiveAssembly.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.29.18●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_gateCount
  {q : ℕ} (t : ℕ) (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage t
        c).gateCount =
    c.gateCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage_gateCount
  {q : ℕ} (t : ℕ)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.placeStage
        t c).gateCount =
    c.gateCount

Definition6.29.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “assemble”. Assemble one actual primitive list, with each bond stage on its final 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. Assemble one actual primitive list, with each bond stage on its final wires.

Declaration kind. def.

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

Lean code for Definition6.29.19●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble (q : ℕ)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit (q + n)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + n)

Assemble one actual primitive list, with each bond stage on its final wires.

Definition6.29.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “assembled 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. 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/SequentialPrimitiveAssembly.lean:146. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.29.20●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix (q : ℕ)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis (q + n))
    (QuantumBlockEncoding.PrimitiveBasis (q + n)) ℂ

def QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      (q + n))
    (QuantumBlockEncoding.PrimitiveBasis
      (q + n))
    ℂ

Theorem6.29.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.21●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_assemble (q : ℕ)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble q
        stages n) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix q
      stages n

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.eval_assemble
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble
        q stages n) =
    QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix
      q stages n

Theorem6.29.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.22●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix_clean_column
  (q : ℕ) (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n : ℕ) (a b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis n) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix q
      stages n (Fin.append b x) (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary a) n
      (x, b)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix_clean_column
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  QuantumBlockEncoding.SequentialPrimitiveAssembly.assembledMatrix
      q stages n (Fin.append b x)
      (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
        a)
      n (x, b)

Theorem6.29.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “assemble clean column”; the hypotheses and conclusion in the code panel fix its exact scope. A flattened primitive circuit has exactly the sequential state action; the fresh data inputs are all zero and every output amplitude is covered.

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

Technical source note. A flattened primitive circuit has exactly the sequential state action; the fresh data inputs are all zero and every output amplitude is covered.

Declaration kind. theorem.

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

Lean code for Theorem6.29.23●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble_clean_column
  (q : ℕ) (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n : ℕ) (a b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble q
        stages n)
      (Fin.append b x) (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary a) n
      (x, b)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble_clean_column
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble
        q stages n)
      (Fin.append b x)
      (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
        a)
      n (x, b)

A flattened primitive circuit has exactly the sequential state action;
the fresh data inputs are all zero and every output amplitude is covered.

Theorem6.29.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.24●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.run_boundary_decomposition
  {q : ℕ}
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        (QuantumBlockEncoding.PrimitiveBasis q))
  (v : QuantumBlockEncoding.PrimitiveBasis q → ℂ) (n : ℕ)
  (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  QuantumBlockEncoding.SequentialBondPreparation.run U v n (x, b) =
    ∑ a,
      QuantumBlockEncoding.SequentialBondPreparation.run U
          (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
            a)
          n (x, b) *
        v a

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.run_boundary_decomposition
  {q : ℕ}
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        (QuantumBlockEncoding.PrimitiveBasis
          q))
  (v :
    QuantumBlockEncoding.PrimitiveBasis
        q →
      ℂ)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U v n (x, b) =
    ∑ a,
      QuantumBlockEncoding.SequentialBondPreparation.run
          U
          (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
            a)
          n (x, b) *
        v a

Definition6.29.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “with initial”. The initial bond vector is prepared by an actual circuit, never supplied as a free state.

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. The initial bond vector is prepared by an actual circuit, never supplied as a free state. Its gate cost is added to the sequential-stage costs.

Declaration kind. def.

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

Lean code for Definition6.29.25●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial {q : ℕ}
  (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit (q + n)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (q + n)

The initial bond vector is prepared by an actual circuit, never supplied
as a free state. Its gate cost is added to the sequential-stage costs.

Theorem6.29.26

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.26●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_column
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ)
  (a b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
        initial stages n)
      (Fin.append b x) (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c => QuantumBlockEncoding.evalPrimitiveCircuit initial c a) n
      (x, b)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_column
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
        initial stages n)
      (Fin.append b x)
      (Fin.append a fun x => 0) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c =>
        QuantumBlockEncoding.evalPrimitiveCircuit
          initial c a)
      n (x, b)

Theorem6.29.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.27●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

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

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

Theorem6.29.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.28●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

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

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

Theorem6.29.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.29●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble_noOracle
  (q : ℕ) (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble q stages
          n).resource.oracleCalls =
    0

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble_noOracle
  (q : ℕ)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.assemble
          q stages
          n).resource.oracleCalls =
    0

Theorem6.29.30

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.30●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_ryCount
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial initial
        stages n).ryCount =
    initial.ryCount + ∑ t ∈ Finset.range n, (stages t).ryCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_ryCount
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
        initial stages n).ryCount =
    initial.ryCount +
      ∑ t ∈ Finset.range n,
        (stages t).ryCount

Theorem6.29.31

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.31●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_cxCount
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial initial
        stages n).cxCount =
    initial.cxCount + ∑ t ∈ Finset.range n, (stages t).cxCount

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_cxCount
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
        initial stages n).cxCount =
    initial.cxCount +
      ∑ t ∈ Finset.range n,
        (stages t).cxCount

Theorem6.29.32

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.32●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_primitive_bound
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n bound : ℕ)
  (h : ∀ t < n, (stages t).ryCount + (stages t).cxCount ≤ bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial initial
          stages n).ryCount +
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
          initial stages n).cxCount ≤
    initial.ryCount + initial.cxCount + n * bound

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial_primitive_bound
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n bound : ℕ)
  (h :
    ∀ t < n,
      (stages t).ryCount +
          (stages t).cxCount ≤
        bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
          initial stages n).ryCount +
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.withInitial
          initial stages n).cxCount ≤
    initial.ryCount + initial.cxCount +
      n * bound

Definition6.29.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “output wires”. Place the first emitted bit at the most-significant data wire, and the bond after the data register.

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. Place the first emitted bit at the most-significant data wire, and the bond after the data register. This relabels every instruction, not the state.

Declaration kind. def.

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

Lean code for Definition6.29.33●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires (q n : ℕ) :
  Fin (q + n) ≃ Fin (n + q)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires
  (q n : ℕ) : Fin (q + n) ≃ Fin (n + q)

Place the first emitted bit at the most-significant data wire, and the
bond after the data register. This relabels every instruction, not the state.

Theorem6.29.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.34●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires_basis
  (q n : ℕ) (b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis n) :
  (fun w =>
      Fin.append x b
        ((QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires q
            n)
          w)) =
    Fin.append b fun i => x i.rev

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires_basis
  (q n : ℕ)
  (b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  (fun w =>
      Fin.append x b
        ((QuantumBlockEncoding.SequentialPrimitiveAssembly.outputWires
            q n)
          w)) =
    Fin.append b fun i => x i.rev

Definition6.29.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “public circuit”. Physical output convention: low data wires are little-endian, clean bond wires follow them.

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. Physical output convention: low data wires are little-endian, clean bond wires follow them. Both preparation and stages incur their actual gate costs.

Declaration kind. def.

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

Lean code for Definition6.29.35●1 definition

defdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

def QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit {q : ℕ}
  (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit (n + q)

def QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ) :
  QuantumBlockEncoding.PrimitiveCircuit
    (n + q)

Physical output convention: low data wires are little-endian, clean bond
wires follow them. Both preparation and stages incur their actual gate costs.

Theorem6.29.36

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.36●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit_column
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1)) (n : ℕ)
  (a b : QuantumBlockEncoding.PrimitiveBasis q)
  (x : QuantumBlockEncoding.PrimitiveBasis n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
        initial stages n)
      (Fin.append x b) (Fin.append (fun x => 0) a) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c => QuantumBlockEncoding.evalPrimitiveCircuit initial c a) n
      (fun i => x i.rev, b)

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit_column
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n : ℕ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis q)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
        initial stages n)
      (Fin.append x b)
      (Fin.append (fun x => 0) a) =
    QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (stages t))
      (fun c =>
        QuantumBlockEncoding.evalPrimitiveCircuit
          initial c a)
      n (fun i => x i.rev, b)

Theorem6.29.37

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.29.37●1 theorem

theoremdefined in QuantumBlockEncoding/SequentialPrimitiveAssembly.lean

complete

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit_primitive_bound
  {q : ℕ} (initial : QuantumBlockEncoding.PrimitiveCircuit q)
  (stages : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (n bound : ℕ)
  (h : ∀ t < n, (stages t).ryCount + (stages t).cxCount ≤ bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
          initial stages n).ryCount +
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
          initial stages n).cxCount ≤
    initial.ryCount + initial.cxCount + n * bound

theorem QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit_primitive_bound
  {q : ℕ}
  (initial :
    QuantumBlockEncoding.PrimitiveCircuit
      q)
  (stages :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (n bound : ℕ)
  (h :
    ∀ t < n,
      (stages t).ryCount +
          (stages t).cxCount ≤
        bound) :
  (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
          initial stages n).ryCount +
      (QuantumBlockEncoding.SequentialPrimitiveAssembly.publicCircuit
          initial stages n).cxCount ≤
    initial.ryCount + initial.cxCount +
      n * bound