6.6. QuantumBlockEncoding/PrimitiveMacros.lean🔗

43 explicit public declarations, in source order.

Definition6.6.1

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.1●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.hadamardMatrix : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.hadamardMatrix :
  Matrix (Fin 2) (Fin 2) ℂ

Definition6.6.2

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.2●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.phaseMatrix (theta : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.phaseMatrix
  (theta : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

Theorem6.6.3

uses 0used by 0✓L∃∀N

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveMacros.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.6.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.hadamardMatrix_apply (row column : Fin 2) :
  QuantumBlockEncoding.hadamardMatrix row column =
    have scale := ↑(√2 / 2);
    match ↑row, ↑column with
    | 0, 0 => scale
    | 0, 1 => scale
    | 1, 0 => scale
    | x, x_1 => -scale

theorem QuantumBlockEncoding.hadamardMatrix_apply
  (row column : Fin 2) :
  QuantumBlockEncoding.hadamardMatrix row
      column =
    have scale := ↑(√2 / 2);
    match ↑row, ↑column with
    | 0, 0 => scale
    | 0, 1 => scale
    | 1, 0 => scale
    | x, x_1 => -scale

Theorem6.6.4

uses 0used by 0✓L∃∀N

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.phaseMatrix_apply (theta : ℝ)
  (row column : Fin 2) :
  QuantumBlockEncoding.phaseMatrix theta row column =
    if row = column then
      if row = 0 then 1 else Complex.exp (↑theta * Complex.I)
    else 0

theorem QuantumBlockEncoding.phaseMatrix_apply
  (theta : ℝ) (row column : Fin 2) :
  QuantumBlockEncoding.phaseMatrix theta
      row column =
    if row = column then
      if row = 0 then 1
      else
        Complex.exp (↑theta * Complex.I)
    else 0

Definition6.6.5

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.5●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveHProgram {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveHProgram
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Definition6.6.6

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.6●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveTProgram {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveTProgram
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Definition6.6.7

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.7●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveTdgProgram {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveTdgProgram
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Theorem6.6.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval global phase pi div two”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.evalGlobalPhase_pi_div_two :
  QuantumBlockEncoding.evalGlobalPhase
      (QuantumBlockEncoding.ExactAngle.piRational (1 / 2)) =
    Complex.I

theorem QuantumBlockEncoding.evalGlobalPhase_pi_div_two :
  QuantumBlockEncoding.evalGlobalPhase
      (QuantumBlockEncoding.ExactAngle.piRational
        (1 / 2)) =
    Complex.I

Theorem6.6.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift primitive one qubit 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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.9●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_mul {qubits : ℕ}
  (target : Fin qubits) (left right : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target (left * right) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target left *
      QuantumBlockEncoding.liftPrimitiveOneQubit target right

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_mul
  {qubits : ℕ} (target : Fin qubits)
  (left right :
    Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target (left * right) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
        target left *
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target right

Theorem6.6.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smul lift primitive 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.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.smul_liftPrimitiveOneQubit {qubits : ℕ}
  (target : Fin qubits) (scalar : ℂ) (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  scalar • QuantumBlockEncoding.liftPrimitiveOneQubit target gate =
    QuantumBlockEncoding.liftPrimitiveOneQubit target (scalar • gate)

theorem QuantumBlockEncoding.smul_liftPrimitiveOneQubit
  {qubits : ℕ} (target : Fin qubits)
  (scalar : ℂ)
  (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  scalar •
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target gate =
    QuantumBlockEncoding.liftPrimitiveOneQubit
      target (scalar • gate)

Theorem6.6.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive h program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/PrimitiveMacros.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.6.11●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveHProgram_eval {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveHProgram target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target
      QuantumBlockEncoding.hadamardMatrix

theorem QuantumBlockEncoding.primitiveHProgram_eval
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveHProgram
        target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
      target
      QuantumBlockEncoding.hadamardMatrix

Theorem6.6.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive t program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.12●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveTProgram_eval {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTProgram target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target
      (QuantumBlockEncoding.phaseMatrix (Real.pi / 4))

theorem QuantumBlockEncoding.primitiveTProgram_eval
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTProgram
        target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
      target
      (QuantumBlockEncoding.phaseMatrix
        (Real.pi / 4))

Theorem6.6.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive tdg program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.13●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveTdgProgram_eval {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTdgProgram target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target
      (QuantumBlockEncoding.phaseMatrix (-Real.pi / 4))

theorem QuantumBlockEncoding.primitiveTdgProgram_eval
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTdgProgram
        target) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
      target
      (QuantumBlockEncoding.phaseMatrix
        (-Real.pi / 4))

Definition6.6.14

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.14●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.phasePermutationMatrix.{u_1} {index : Type u_1}
  [Fintype index] [DecidableEq index] (phase : index → ℂ)
  (permutation : index ≃ index) : Matrix index index ℂ

def QuantumBlockEncoding.phasePermutationMatrix.{u_1}
  {index : Type u_1} [Fintype index]
  [DecidableEq index] (phase : index → ℂ)
  (permutation : index ≃ index) :
  Matrix index index ℂ

Theorem6.6.15

uses 0used by 0✓L∃∀N

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.15●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.phasePermutationMatrix_mul.{u_1} {index : Type u_1}
  [Fintype index] [DecidableEq index] (leftPhase rightPhase : index → ℂ)
  (leftPerm rightPerm : index ≃ index) :
  QuantumBlockEncoding.phasePermutationMatrix rightPhase rightPerm *
      QuantumBlockEncoding.phasePermutationMatrix leftPhase leftPerm =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state => leftPhase state * rightPhase (leftPerm state))
      (leftPerm.trans rightPerm)

theorem QuantumBlockEncoding.phasePermutationMatrix_mul.{u_1}
  {index : Type u_1} [Fintype index]
  [DecidableEq index]
  (leftPhase rightPhase : index → ℂ)
  (leftPerm rightPerm : index ≃ index) :
  QuantumBlockEncoding.phasePermutationMatrix
        rightPhase rightPerm *
      QuantumBlockEncoding.phasePermutationMatrix
        leftPhase leftPerm =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        leftPhase state *
          rightPhase (leftPerm state))
      (leftPerm.trans rightPerm)

Theorem6.6.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive cx eq phase permutation matrix”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.16●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveCx_eq_phasePermutationMatrix
  {qubits : ℕ} (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.cx control target distinct) =
    QuantumBlockEncoding.phasePermutationMatrix (fun x => 1)
      (QuantumBlockEncoding.cxBasisEquiv control target distinct)

theorem QuantumBlockEncoding.evalPrimitiveCx_eq_phasePermutationMatrix
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.cx
        control target distinct) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun x => 1)
      (QuantumBlockEncoding.cxBasisEquiv
        control target distinct)

Theorem6.6.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift phase matrix eq phase permutation matrix”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.17●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.liftPhaseMatrix_eq_phasePermutationMatrix
  {qubits : ℕ} (target : Fin qubits) (theta : ℝ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target
      (QuantumBlockEncoding.phaseMatrix theta) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else Complex.exp (↑theta * Complex.I))
      (Equiv.refl (QuantumBlockEncoding.PrimitiveBasis qubits))

theorem QuantumBlockEncoding.liftPhaseMatrix_eq_phasePermutationMatrix
  {qubits : ℕ} (target : Fin qubits)
  (theta : ℝ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target
      (QuantumBlockEncoding.phaseMatrix
        theta) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else
          Complex.exp
            (↑theta * Complex.I))
      (Equiv.refl
        (QuantumBlockEncoding.PrimitiveBasis
          qubits))

Definition6.6.18

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.18●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveCxProgram {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveCxProgram
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Theorem6.6.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive cx program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.19●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveCxProgram_eval {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCxProgram control target
        distinct) =
    QuantumBlockEncoding.phasePermutationMatrix (fun x => 1)
      (QuantumBlockEncoding.cxBasisEquiv control target distinct)

theorem QuantumBlockEncoding.primitiveCxProgram_eval
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCxProgram
        control target distinct) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun x => 1)
      (QuantumBlockEncoding.cxBasisEquiv
        control target distinct)

Theorem6.6.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive t program eval monomial”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.20●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveTProgram_eval_monomial {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTProgram target) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else Complex.exp (↑(Real.pi / 4) * Complex.I))
      (Equiv.refl (QuantumBlockEncoding.PrimitiveBasis qubits))

theorem QuantumBlockEncoding.primitiveTProgram_eval_monomial
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTProgram
        target) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else
          Complex.exp
            (↑(Real.pi / 4) * Complex.I))
      (Equiv.refl
        (QuantumBlockEncoding.PrimitiveBasis
          qubits))

Theorem6.6.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive tdg program eval monomial”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.21●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveTdgProgram_eval_monomial {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTdgProgram target) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else Complex.exp (↑(-Real.pi / 4) * Complex.I))
      (Equiv.refl (QuantumBlockEncoding.PrimitiveBasis qubits))

theorem QuantumBlockEncoding.primitiveTdgProgram_eval_monomial
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveTdgProgram
        target) =
    QuantumBlockEncoding.phasePermutationMatrix
      (fun state =>
        if state target = 0 then 1
        else
          Complex.exp
            (↑(-Real.pi / 4) * Complex.I))
      (Equiv.refl
        (QuantumBlockEncoding.PrimitiveBasis
          qubits))

Definition6.6.22

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “monomial program”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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. structure.

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

Lean code for Definition6.6.22●1 definition

structure(4 fields)defined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

structure QuantumBlockEncoding.MonomialProgram (qubits : ℕ) : Type

structure QuantumBlockEncoding.MonomialProgram
  (qubits : ℕ) : Type

Fields

program : QuantumBlockEncoding.PrimitiveProgram qubits

phase : QuantumBlockEncoding.PrimitiveBasis qubits → ℂ

permutation : QuantumBlockEncoding.PrimitiveBasis qubits ≃ QuantumBlockEncoding.PrimitiveBasis qubits

exact : QuantumBlockEncoding.evalPrimitiveProgram self.program =
  QuantumBlockEncoding.phasePermutationMatrix self.phase self.permutation

Definition6.6.23

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.23●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.MonomialProgram.seq {qubits : ℕ}
  (left right : QuantumBlockEncoding.MonomialProgram qubits) :
  QuantumBlockEncoding.MonomialProgram qubits

def QuantumBlockEncoding.MonomialProgram.seq
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.MonomialProgram
      qubits) :
  QuantumBlockEncoding.MonomialProgram
    qubits

