6.8. QuantumBlockEncoding/PrimitiveSemantics.lean🔗

54 explicit public declarations, in source order.

Definition6.8.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “standard ry matrix”. Standard 'RY(theta)' in the convention used by Qiskit and OpenQASM 3.

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. Standard 'RY(theta)' in the convention used by Qiskit and OpenQASM 3.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

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

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

Standard `RY(theta)` in the convention used by Qiskit and OpenQASM 3.

Theorem6.8.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix zero”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/PrimitiveSemantics.lean:22. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.8.2●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_zero :
  QuantumBlockEncoding.standardRyMatrix 0 = 1

theorem QuantumBlockEncoding.standardRyMatrix_zero :
  QuantumBlockEncoding.standardRyMatrix
      0 =
    1

Theorem6.8.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix add”; the hypotheses and conclusion in the code panel fix its exact scope. Standard rotations compose by adding their physical angles.

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. Standard rotations compose by adding their physical angles.

Declaration kind. theorem.

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

Lean code for Theorem6.8.3●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_add (left right : ℝ) :
  QuantumBlockEncoding.standardRyMatrix (left + right) =
    QuantumBlockEncoding.standardRyMatrix right *
      QuantumBlockEncoding.standardRyMatrix left

theorem QuantumBlockEncoding.standardRyMatrix_add
  (left right : ℝ) :
  QuantumBlockEncoding.standardRyMatrix
      (left + right) =
    QuantumBlockEncoding.standardRyMatrix
        right *
      QuantumBlockEncoding.standardRyMatrix
        left

Standard rotations compose by adding their physical angles.

Theorem6.8.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star complex cos of real”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/PrimitiveSemantics.lean:39. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.8.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.star_complex_cos_ofReal (theta : ℝ) :
  star (Complex.cos ↑theta) = Complex.cos ↑theta

theorem QuantumBlockEncoding.star_complex_cos_ofReal
  (theta : ℝ) :
  star (Complex.cos ↑theta) =
    Complex.cos ↑theta

Theorem6.8.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “conj complex cos of real”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/PrimitiveSemantics.lean:43. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.8.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.conj_complex_cos_ofReal (theta : ℝ) :
  (starRingEnd ℂ) (Complex.cos ↑theta) = Complex.cos ↑theta

theorem QuantumBlockEncoding.conj_complex_cos_ofReal
  (theta : ℝ) :
  (starRingEnd ℂ) (Complex.cos ↑theta) =
    Complex.cos ↑theta

Theorem6.8.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star complex sin of real”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/PrimitiveSemantics.lean:48. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.8.6●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.star_complex_sin_ofReal (theta : ℝ) :
  star (Complex.sin ↑theta) = Complex.sin ↑theta

theorem QuantumBlockEncoding.star_complex_sin_ofReal
  (theta : ℝ) :
  star (Complex.sin ↑theta) =
    Complex.sin ↑theta

Theorem6.8.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “conj complex sin of real”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/PrimitiveSemantics.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.8.7●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.conj_complex_sin_ofReal (theta : ℝ) :
  (starRingEnd ℂ) (Complex.sin ↑theta) = Complex.sin ↑theta

theorem QuantumBlockEncoding.conj_complex_sin_ofReal
  (theta : ℝ) :
  (starRingEnd ℂ) (Complex.sin ↑theta) =
    Complex.sin ↑theta

Theorem6.8.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “complex of real 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/PrimitiveSemantics.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.8.8●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.complex_ofReal_div_two (theta : ℝ) :
  ↑theta / 2 = ↑(theta / 2)

theorem QuantumBlockEncoding.complex_ofReal_div_two
  (theta : ℝ) : ↑theta / 2 = ↑(theta / 2)

Theorem6.8.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.9●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.conj_complex_cos_ofReal_div_two (theta : ℝ) :
  (starRingEnd ℂ) (Complex.cos (↑theta / 2)) = Complex.cos (↑theta / 2)

theorem QuantumBlockEncoding.conj_complex_cos_ofReal_div_two
  (theta : ℝ) :
  (starRingEnd ℂ)
      (Complex.cos (↑theta / 2)) =
    Complex.cos (↑theta / 2)

