6.21. QuantumBlockEncoding/PrimitiveWireRename.lean🔗

12 explicit public declarations, in source order.

Definition6.21.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.21.1●1 definition

defdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

def QuantumBlockEncoding.PrimitiveWireRename.basisEquiv {m n : ℕ}
  (e : Fin m ≃ Fin n) :
  QuantumBlockEncoding.PrimitiveBasis m ≃
    QuantumBlockEncoding.PrimitiveBasis n

def QuantumBlockEncoding.PrimitiveWireRename.basisEquiv
  {m n : ℕ} (e : Fin m ≃ Fin n) :
  QuantumBlockEncoding.PrimitiveBasis m ≃
    QuantumBlockEncoding.PrimitiveBasis n

Definition6.21.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.21.2●1 definition

defdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

def QuantumBlockEncoding.PrimitiveWireRename.gate {m n : ℕ}
  (e : Fin m ≃ Fin n) :
  QuantumBlockEncoding.PrimitiveGate m →
    QuantumBlockEncoding.PrimitiveGate n

def QuantumBlockEncoding.PrimitiveWireRename.gate
  {m n : ℕ} (e : Fin m ≃ Fin n) :
  QuantumBlockEncoding.PrimitiveGate m →
    QuantumBlockEncoding.PrimitiveGate n

Definition6.21.3

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.21.3●1 definition

defdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

def QuantumBlockEncoding.PrimitiveWireRename.circuit {m n : ℕ}
  (e : Fin m ≃ Fin n) (c : QuantumBlockEncoding.PrimitiveCircuit m) :
  QuantumBlockEncoding.PrimitiveCircuit n

def QuantumBlockEncoding.PrimitiveWireRename.circuit
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m) :
  QuantumBlockEncoding.PrimitiveCircuit n

Definition6.21.4

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.21.4●1 definition

defdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

def QuantumBlockEncoding.PrimitiveWireRename.matrix {m n : ℕ}
  (e : Fin m ≃ Fin n)
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis m)
      (QuantumBlockEncoding.PrimitiveBasis m) ℂ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis n)
    (QuantumBlockEncoding.PrimitiveBasis n) ℂ

def QuantumBlockEncoding.PrimitiveWireRename.matrix
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      ℂ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      n)
    (QuantumBlockEncoding.PrimitiveBasis
      n)
    ℂ

Theorem6.21.5

uses 0used by 0✓L∃∀N

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

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.matrix_apply {m n : ℕ}
  (e : Fin m ≃ Fin n)
  (M :
    Matrix (QuantumBlockEncoding.PrimitiveBasis m)
      (QuantumBlockEncoding.PrimitiveBasis m) ℂ)
  (a b : QuantumBlockEncoding.PrimitiveBasis n) :
  QuantumBlockEncoding.PrimitiveWireRename.matrix e M a b =
    M (fun w => a (e w)) fun w => b (e w)

theorem QuantumBlockEncoding.PrimitiveWireRename.matrix_apply
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (M :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      ℂ)
  (a b :
    QuantumBlockEncoding.PrimitiveBasis
      n) :
  QuantumBlockEncoding.PrimitiveWireRename.matrix
      e M a b =
    M (fun w => a (e w)) fun w => b (e w)

Theorem6.21.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.21.6●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.matrix_mul {m n : ℕ}
  (e : Fin m ≃ Fin n)
  (M N :
    Matrix (QuantumBlockEncoding.PrimitiveBasis m)
      (QuantumBlockEncoding.PrimitiveBasis m) ℂ) :
  QuantumBlockEncoding.PrimitiveWireRename.matrix e (M * N) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix e M *
      QuantumBlockEncoding.PrimitiveWireRename.matrix e N

theorem QuantumBlockEncoding.PrimitiveWireRename.matrix_mul
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (M N :
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      (QuantumBlockEncoding.PrimitiveBasis
        m)
      ℂ) :
  QuantumBlockEncoding.PrimitiveWireRename.matrix
      e (M * N) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix
        e M *
      QuantumBlockEncoding.PrimitiveWireRename.matrix
        e N

Theorem6.21.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.21.7●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.oneQubit {m n : ℕ}
  (e : Fin m ≃ Fin n) (t : Fin m) (M : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit (e t) M =
    QuantumBlockEncoding.PrimitiveWireRename.matrix e
      (QuantumBlockEncoding.liftPrimitiveOneQubit t M)

theorem QuantumBlockEncoding.PrimitiveWireRename.oneQubit
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (t : Fin m)
  (M : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      (e t) M =
    QuantumBlockEncoding.PrimitiveWireRename.matrix
      e
      (QuantumBlockEncoding.liftPrimitiveOneQubit
        t M)

Theorem6.21.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.21.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.eval_gate {m n : ℕ}
  (e : Fin m ≃ Fin n) (g : QuantumBlockEncoding.PrimitiveGate m) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveWireRename.gate e g) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix e
      (QuantumBlockEncoding.evalPrimitiveGate g)

theorem QuantumBlockEncoding.PrimitiveWireRename.eval_gate
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (g :
    QuantumBlockEncoding.PrimitiveGate
      m) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveWireRename.gate
        e g) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix
      e
      (QuantumBlockEncoding.evalPrimitiveGate
        g)

Theorem6.21.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval circuit”; the hypotheses and conclusion in the code panel fix its exact scope. One actual renamed primitive list, with both boundary index maps exposed.

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

Technical source note. One actual renamed primitive list, with both boundary index maps exposed.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.eval_circuit {m n : ℕ}
  (e : Fin m ≃ Fin n) (c : QuantumBlockEncoding.PrimitiveCircuit m) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.PrimitiveWireRename.circuit e c) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix e
      (QuantumBlockEncoding.evalPrimitiveCircuit c)

theorem QuantumBlockEncoding.PrimitiveWireRename.eval_circuit
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.PrimitiveWireRename.circuit
        e c) =
    QuantumBlockEncoding.PrimitiveWireRename.matrix
      e
      (QuantumBlockEncoding.evalPrimitiveCircuit
        c)

One actual renamed primitive list, with both boundary index maps exposed.

Theorem6.21.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.21.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.gateCount {m n : ℕ}
  (e : Fin m ≃ Fin n) (c : QuantumBlockEncoding.PrimitiveCircuit m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit e c).gateCount =
    c.gateCount

theorem QuantumBlockEncoding.PrimitiveWireRename.gateCount
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit
        e c).gateCount =
    c.gateCount

Theorem6.21.11

uses 0used by 0✓L∃∀N

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

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.ryCount {m n : ℕ}
  (e : Fin m ≃ Fin n) (c : QuantumBlockEncoding.PrimitiveCircuit m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit e c).ryCount =
    c.ryCount

theorem QuantumBlockEncoding.PrimitiveWireRename.ryCount
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit
        e c).ryCount =
    c.ryCount

Theorem6.21.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.21.12●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveWireRename.lean

complete

theorem QuantumBlockEncoding.PrimitiveWireRename.cxCount {m n : ℕ}
  (e : Fin m ≃ Fin n) (c : QuantumBlockEncoding.PrimitiveCircuit m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit e c).cxCount =
    c.cxCount

theorem QuantumBlockEncoding.PrimitiveWireRename.cxCount
  {m n : ℕ} (e : Fin m ≃ Fin n)
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      m) :
  (QuantumBlockEncoding.PrimitiveWireRename.circuit
        e c).cxCount =
    c.cxCount