Definition6.6.24

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.24●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.MonomialProgram.cx {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.MonomialProgram qubits

def QuantumBlockEncoding.MonomialProgram.cx
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.MonomialProgram
    qubits

Definition6.6.25

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.25●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.MonomialProgram.t {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.MonomialProgram qubits

def QuantumBlockEncoding.MonomialProgram.t
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.MonomialProgram
    qubits

Definition6.6.26

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.26●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.MonomialProgram.tdg {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.MonomialProgram qubits

def QuantumBlockEncoding.MonomialProgram.tdg
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.MonomialProgram
    qubits

Definition6.6.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive ccx middle”. The phase-only middle of the standard exact Toffoli decomposition.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The phase-only middle of the standard exact Toffoli decomposition.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveCCXMiddle {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.MonomialProgram qubits

def QuantumBlockEncoding.primitiveCCXMiddle
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.MonomialProgram
    qubits

The phase-only middle of the standard exact Toffoli decomposition.

Definition6.6.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive ccx program”. The exact primitive program uses the requested H/T/Tdg/CX chronology.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The exact primitive program uses the requested H/T/Tdg/CX chronology.

Declaration kind. def.

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

Lean code for Definition6.6.28●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveCCXProgram {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveCCXProgram
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

The exact primitive program uses the requested H/T/Tdg/CX chronology.

Theorem6.6.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive ccx middle permutation eq refl”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.29●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveCCXMiddle_permutation_eq_refl {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  (QuantumBlockEncoding.primitiveCCXMiddle a b target a_ne_b a_ne_target
        b_ne_target).permutation =
    Equiv.refl (QuantumBlockEncoding.PrimitiveBasis qubits)

theorem QuantumBlockEncoding.primitiveCCXMiddle_permutation_eq_refl
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  (QuantumBlockEncoding.primitiveCCXMiddle
        a b target a_ne_b a_ne_target
        b_ne_target).permutation =
    Equiv.refl
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)

Theorem6.6.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive ccx middle phase eq ccz”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.30●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveCCXMiddle_phase_eq_ccz {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits) :
  (QuantumBlockEncoding.primitiveCCXMiddle a b target a_ne_b a_ne_target
          b_ne_target).phase
      state =
    if state a = 1 ∧ state b = 1 ∧ state target = 1 then -1 else 1

theorem QuantumBlockEncoding.primitiveCCXMiddle_phase_eq_ccz
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  (QuantumBlockEncoding.primitiveCCXMiddle
          a b target a_ne_b a_ne_target
          b_ne_target).phase
      state =
    if
        state a = 1 ∧
          state b = 1 ∧
            state target = 1 then
      -1
    else 1

Definition6.6.31

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.31●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.cczMatrix {qubits : ℕ} (a b target : Fin qubits) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.cczMatrix
  {qubits : ℕ} (a b target : Fin qubits) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℂ

Theorem6.6.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive ccx middle eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.32●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveCCXMiddle_eval {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCCXMiddle a b target a_ne_b
          a_ne_target b_ne_target).program =
    QuantumBlockEncoding.cczMatrix a b target

theorem QuantumBlockEncoding.primitiveCCXMiddle_eval
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCCXMiddle
          a b target a_ne_b a_ne_target
          b_ne_target).program =
    QuantumBlockEncoding.cczMatrix a b
      target

Definition6.6.33

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.33●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.zMatrix : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.zMatrix :
  Matrix (Fin 2) (Fin 2) ℂ

Theorem6.6.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard mul hadamard”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.34●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.hadamard_mul_hadamard :
  QuantumBlockEncoding.hadamardMatrix *
      QuantumBlockEncoding.hadamardMatrix =
    1

theorem QuantumBlockEncoding.hadamard_mul_hadamard :
  QuantumBlockEncoding.hadamardMatrix *
      QuantumBlockEncoding.hadamardMatrix =
    1

Theorem6.6.35

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard mul z mul hadamard”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.35●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.hadamard_mul_z_mul_hadamard :
  QuantumBlockEncoding.hadamardMatrix * QuantumBlockEncoding.zMatrix *
      QuantumBlockEncoding.hadamardMatrix =
    QuantumBlockEncoding.xMatrix

theorem QuantumBlockEncoding.hadamard_mul_z_mul_hadamard :
  QuantumBlockEncoding.hadamardMatrix *
        QuantumBlockEncoding.zMatrix *
      QuantumBlockEncoding.hadamardMatrix =
    QuantumBlockEncoding.xMatrix

Theorem6.6.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift primitive one qubit eq block diagonal”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.36●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_eq_blockDiagonal {qubits : ℕ}
  (target : Fin qubits) (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target gate =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire target).symm)
      (Matrix.blockDiagonal fun x => gate)

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_eq_blockDiagonal
  {qubits : ℕ} (target : Fin qubits)
  (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target gate =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire
            target).symm)
      (Matrix.blockDiagonal fun x => gate)

Definition6.6.37

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.37●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.cczTargetBlock {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (context : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2) :
  Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.cczTargetBlock
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (context :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2) :
  Matrix (Fin 2) (Fin 2) ℂ

Theorem6.6.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “ccz matrix eq block diagonal”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.38●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.cczMatrix_eq_blockDiagonal {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.cczMatrix a b target =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire target).symm)
      (Matrix.blockDiagonal
        (QuantumBlockEncoding.cczTargetBlock a b target a_ne_target
          b_ne_target))

theorem QuantumBlockEncoding.cczMatrix_eq_blockDiagonal
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.cczMatrix a b
      target =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire
            target).symm)
      (Matrix.blockDiagonal
        (QuantumBlockEncoding.cczTargetBlock
          a b target a_ne_target
          b_ne_target))