Theorem6.8.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.conj_complex_sin_ofReal_div_two (theta : ℝ) :
  (starRingEnd ℂ) (Complex.sin (↑theta / 2)) = Complex.sin (↑theta / 2)

theorem QuantumBlockEncoding.conj_complex_sin_ofReal_div_two
  (theta : ℝ) :
  (starRingEnd ℂ)
      (Complex.sin (↑theta / 2)) =
    Complex.sin (↑theta / 2)

Theorem6.8.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.11●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_neg (theta : ℝ) :
  QuantumBlockEncoding.standardRyMatrix (-theta) =
    star (QuantumBlockEncoding.standardRyMatrix theta)

theorem QuantumBlockEncoding.standardRyMatrix_neg
  (theta : ℝ) :
  QuantumBlockEncoding.standardRyMatrix
      (-theta) =
    star
      (QuantumBlockEncoding.standardRyMatrix
        theta)

Definition6.8.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “x matrix”. Pauli X in the same two-dimensional basis as 'standardRyMatrix'.

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. Pauli X in the same two-dimensional basis as 'standardRyMatrix'.

Declaration kind. def.

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

Lean code for Definition6.8.12●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

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

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

Pauli X in the same two-dimensional basis as `standardRyMatrix`.

Theorem6.8.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “x matrix conjugates standard ry”; 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/PrimitiveSemantics.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.8.13●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.xMatrix_conjugates_standardRy (theta : ℝ) :
  QuantumBlockEncoding.xMatrix *
        QuantumBlockEncoding.standardRyMatrix theta *
      QuantumBlockEncoding.xMatrix =
    QuantumBlockEncoding.standardRyMatrix (-theta)

theorem QuantumBlockEncoding.xMatrix_conjugates_standardRy
  (theta : ℝ) :
  QuantumBlockEncoding.xMatrix *
        QuantumBlockEncoding.standardRyMatrix
          theta *
      QuantumBlockEncoding.xMatrix =
    QuantumBlockEncoding.standardRyMatrix
      (-theta)

Theorem6.8.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.14●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_unitary (theta : ℝ) :
  QuantumBlockEncoding.standardRyMatrix theta ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.standardRyMatrix_unitary
  (theta : ℝ) :
  QuantumBlockEncoding.standardRyMatrix
      theta ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Theorem6.8.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix two arccos eq amplitude rotation”; the hypotheses and conclusion in the code panel fix its exact scope. The exact half-angle correction from standard 'RY' to the logical loader.

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 exact half-angle correction from standard 'RY' to the logical loader.

Declaration kind. theorem.

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

Lean code for Theorem6.8.15●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_two_arccos_eq_amplitudeRotation
  (coefficient : ℝ) (_lower : -1 ≤ coefficient)
  (_upper : coefficient ≤ 1) :
  QuantumBlockEncoding.standardRyMatrix (2 * Real.arccos coefficient) =
    QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation coefficient

theorem QuantumBlockEncoding.standardRyMatrix_two_arccos_eq_amplitudeRotation
  (coefficient : ℝ)
  (_lower : -1 ≤ coefficient)
  (_upper : coefficient ≤ 1) :
  QuantumBlockEncoding.standardRyMatrix
      (2 * Real.arccos coefficient) =
    QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
      coefficient

The exact half-angle correction from standard `RY` to the logical loader.

Theorem6.8.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix pi div two eq warm robin uniform bit prepare”; the hypotheses and conclusion in the code panel fix its exact scope. The symmetry PREPARE is exactly a standard 'RY(pi/2)', not an opaque H.

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 symmetry PREPARE is exactly a standard 'RY(pi/2)', not an opaque H.

Declaration kind. theorem.

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

Lean code for Theorem6.8.16●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRyMatrix_pi_div_two_eq_warmRobinUniformBitPrepare :
  QuantumBlockEncoding.standardRyMatrix (Real.pi / 2) =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare

theorem QuantumBlockEncoding.standardRyMatrix_pi_div_two_eq_warmRobinUniformBitPrepare :
  QuantumBlockEncoding.standardRyMatrix
      (Real.pi / 2) =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare

The symmetry PREPARE is exactly a standard `RY(pi/2)`, not an opaque H.

