6.14. QuantumBlockEncoding/PrimitiveCircuit.lean🔗

39 explicit public declarations, in source order.

Definition6.14.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “exact angle”; its constructors are the cases that downstream code must handle.

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. inductive.

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

Lean code for Definition6.14.1●1 definition

inductive(8 constructors)defined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

inductive QuantumBlockEncoding.ExactAngle : Type

inductive QuantumBlockEncoding.ExactAngle : Type

Constructors

rational (value : ℚ) : QuantumBlockEncoding.ExactAngle

piRational (value : ℚ) : QuantumBlockEncoding.ExactAngle

twiceArccosRational (value : ℚ) (bounded : |↑value| ≤ 1) :
  QuantumBlockEncoding.ExactAngle

twiceArccosSqrtRational (value : ℚ)
  (bounded : 0 ≤ ↑value ∧ ↑value ≤ 1) :
  QuantumBlockEncoding.ExactAngle

real (value : ℝ) : QuantumBlockEncoding.ExactAngle

An exact real angle in the mathematical circuit. This constructor does
not promise a computable decimal export; exporters must supply and audit
their own numerical evaluation of the defining real expression.

add (left right : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

neg (value : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

scale (factor : ℚ)
  (value : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

Definition6.14.2

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.2●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.ExactAngle.eval :
  QuantumBlockEncoding.ExactAngle → ℝ

def QuantumBlockEncoding.ExactAngle.eval :
  QuantumBlockEncoding.ExactAngle → ℝ

Theorem6.14.3

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_add
  (left right : QuantumBlockEncoding.ExactAngle) :
  (left.add right).eval = left.eval + right.eval

theorem QuantumBlockEncoding.ExactAngle.eval_add
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  (left.add right).eval =
    left.eval + right.eval

Theorem6.14.4

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.14.4●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_neg
  (value : QuantumBlockEncoding.ExactAngle) :
  value.neg.eval = -value.eval

theorem QuantumBlockEncoding.ExactAngle.eval_neg
  (value :
    QuantumBlockEncoding.ExactAngle) :
  value.neg.eval = -value.eval

Theorem6.14.5

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.5●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_scale (factor : ℚ)
  (value : QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.ExactAngle.scale factor value).eval =
    ↑factor * value.eval

theorem QuantumBlockEncoding.ExactAngle.eval_scale
  (factor : ℚ)
  (value :
    QuantumBlockEncoding.ExactAngle) :
  (QuantumBlockEncoding.ExactAngle.scale
        factor value).eval =
    ↑factor * value.eval

Definition6.14.6

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.6●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.ExactAngle.sub
  (left right : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.ExactAngle.sub
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

Definition6.14.7

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.7●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.ExactAngle.halfAdd
  (left right : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.ExactAngle.halfAdd
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

Definition6.14.8

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.8●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.ExactAngle.halfSub
  (left right : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.ExactAngle.halfSub
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.ExactAngle

Theorem6.14.9

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.9●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_sub
  (left right : QuantumBlockEncoding.ExactAngle) :
  (left.sub right).eval = left.eval - right.eval

theorem QuantumBlockEncoding.ExactAngle.eval_sub
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  (left.sub right).eval =
    left.eval - right.eval

Theorem6.14.10

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.10●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_half_add
  (left right : QuantumBlockEncoding.ExactAngle) :
  (left.halfAdd right).eval = (left.eval + right.eval) / 2

theorem QuantumBlockEncoding.ExactAngle.eval_half_add
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  (left.halfAdd right).eval =
    (left.eval + right.eval) / 2

Theorem6.14.11

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.11●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.ExactAngle.eval_half_sub
  (left right : QuantumBlockEncoding.ExactAngle) :
  (left.halfSub right).eval = (left.eval - right.eval) / 2

theorem QuantumBlockEncoding.ExactAngle.eval_half_sub
  (left right :
    QuantumBlockEncoding.ExactAngle) :
  (left.halfSub right).eval =
    (left.eval - right.eval) / 2

Definition6.14.12

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “primitive gate”; its constructors are the cases that downstream code must handle.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. inductive.

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

Lean code for Definition6.14.12●1 definition

inductive(4 constructors, 1 parameter)defined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

inductive QuantumBlockEncoding.PrimitiveGate (qubits : ℕ) : Type

inductive QuantumBlockEncoding.PrimitiveGate
  (qubits : ℕ) : Type

Constructors

x {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveGate qubits

ry {qubits : ℕ} (target : Fin qubits)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveGate qubits

rz {qubits : ℕ} (target : Fin qubits)
  (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveGate qubits

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

Definition6.14.13

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. abbrev.

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

Lean code for Definition6.14.13●1 definition

abbrevdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

abbrev QuantumBlockEncoding.PrimitiveCircuit (qubits : ℕ) : Type

abbrev QuantumBlockEncoding.PrimitiveCircuit
  (qubits : ℕ) : Type

Definition6.14.14

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “primitive program”. A proposition-valued field is a requirement until a constructor supplies it. A primitive circuit together with an exact global phase.

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

Technical source note. A primitive circuit together with an exact global phase.

Declaration kind. structure.

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

Lean code for Definition6.14.14●1 definition

structure(2 fields)defined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

structure QuantumBlockEncoding.PrimitiveProgram (qubits : ℕ) : Type

structure QuantumBlockEncoding.PrimitiveProgram
  (qubits : ℕ) : Type

A primitive circuit together with an exact global phase.

Fields

circuit : QuantumBlockEncoding.PrimitiveCircuit qubits

globalPhase : QuantumBlockEncoding.ExactAngle

Definition6.14.15

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.15●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveGate.dagger {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate qubits →
    QuantumBlockEncoding.PrimitiveGate qubits

def QuantumBlockEncoding.PrimitiveGate.dagger
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    QuantumBlockEncoding.PrimitiveGate
      qubits

Definition6.14.16

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveGate.touched {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate qubits → Finset (Fin qubits)

def QuantumBlockEncoding.PrimitiveGate.touched
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    Finset (Fin qubits)

Definition6.14.17

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.17●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveGate.oneQubitCount {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate qubits → ℕ

def QuantumBlockEncoding.PrimitiveGate.oneQubitCount
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    ℕ

Definition6.14.18

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.18●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveGate.twoQubitCount {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate qubits → ℕ

def QuantumBlockEncoding.PrimitiveGate.twoQubitCount
  {qubits : ℕ} :
  QuantumBlockEncoding.PrimitiveGate
      qubits →
    ℕ

Definition6.14.19

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.19●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.gateCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.gateCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Definition6.14.20

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.20●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.oneQubitCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.oneQubitCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Definition6.14.21

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.21●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.twoQubitCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.twoQubitCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Definition6.14.22

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.22●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.ryCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.ryCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Definition6.14.23

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.23●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.cxCount {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.cxCount
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Theorem6.14.24

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.24●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_append {qubits : ℕ}
  (left right : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  (left ++ right).ryCount = left.ryCount + right.ryCount

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_append
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  (left ++ right).ryCount =
    left.ryCount + right.ryCount

Theorem6.14.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cx count append”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.25●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_append {qubits : ℕ}
  (left right : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  (left ++ right).cxCount = left.cxCount + right.cxCount

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_append
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  (left ++ right).cxCount =
    left.cxCount + right.cxCount

Theorem6.14.26

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.14.26●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_singleton_ry {qubits : ℕ}
  (target : Fin qubits) (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      [QuantumBlockEncoding.PrimitiveGate.ry target angle] =
    1

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_singleton_ry
  {qubits : ℕ} (target : Fin qubits)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      [QuantumBlockEncoding.PrimitiveGate.ry
          target angle] =
    1

Theorem6.14.27

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.27●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_singleton_cx {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      [QuantumBlockEncoding.PrimitiveGate.cx control target distinct] =
    0

theorem QuantumBlockEncoding.PrimitiveCircuit.ryCount_singleton_cx
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveCircuit.ryCount
      [QuantumBlockEncoding.PrimitiveGate.cx
          control target distinct] =
    0

Theorem6.14.28

uses 0used by 0✓L∃∀N

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

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

Lean code for Theorem6.14.28●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_singleton_ry {qubits : ℕ}
  (target : Fin qubits) (angle : QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      [QuantumBlockEncoding.PrimitiveGate.ry target angle] =
    0

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_singleton_ry
  {qubits : ℕ} (target : Fin qubits)
  (angle :
    QuantumBlockEncoding.ExactAngle) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      [QuantumBlockEncoding.PrimitiveGate.ry
          target angle] =
    0

Theorem6.14.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cx count singleton cx”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.29●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_singleton_cx {qubits : ℕ}
  (control target : Fin qubits) (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      [QuantumBlockEncoding.PrimitiveGate.cx control target distinct] =
    1

theorem QuantumBlockEncoding.PrimitiveCircuit.cxCount_singleton_cx
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target) :
  QuantumBlockEncoding.PrimitiveCircuit.cxCount
      [QuantumBlockEncoding.PrimitiveGate.cx
          control target distinct] =
    1

Definition6.14.30

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.30●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth {qubits : ℕ}
  (depth : Fin qubits → ℕ)
  (gate : QuantumBlockEncoding.PrimitiveGate qubits) : Fin qubits → ℕ

def QuantumBlockEncoding.PrimitiveCircuit.nextWireDepth
  {qubits : ℕ} (depth : Fin qubits → ℕ)
  (gate :
    QuantumBlockEncoding.PrimitiveGate
      qubits) :
  Fin qubits → ℕ

Definition6.14.31

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.31●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.wireDepths {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  Fin qubits → ℕ

def QuantumBlockEncoding.PrimitiveCircuit.wireDepths
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  Fin qubits → ℕ

Definition6.14.32

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.32●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.depth {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) : ℕ

def QuantumBlockEncoding.PrimitiveCircuit.depth
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  ℕ

Definition6.14.33

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.33●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveCircuit.resource {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.PrimitiveCircuit.resource
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.Resource

Theorem6.14.34

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

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

Lean code for Theorem6.14.34●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.gateCount_eq_length {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  circuit.gateCount = List.length circuit

theorem QuantumBlockEncoding.PrimitiveCircuit.gateCount_eq_length
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  circuit.gateCount = List.length circuit

Theorem6.14.35

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “resource oracle calls eq 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.

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

Lean code for Theorem6.14.35●1 theorem

theoremdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

theorem QuantumBlockEncoding.PrimitiveCircuit.resource_oracleCalls_eq_zero
  {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  circuit.resource.oracleCalls = 0

theorem QuantumBlockEncoding.PrimitiveCircuit.resource_oracleCalls_eq_zero
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  circuit.resource.oracleCalls = 0

Definition6.14.36

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.36●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveProgram.identity (qubits : ℕ) :
  QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.PrimitiveProgram.identity
  (qubits : ℕ) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Definition6.14.37

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “seq”. Execute 'left', then 'right', using chronological list semantics.

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

Technical source note. Execute 'left', then 'right', using chronological list semantics.

Declaration kind. def.

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

Lean code for Definition6.14.37●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

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

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

Execute `left`, then `right`, using chronological list semantics.

Definition6.14.38

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.38●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveProgram.dagger {qubits : ℕ}
  (program : QuantumBlockEncoding.PrimitiveProgram qubits) :
  QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.PrimitiveProgram.dagger
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Definition6.14.39

uses 0used by 0✓L∃∀N

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

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

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

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

Lean code for Definition6.14.39●1 definition

defdefined in QuantumBlockEncoding/PrimitiveCircuit.lean

complete

def QuantumBlockEncoding.PrimitiveProgram.resource {qubits : ℕ}
  (program : QuantumBlockEncoding.PrimitiveProgram qubits) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.PrimitiveProgram.resource
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.PrimitiveProgram
      qubits) :
  QuantumBlockEncoding.Resource