5.2. QuantumBlockEncoding/Circuit.lean🔗

12 explicit public declarations, in source order.

Definition5.2.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.1●1 definition

inductive(7 constructors)defined in QuantumBlockEncoding/Circuit.lean

complete

inductive QuantumBlockEncoding.Gate : Type

inductive QuantumBlockEncoding.Gate : Type

Constructors

oneQubit (name : String) (target : ℕ) :
  QuantumBlockEncoding.Gate

rotationY (target : ℕ) (angleLabel : String) :
  QuantumBlockEncoding.Gate

rotationZ (target : ℕ) (angleLabel : String) :
  QuantumBlockEncoding.Gate

cnot (control target : ℕ) : QuantumBlockEncoding.Gate

swap (left right : ℕ) : QuantumBlockEncoding.Gate

multiControlled (controls : List (ℕ × Bool))
  (body : QuantumBlockEncoding.Gate) :
  QuantumBlockEncoding.Gate

oracleCall (name : String) : QuantumBlockEncoding.Gate

Definition5.2.2

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.2●1 definition

abbrevdefined in QuantumBlockEncoding/Circuit.lean

complete

abbrev QuantumBlockEncoding.Circuit : Type

abbrev QuantumBlockEncoding.Circuit : Type

Definition5.2.3

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Conservative elementary-resource estimate for the current IR. Oracle calls have zero local cost here because their implementation should be expanded or certified separately.

Declaration kind. def.

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

Lean code for Definition5.2.3●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.Gate.resource :
  QuantumBlockEncoding.Gate → QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Gate.resource :
  QuantumBlockEncoding.Gate →
    QuantumBlockEncoding.Resource

Conservative elementary-resource estimate for the current IR.
Oracle calls have zero local cost here because their implementation should be
expanded or certified separately.

Definition5.2.4

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “circuit layer”. A layer is a list of gates intended to be scheduled in parallel.

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A layer is a list of gates intended to be scheduled in parallel. The current IR does not yet prove non-overlap of qubits inside a layer; that belongs to the semantic proof obligations for a concrete backend.

Declaration kind. abbrev.

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

Lean code for Definition5.2.4●1 definition

abbrevdefined in QuantumBlockEncoding/Circuit.lean

complete

abbrev QuantumBlockEncoding.CircuitLayer : Type

abbrev QuantumBlockEncoding.CircuitLayer : Type

A layer is a list of gates intended to be scheduled in parallel.  The current
IR does not yet prove non-overlap of qubits inside a layer; that belongs to
the semantic proof obligations for a concrete backend.

Definition5.2.5

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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.5●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.CircuitLayer.resource
  (layer : QuantumBlockEncoding.CircuitLayer) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.CircuitLayer.resource
  (layer :
    QuantumBlockEncoding.CircuitLayer) :
  QuantumBlockEncoding.Resource

Definition5.2.6

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “layered circuit”. A layered circuit is the schedule used for depth comparisons.

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A layered circuit is the schedule used for depth comparisons.

Declaration kind. abbrev.

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

Lean code for Definition5.2.6●1 definition

abbrevdefined in QuantumBlockEncoding/Circuit.lean

complete

abbrev QuantumBlockEncoding.LayeredCircuit : Type

abbrev QuantumBlockEncoding.LayeredCircuit : Type

A layered circuit is the schedule used for depth comparisons.

Definition5.2.7

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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.7●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.LayeredCircuit.resource :
  QuantumBlockEncoding.LayeredCircuit → QuantumBlockEncoding.Resource

def QuantumBlockEncoding.LayeredCircuit.resource :
  QuantumBlockEncoding.LayeredCircuit →
    QuantumBlockEncoding.Resource

Definition5.2.8

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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.8●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.LayeredCircuit.depth
  (circuit : QuantumBlockEncoding.LayeredCircuit) : ℕ

def QuantumBlockEncoding.LayeredCircuit.depth
  (circuit :
    QuantumBlockEncoding.LayeredCircuit) :
  ℕ

Definition5.2.9

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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.9●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.Circuit.resource :
  QuantumBlockEncoding.Circuit → QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Circuit.resource :
  QuantumBlockEncoding.Circuit →
    QuantumBlockEncoding.Resource

Theorem5.2.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “resource nil”; 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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Theorem5.2.10●1 theorem

theoremdefined in QuantumBlockEncoding/Circuit.lean

complete

theorem QuantumBlockEncoding.Circuit.resource_nil :
  QuantumBlockEncoding.Circuit.resource [] = 0

theorem QuantumBlockEncoding.Circuit.resource_nil :
  QuantumBlockEncoding.Circuit.resource
      [] =
    0

Theorem5.2.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “resource cons”; 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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Theorem5.2.11●1 theorem

theoremdefined in QuantumBlockEncoding/Circuit.lean

complete

theorem QuantumBlockEncoding.Circuit.resource_cons
  (gate : QuantumBlockEncoding.Gate)
  (rest : QuantumBlockEncoding.Circuit) :
  QuantumBlockEncoding.Circuit.resource (gate :: rest) =
    gate.resource + rest.resource

theorem QuantumBlockEncoding.Circuit.resource_cons
  (gate : QuantumBlockEncoding.Gate)
  (rest : QuantumBlockEncoding.Circuit) :
  QuantumBlockEncoding.Circuit.resource
      (gate :: rest) =
    gate.resource + rest.resource

Definition5.2.12

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.

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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

Lean code for Definition5.2.12●1 definition

defdefined in QuantumBlockEncoding/Circuit.lean

complete

def QuantumBlockEncoding.Circuit.depth
  (circuit : QuantumBlockEncoding.Circuit) : ℕ

def QuantumBlockEncoding.Circuit.depth
  (circuit :
    QuantumBlockEncoding.Circuit) :
  ℕ