Definition6.8.17

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “primitive basis”. Computational-basis bit strings with one named coordinate per qubit.

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. Computational-basis bit strings with one named coordinate per qubit.

Declaration kind. abbrev.

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

Lean code for Definition6.8.17●1 definition

abbrevdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

abbrev QuantumBlockEncoding.PrimitiveBasis (qubits : ℕ) : Type

abbrev QuantumBlockEncoding.PrimitiveBasis
  (qubits : ℕ) : Type

Computational-basis bit strings with one named coordinate per qubit.

Definition6.8.18

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.18●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.flipBit (bit : Fin 2) : Fin 2

def QuantumBlockEncoding.flipBit
  (bit : Fin 2) : Fin 2

Theorem6.8.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “flip bit flip bit”; 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/PrimitiveSemantics.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.8.19●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.flipBit_flipBit (bit : Fin 2) :
  QuantumBlockEncoding.flipBit (QuantumBlockEncoding.flipBit bit) = bit

theorem QuantumBlockEncoding.flipBit_flipBit
  (bit : Fin 2) :
  QuantumBlockEncoding.flipBit
      (QuantumBlockEncoding.flipBit bit) =
    bit

Definition6.8.20

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.20●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.xBasisAction {qubits : ℕ} (target : Fin qubits)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.xBasisAction
  {qubits : ℕ} (target : Fin qubits)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.PrimitiveBasis
    qubits

Theorem6.8.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.21●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.xBasisAction_involutive {qubits : ℕ}
  (target : Fin qubits) :
  Function.Involutive (QuantumBlockEncoding.xBasisAction target)

theorem QuantumBlockEncoding.xBasisAction_involutive
  {qubits : ℕ} (target : Fin qubits) :
  Function.Involutive
    (QuantumBlockEncoding.xBasisAction
      target)

Definition6.8.22

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.8.22●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.xBasisEquiv {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.xBasisEquiv
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    QuantumBlockEncoding.PrimitiveBasis
      qubits

Definition6.8.23

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.23●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.cxBasisAction {qubits : ℕ}
  (control target : Fin qubits)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.cxBasisAction
  {qubits : ℕ}
  (control target : Fin qubits)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.PrimitiveBasis
    qubits

Theorem6.8.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.24●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.cxBasisAction_involutive {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  Function.Involutive
    (QuantumBlockEncoding.cxBasisAction control target)

theorem QuantumBlockEncoding.cxBasisAction_involutive
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  Function.Involutive
    (QuantumBlockEncoding.cxBasisAction
      control target)

Definition6.8.25

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.8.25●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.cxBasisEquiv {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.cxBasisEquiv
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    QuantumBlockEncoding.PrimitiveBasis
      qubits

Definition6.8.26

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “other primitive wires”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. 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. abbrev.

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

Lean code for Definition6.8.26●1 definition

abbrevdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

abbrev QuantumBlockEncoding.OtherPrimitiveWires {qubits : ℕ}
  (target : Fin qubits) : Type

abbrev QuantumBlockEncoding.OtherPrimitiveWires
  {qubits : ℕ} (target : Fin qubits) :
  Type

Definition6.8.27

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.27●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.splitPrimitiveWire {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    Fin 2 × (QuantumBlockEncoding.OtherPrimitiveWires target → Fin 2)

def QuantumBlockEncoding.splitPrimitiveWire
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    Fin 2 ×
      (QuantumBlockEncoding.OtherPrimitiveWires
          target →
        Fin 2)

Theorem6.8.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.28●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.splitPrimitiveWire_other_apply {qubits : ℕ}
  (target : Fin qubits)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits)
  (wire : QuantumBlockEncoding.OtherPrimitiveWires target) :
  ((QuantumBlockEncoding.splitPrimitiveWire target) state).2 wire =
    state ↑wire

theorem QuantumBlockEncoding.splitPrimitiveWire_other_apply
  {qubits : ℕ} (target : Fin qubits)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits)
  (wire :
    QuantumBlockEncoding.OtherPrimitiveWires
      target) :
  ((QuantumBlockEncoding.splitPrimitiveWire
            target)
          state).2
      wire =
    state ↑wire

Definition6.8.29

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift primitive one qubit”. Lift a one-qubit matrix to a named wire, leaving every other wire fixed.

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. Lift a one-qubit matrix to a named wire, leaving every other wire fixed.

Declaration kind. def.

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

Lean code for Definition6.8.29●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.liftPrimitiveOneQubit {qubits : ℕ}
  (target : Fin qubits) (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.liftPrimitiveOneQubit
  {qubits : ℕ} (target : Fin qubits)
  (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℂ

Lift a one-qubit matrix to a named wire, leaving every other wire fixed.

Theorem6.8.30

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.30●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_apply {qubits : ℕ}
  (target : Fin qubits) (gate : Matrix (Fin 2) (Fin 2) ℂ)
  (row column : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target gate row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire target) row).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire target)
              column).2 then
      gate (row target) (column target)
    else 0

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_apply
  {qubits : ℕ} (target : Fin qubits)
  (gate : Matrix (Fin 2) (Fin 2) ℂ)
  (row column :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target gate row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              row).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              column).2 then
      gate (row target) (column target)
    else 0