Definition6.6.39

uses 0used by 0✓L∃∀N

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

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.39●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.ccxTargetBlock {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (context : QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2) :
  Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.ccxTargetBlock
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target)
  (context :
    QuantumBlockEncoding.OtherPrimitiveWires
        target →
      Fin 2) :
  Matrix (Fin 2) (Fin 2) ℂ

Theorem6.6.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “equiv permutation matrix ccx eq block diagonal”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.40●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.equivPermutationMatrix_ccx_eq_blockDiagonal
  {qubits : ℕ} (a b target : Fin qubits) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv a b target a_ne_target
        b_ne_target) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire target).symm)
      (Matrix.blockDiagonal
        (QuantumBlockEncoding.ccxTargetBlock a b target a_ne_target
          b_ne_target))

theorem QuantumBlockEncoding.equivPermutationMatrix_ccx_eq_blockDiagonal
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv
        a b target a_ne_target
        b_ne_target) =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.splitPrimitiveWire
            target).symm)
      (Matrix.blockDiagonal
        (QuantumBlockEncoding.ccxTargetBlock
          a b target a_ne_target
          b_ne_target))

Theorem6.6.41

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hadamard conjugates ccz”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Theorem6.6.41●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.hadamard_conjugates_ccz {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target
          QuantumBlockEncoding.hadamardMatrix *
        QuantumBlockEncoding.cczMatrix a b target *
      QuantumBlockEncoding.liftPrimitiveOneQubit target
        QuantumBlockEncoding.hadamardMatrix =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv a b target a_ne_target
        b_ne_target)

