5.4. QuantumBlockEncoding/Resources.lean🔗

25 explicit public declarations, in source order.

Definition5.4.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “resource”. A proposition-valued field is a requirement until a constructor supplies it. Exact resource counts for candidate block-encoding circuits.

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

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

Technical source note. Exact resource counts for candidate block-encoding circuits. 'depth' is the sequential circuit depth under the current schedule. A later hardware backend can refine the gate set, but ABEIS always records this field because parallelizing two independent gates is a real improvement even when the total gate count is unchanged.

Declaration kind. structure.

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

Lean code for Definition5.4.1●1 definition

structure(5 fields)defined in QuantumBlockEncoding/Resources.lean

complete

structure QuantumBlockEncoding.Resource : Type

structure QuantumBlockEncoding.Resource : Type

Exact resource counts for candidate block-encoding circuits.

`depth` is the sequential circuit depth under the current schedule.  A later
hardware backend can refine the gate set, but ABEIS always records this field
because parallelizing two independent gates is a real improvement even when
the total gate count is unchanged.

Fields

oneQubit : ℕ

cnot : ℕ

oracleCalls : ℕ

pureAncilla : ℕ

depth : ℕ

Definition5.4.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “gates”. Gate count used by the search score before an oracle call is expanded.

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. Gate count used by the search score before an oracle call is expanded.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.gates
  (r : QuantumBlockEncoding.Resource) : ℕ

def QuantumBlockEncoding.Resource.gates
  (r : QuantumBlockEncoding.Resource) : ℕ

Gate count used by the search score before an oracle call is expanded.

Definition5.4.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition5.4.3●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.add
  (r s : QuantumBlockEncoding.Resource) : QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Resource.add
  (r s : QuantumBlockEncoding.Resource) :
  QuantumBlockEncoding.Resource

Definition5.4.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “parallel”. Resource combination for one parallel layer.

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. Resource combination for one parallel layer. Gate counts add, while depth is the maximum of the parallel subcircuits.

Declaration kind. def.

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

Lean code for Definition5.4.4●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.parallel
  (r s : QuantumBlockEncoding.Resource) : QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Resource.parallel
  (r s : QuantumBlockEncoding.Resource) :
  QuantumBlockEncoding.Resource

Resource combination for one parallel layer.  Gate counts add, while depth is
the maximum of the parallel subcircuits.

Definition5.4.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition5.4.5●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.scale (k : ℕ)
  (r : QuantumBlockEncoding.Resource) : QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Resource.scale
  (k : ℕ)
  (r : QuantumBlockEncoding.Resource) :
  QuantumBlockEncoding.Resource

Definition5.4.6

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition5.4.6●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.ofCounts (oneQubit cnot pureAncilla : ℕ) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Resource.ofCounts
  (oneQubit cnot pureAncilla : ℕ) :
  QuantumBlockEncoding.Resource

Definition5.4.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “of counts with 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/Resources.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.4.7●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.Resource.ofCountsWithDepth
  (oneQubit cnot oracleCalls pureAncilla depth : ℕ) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Resource.ofCountsWithDepth
  (oneQubit cnot oracleCalls pureAncilla
    depth : ℕ) :
  QuantumBlockEncoding.Resource

Theorem5.4.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.8●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.gates_eq
  (r : QuantumBlockEncoding.Resource) :
  r.gates = r.oneQubit + r.cnot + r.oracleCalls

theorem QuantumBlockEncoding.Resource.gates_eq
  (r : QuantumBlockEncoding.Resource) :
  r.gates =
    r.oneQubit + r.cnot + r.oracleCalls

Theorem5.4.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.9●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.zero_oneQubit :
  QuantumBlockEncoding.Resource.oneQubit 0 = 0

theorem QuantumBlockEncoding.Resource.zero_oneQubit :
  QuantumBlockEncoding.Resource.oneQubit
      0 =
    0

Theorem5.4.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.10●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.zero_cnot :
  QuantumBlockEncoding.Resource.cnot 0 = 0

theorem QuantumBlockEncoding.Resource.zero_cnot :
  QuantumBlockEncoding.Resource.cnot 0 = 0

Theorem5.4.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “zero oracle calls”; 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/Resources.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.4.11●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.zero_oracleCalls :
  QuantumBlockEncoding.Resource.oracleCalls 0 = 0

theorem QuantumBlockEncoding.Resource.zero_oracleCalls :
  QuantumBlockEncoding.Resource.oracleCalls
      0 =
    0

Theorem5.4.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.12●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.zero_pureAncilla :
  QuantumBlockEncoding.Resource.pureAncilla 0 = 0

theorem QuantumBlockEncoding.Resource.zero_pureAncilla :
  QuantumBlockEncoding.Resource.pureAncilla
      0 =
    0

Theorem5.4.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “zero depth”; 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/Resources.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.4.13●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.zero_depth :
  QuantumBlockEncoding.Resource.depth 0 = 0

theorem QuantumBlockEncoding.Resource.zero_depth :
  QuantumBlockEncoding.Resource.depth 0 =
    0

Theorem5.4.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.14●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.add_oneQubit
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).oneQubit = r.oneQubit + s.oneQubit