Theorem6.8.31

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift primitive one qubit unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.31●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_unitary {qubits : ℕ}
  (target : Fin qubits) (gate : Matrix (Fin 2) (Fin 2) ℂ)
  (unitary : gate ∈ Matrix.unitaryGroup (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit target gate ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

theorem QuantumBlockEncoding.liftPrimitiveOneQubit_unitary
  {qubits : ℕ} (target : Fin qubits)
  (gate : Matrix (Fin 2) (Fin 2) ℂ)
  (unitary :
    gate ∈
      Matrix.unitaryGroup (Fin 2) ℂ) :
  QuantumBlockEncoding.liftPrimitiveOneQubit
      target gate ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Definition6.8.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “standard rz matrix”. Standard exact 'RZ(theta)' matrix, including its phase convention.

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. Standard exact 'RZ(theta)' matrix, including its phase convention.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

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

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

Standard exact `RZ(theta)` matrix, including its phase convention.

Theorem6.8.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard rz matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.33●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRzMatrix_unitary (theta : ℝ) :
  QuantumBlockEncoding.standardRzMatrix theta ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.standardRzMatrix_unitary
  (theta : ℝ) :
  QuantumBlockEncoding.standardRzMatrix
      theta ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Theorem6.8.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.34●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.standardRzMatrix_neg (theta : ℝ) :
  QuantumBlockEncoding.standardRzMatrix (-theta) =
    star (QuantumBlockEncoding.standardRzMatrix theta)

theorem QuantumBlockEncoding.standardRzMatrix_neg
  (theta : ℝ) :
  QuantumBlockEncoding.standardRzMatrix
      (-theta) =
    star
      (QuantumBlockEncoding.standardRzMatrix
        theta)

Theorem6.8.35

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.35●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.star_equivPermutationMatrix.{u_1}
  {index : Type u_1} [Fintype index] [DecidableEq index]
  (equiv : index ≃ index) :
  star
      (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        equiv) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      equiv.symm

theorem QuantumBlockEncoding.star_equivPermutationMatrix.{u_1}
  {index : Type u_1} [Fintype index]
  [DecidableEq index]
  (equiv : index ≃ index) :
  star
      (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        equiv) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      equiv.symm

Theorem6.8.36

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.36●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.star_liftPrimitiveOneQubit {qubits : ℕ}
  (target : Fin qubits) (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  star (QuantumBlockEncoding.liftPrimitiveOneQubit target gate) =
    QuantumBlockEncoding.liftPrimitiveOneQubit target (star gate)

theorem QuantumBlockEncoding.star_liftPrimitiveOneQubit
  {qubits : ℕ} (target : Fin qubits)
  (gate : Matrix (Fin 2) (Fin 2) ℂ) :
  star
      (QuantumBlockEncoding.liftPrimitiveOneQubit
        target gate) =
    QuantumBlockEncoding.liftPrimitiveOneQubit
      target (star gate)

Definition6.8.37

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval primitive gate”. Exact matrix denotation of one primitive instruction.

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. Exact matrix denotation of one primitive instruction.

Declaration kind. def.

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

Lean code for Definition6.8.37●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.evalPrimitiveGate {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate qubits →
    Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
      (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.evalPrimitiveGate
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Exact matrix denotation of one primitive instruction.

Theorem6.8.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive gate unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.38●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveGate_unitary {qubits : ℕ}
  (gate : QuantumBlockEncoding.PrimitiveGate qubits) :
  QuantumBlockEncoding.evalPrimitiveGate gate ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

theorem QuantumBlockEncoding.evalPrimitiveGate_unitary
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.PrimitiveGate
      qubits) :
  QuantumBlockEncoding.evalPrimitiveGate
      gate ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Theorem6.8.39

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.39●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.xBasisEquiv_symm {qubits : ℕ}
  (target : Fin qubits) :
  (QuantumBlockEncoding.xBasisEquiv target).symm =
    QuantumBlockEncoding.xBasisEquiv target

theorem QuantumBlockEncoding.xBasisEquiv_symm
  {qubits : ℕ} (target : Fin qubits) :
  (QuantumBlockEncoding.xBasisEquiv
        target).symm =
    QuantumBlockEncoding.xBasisEquiv
      target

Theorem6.8.40

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.40●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.cxBasisEquiv_symm {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  (QuantumBlockEncoding.cxBasisEquiv control target distinct).symm =
    QuantumBlockEncoding.cxBasisEquiv control target distinct

theorem QuantumBlockEncoding.cxBasisEquiv_symm
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  (QuantumBlockEncoding.cxBasisEquiv
        control target distinct).symm =
    QuantumBlockEncoding.cxBasisEquiv
      control target distinct

Theorem6.8.41

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.41●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveGate_dagger {qubits : ℕ}
  (gate : QuantumBlockEncoding.PrimitiveGate qubits) :
  QuantumBlockEncoding.evalPrimitiveGate gate.dagger =
    star (QuantumBlockEncoding.evalPrimitiveGate gate)

theorem QuantumBlockEncoding.evalPrimitiveGate_dagger
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.PrimitiveGate
      qubits) :
  QuantumBlockEncoding.evalPrimitiveGate
      gate.dagger =
    star
      (QuantumBlockEncoding.evalPrimitiveGate
        gate)

Definition6.8.42

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval primitive circuit”. Chronological circuit evaluation: later instructions multiply on the left.

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. Chronological circuit evaluation: later instructions multiply on the left.

Declaration kind. def.

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

Lean code for Definition6.8.42●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.evalPrimitiveCircuit {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveCircuit qubits →
    Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
      (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.evalPrimitiveCircuit
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveCircuit
      qubits →
    Matrix
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Chronological circuit evaluation: later instructions multiply on the left.

Theorem6.8.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.43●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveCircuit_unitary {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit circuit ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

theorem QuantumBlockEncoding.evalPrimitiveCircuit_unitary
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      circuit ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Theorem6.8.44

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.8.44●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveCircuit_append {qubits : ℕ}
  (left right : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit (left ++ right) =
    QuantumBlockEncoding.evalPrimitiveCircuit right *
      QuantumBlockEncoding.evalPrimitiveCircuit left

theorem QuantumBlockEncoding.evalPrimitiveCircuit_append
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (left ++ right) =
    QuantumBlockEncoding.evalPrimitiveCircuit
        right *
      QuantumBlockEncoding.evalPrimitiveCircuit
        left

Theorem6.8.45

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.45●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveCircuit_dagger {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (List.map QuantumBlockEncoding.PrimitiveGate.dagger
        (List.reverse circuit)) =
    star (QuantumBlockEncoding.evalPrimitiveCircuit circuit)

theorem QuantumBlockEncoding.evalPrimitiveCircuit_dagger
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (List.map
        QuantumBlockEncoding.PrimitiveGate.dagger
        (List.reverse circuit)) =
    star
      (QuantumBlockEncoding.evalPrimitiveCircuit
        circuit)

Definition6.8.46

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval global phase”. Unit-modulus scalar represented by an exact global phase.

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. Unit-modulus scalar represented by an exact global phase.

Declaration kind. def.

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

Lean code for Definition6.8.46●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.evalGlobalPhase
  (angle : QuantumBlockEncoding.ExactAngle) : ℂ

def QuantumBlockEncoding.evalGlobalPhase
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  ℂ

Unit-modulus scalar represented by an exact global phase.

Theorem6.8.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval global phase unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.47●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalGlobalPhase_unitary
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalGlobalPhase angle ∈ unitary ℂ

theorem QuantumBlockEncoding.evalGlobalPhase_unitary
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalGlobalPhase
      angle ∈
    unitary ℂ

Theorem6.8.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval global phase neg”; 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/PrimitiveSemantics.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.8.48●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalGlobalPhase_neg
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalGlobalPhase angle.neg =
    star (QuantumBlockEncoding.evalGlobalPhase angle)

theorem QuantumBlockEncoding.evalGlobalPhase_neg
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.evalGlobalPhase
      angle.neg =
    star
      (QuantumBlockEncoding.evalGlobalPhase
        angle)

Definition6.8.49

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eval primitive program”. Exact program semantics, with the same 'exp(i phase)' convention used by Qiskit and OpenQASM 3.

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. Exact program semantics, with the same 'exp(i phase)' convention used by Qiskit and OpenQASM 3.

Declaration kind. def.

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

Lean code for Definition6.8.49●1 definition

defdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

def QuantumBlockEncoding.evalPrimitiveProgram {qubits : ℕ}
  (program : QuantumBlockEncoding.PrimitiveProgram qubits) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis qubits)
    (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

def QuantumBlockEncoding.evalPrimitiveProgram
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    (QuantumBlockEncoding.PrimitiveBasis
      qubits)
    ℂ

Exact program semantics, with the same `exp(i phase)` convention used by
Qiskit and OpenQASM 3.

Theorem6.8.50

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.50●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveProgram_identity (qubits : ℕ) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.PrimitiveProgram.identity qubits) =
    1

theorem QuantumBlockEncoding.evalPrimitiveProgram_identity
  (qubits : ℕ) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.PrimitiveProgram.identity
        qubits) =
    1

Theorem6.8.51

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.51●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveProgram_seq {qubits : ℕ}
  (left right : QuantumBlockEncoding.PrimitiveProgram qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram (left.seq right) =
    QuantumBlockEncoding.evalPrimitiveProgram right *
      QuantumBlockEncoding.evalPrimitiveProgram left

theorem QuantumBlockEncoding.evalPrimitiveProgram_seq
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (left.seq right) =
    QuantumBlockEncoding.evalPrimitiveProgram
        right *
      QuantumBlockEncoding.evalPrimitiveProgram
        left

Theorem6.8.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive program unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.8.52●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveProgram_unitary {qubits : ℕ}
  (program : QuantumBlockEncoding.PrimitiveProgram qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram program ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

theorem QuantumBlockEncoding.evalPrimitiveProgram_unitary
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      program ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        qubits)
      ℂ

Theorem6.8.53

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.53●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

theorem QuantumBlockEncoding.evalPrimitiveProgram_dagger {qubits : ℕ}
  (program : QuantumBlockEncoding.PrimitiveProgram qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram program.dagger =
    star (QuantumBlockEncoding.evalPrimitiveProgram program)

theorem QuantumBlockEncoding.evalPrimitiveProgram_dagger
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      program.dagger =
    star
      (QuantumBlockEncoding.evalPrimitiveProgram
        program)

Definition6.8.54

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “primitive refinement”. A proposition-valued field is a requirement until a constructor supplies it. A typed primitive refinement records exact equality, not equality up to phase.

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. A typed primitive refinement records exact equality, not equality up to phase.

Declaration kind. structure.

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

Lean code for Definition6.8.54●1 definition

structure(3 fields)defined in QuantumBlockEncoding/PrimitiveSemantics.lean

complete

structure QuantumBlockEncoding.PrimitiveRefinement (qubits : ℕ) : Type

structure QuantumBlockEncoding.PrimitiveRefinement
  (qubits : ℕ) : Type

A typed primitive refinement records exact equality, not equality up to phase.

Fields

circuit : QuantumBlockEncoding.PrimitiveCircuit qubits

target : Matrix (QuantumBlockEncoding.PrimitiveBasis qubits) (QuantumBlockEncoding.PrimitiveBasis qubits) ℂ

exact : QuantumBlockEncoding.evalPrimitiveCircuit self.circuit = self.target