theorem QuantumBlockEncoding.hadamard_conjugates_ccz
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
          target
          QuantumBlockEncoding.hadamardMatrix *
        QuantumBlockEncoding.cczMatrix a b
          target *
      QuantumBlockEncoding.liftPrimitiveOneQubit
        target
        QuantumBlockEncoding.hadamardMatrix =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv
        a b target a_ne_target
        b_ne_target)

Theorem6.6.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive ccx program eval”; the hypotheses and conclusion in the code panel fix its exact scope. The requested H/T/Tdg/CX decomposition is exactly Toffoli, including its global phase.

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

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The requested H/T/Tdg/CX decomposition is exactly Toffoli, including its global phase.

Declaration kind. theorem.

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

Lean code for Theorem6.6.42●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

theorem QuantumBlockEncoding.primitiveCCXProgram_eval {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCCXProgram a b target a_ne_b
        a_ne_target b_ne_target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv a b target a_ne_target
        b_ne_target)

theorem QuantumBlockEncoding.primitiveCCXProgram_eval
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveCCXProgram
        a b target a_ne_b a_ne_target
        b_ne_target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.ccxBasisEquiv
        a b target a_ne_target
        b_ne_target)

The requested H/T/Tdg/CX decomposition is exactly Toffoli, including its
global phase.

Definition6.6.43

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive ccx program refinement”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Lean code for Definition6.6.43●1 definition

defdefined in QuantumBlockEncoding/PrimitiveMacros.lean

complete

def QuantumBlockEncoding.primitiveCCXProgramRefinement {qubits : ℕ}
  (a b target : Fin qubits) (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.PrimitiveProgramRefinement qubits

def QuantumBlockEncoding.primitiveCCXProgramRefinement
  {qubits : ℕ} (a b target : Fin qubits)
  (a_ne_b : a ≠ b)
  (a_ne_target : a ≠ target)
  (b_ne_target : b ≠ target) :
  QuantumBlockEncoding.PrimitiveProgramRefinement
    qubits