theorem QuantumBlockEncoding.Resource.add_oneQubit
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).oneQubit =
    r.oneQubit + s.oneQubit

Theorem5.4.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.15●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.add_cnot
  (r s : QuantumBlockEncoding.Resource) : (r + s).cnot = r.cnot + s.cnot

theorem QuantumBlockEncoding.Resource.add_cnot
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).cnot = r.cnot + s.cnot

Theorem5.4.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.16●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.add_oracleCalls
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).oracleCalls = r.oracleCalls + s.oracleCalls

theorem QuantumBlockEncoding.Resource.add_oracleCalls
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).oracleCalls =
    r.oracleCalls + s.oracleCalls

Theorem5.4.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.17●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.add_pureAncilla
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).pureAncilla = r.pureAncilla + s.pureAncilla

theorem QuantumBlockEncoding.Resource.add_pureAncilla
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).pureAncilla =
    r.pureAncilla + s.pureAncilla

Theorem5.4.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem5.4.18●1 theorem

theoremdefined in QuantumBlockEncoding/Resources.lean

complete

theorem QuantumBlockEncoding.Resource.add_depth
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).depth = r.depth + s.depth

theorem QuantumBlockEncoding.Resource.add_depth
  (r s : QuantumBlockEncoding.Resource) :
  (r + s).depth = r.depth + s.depth

Definition5.4.19

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “cost expr”; its constructors are the cases that downstream code must handle. A small expression language for big-O resource formulas.

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 small expression language for big-O resource formulas.

Declaration kind. inductive.

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

Lean code for Definition5.4.19●1 definition

inductive(6 constructors)defined in QuantumBlockEncoding/Resources.lean

complete

inductive QuantumBlockEncoding.CostExpr : Type

inductive QuantumBlockEncoding.CostExpr : Type

A small expression language for big-O resource formulas.

Constructors

nat (n : ℕ) : QuantumBlockEncoding.CostExpr

atom (name : String) : QuantumBlockEncoding.CostExpr

add (a b : QuantumBlockEncoding.CostExpr) :
  QuantumBlockEncoding.CostExpr

mul (a b : QuantumBlockEncoding.CostExpr) :
  QuantumBlockEncoding.CostExpr

log (a : QuantumBlockEncoding.CostExpr) :
  QuantumBlockEncoding.CostExpr

sum (index : String)
  (body : QuantumBlockEncoding.CostExpr) :
  QuantumBlockEncoding.CostExpr

Definition5.4.20

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition5.4.20●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.CostExpr.atoms (names : List String) :
  List QuantumBlockEncoding.CostExpr

def QuantumBlockEncoding.CostExpr.atoms
  (names : List String) :
  List QuantumBlockEncoding.CostExpr

Definition5.4.21

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “asymptotic resource”. A proposition-valued field is a requirement until a constructor supplies it. Big-O style resource claim.

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

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

Technical source note. Big-O style resource claim.

Declaration kind. structure.

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

Lean code for Definition5.4.21●1 definition

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

complete

structure QuantumBlockEncoding.AsymptoticResource : Type

structure QuantumBlockEncoding.AsymptoticResource :
  Type

Big-O style resource claim.

Fields

gates : QuantumBlockEncoding.CostExpr

pureAncilla : QuantumBlockEncoding.CostExpr

Definition5.4.22

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition5.4.22●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.AsymptoticResource.add
  (r s : QuantumBlockEncoding.AsymptoticResource) :
  QuantumBlockEncoding.AsymptoticResource

def QuantumBlockEncoding.AsymptoticResource.add
  (r s :
    QuantumBlockEncoding.AsymptoticResource) :
  QuantumBlockEncoding.AsymptoticResource

Definition5.4.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “banded sparse access resource”. Lemma 1 resource count from Guseynov-Huang-Liu 2025.

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. Lemma 1 resource count from Guseynov-Huang-Liu 2025.

Declaration kind. def.

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

Lean code for Definition5.4.23●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.bandedSparseAccessResource (n l : ℕ) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.bandedSparseAccessResource
  (n l : ℕ) :
  QuantumBlockEncoding.Resource

Lemma 1 resource count from Guseynov-Huang-Liu 2025.

Definition5.4.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sparse amplitude oracle resource”. Lemma 3 resource count for the sparse-amplitude oracle.

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. Lemma 3 resource count for the sparse-amplitude oracle.

Declaration kind. def.

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

Lean code for Definition5.4.24●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.sparseAmplitudeOracleResource (l : ℕ) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.sparseAmplitudeOracleResource
  (l : ℕ) : QuantumBlockEncoding.Resource

Lemma 3 resource count for the sparse-amplitude oracle.

Definition5.4.25

uses 0used by 0✓L∃∀N

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

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. Appendix comparator/indicator resource count.

Declaration kind. def.

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

Lean code for Definition5.4.25●1 definition

defdefined in QuantumBlockEncoding/Resources.lean

complete

def QuantumBlockEncoding.indicatorResource (n : ℕ) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.indicatorResource
  (n : ℕ) : QuantumBlockEncoding.Resource

Appendix comparator/indicator resource count.