QuantumBlockEncoding/Resources.lean

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.

structure Resource where
  oneQubit : Nat := 0
  cnot : Nat := 0
  oracleCalls : Nat := 0
  pureAncilla : Nat := 0
  depth : Nat := 0
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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.

def gates (r : Resource) : Nat := r.oneQubit + r.cnot + r.oracleCalls

commit-pinned source · Verso Blueprint panel

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

def add (r s : Resource) : Resource where
  oneQubit := r.oneQubit + s.oneQubit
  cnot := r.cnot + s.cnot
  oracleCalls := r.oracleCalls + s.oracleCalls
  pureAncilla := r.pureAncilla + s.pureAncilla
  depth := r.depth + s.depth

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

commit-pinned source · Verso Blueprint panel

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

def parallel (r s : Resource) : Resource where
  oneQubit := r.oneQubit + s.oneQubit
  cnot := r.cnot + s.cnot
  oracleCalls := r.oracleCalls + s.oracleCalls
  pureAncilla := Nat.max r.pureAncilla s.pureAncilla
  depth := Nat.max r.depth s.depth

instance : Zero Resource := ⟨{}⟩
instance : HAdd Resource Resource Resource := ⟨add⟩

commit-pinned source · Verso Blueprint panel

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

def scale (k : Nat) (r : Resource) : Resource where
  oneQubit := k * r.oneQubit
  cnot := k * r.cnot
  oracleCalls := k * r.oracleCalls
  pureAncilla := k * r.pureAncilla
  depth := k * r.depth

commit-pinned source · Verso Blueprint panel

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

def ofCounts (oneQubit cnot pureAncilla : Nat) : Resource where
  oneQubit := oneQubit
  cnot := cnot
  pureAncilla := pureAncilla
  depth := oneQubit + cnot

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “of counts with depth”.

def ofCountsWithDepth (oneQubit cnot oracleCalls pureAncilla depth : Nat) : Resource where
  oneQubit := oneQubit
  cnot := cnot
  oracleCalls := oracleCalls
  pureAncilla := pureAncilla
  depth := depth

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “gates eq”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem gates_eq (r : Resource) :
    r.gates = r.oneQubit + r.cnot + r.oracleCalls := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero one qubit”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem zero_oneQubit : (0 : Resource).oneQubit = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero cnot”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem zero_cnot : (0 : Resource).cnot = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem zero_oracleCalls : (0 : Resource).oracleCalls = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero pure ancilla”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem zero_pureAncilla : (0 : Resource).pureAncilla = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “zero depth”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem zero_depth : (0 : Resource).depth = 0 := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “add one qubit”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem add_oneQubit (r s : Resource) :
    (r + s).oneQubit = r.oneQubit + s.oneQubit := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “add cnot”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem add_cnot (r s : Resource) :
    (r + s).cnot = r.cnot + s.cnot := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “add oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem add_oracleCalls (r s : Resource) :
    (r + s).oracleCalls = r.oracleCalls + s.oracleCalls := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “add pure ancilla”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem add_pureAncilla (r s : Resource) :
    (r + s).pureAncilla = r.pureAncilla + s.pureAncilla := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “add depth”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem add_depth (r s : Resource) :
    (r + s).depth = r.depth + s.depth := rfl

commit-pinned source · Verso Blueprint panel

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.

inductive CostExpr where
  | nat (n : Nat)
  | atom (name : String)
  | add (a b : CostExpr)
  | mul (a b : CostExpr)
  | log (a : CostExpr)
  | sum (index : String) (body : CostExpr)
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def atoms (names : List String) : List CostExpr :=
  names.map CostExpr.atom

commit-pinned source · Verso Blueprint panel

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.

structure AsymptoticResource where
  gates : CostExpr
  pureAncilla : CostExpr
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

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

def add (r s : AsymptoticResource) : AsymptoticResource where
  gates := r.gates + s.gates
  pureAncilla := r.pureAncilla + s.pureAncilla

instance : HAdd AsymptoticResource AsymptoticResource AsymptoticResource := ⟨add⟩

commit-pinned source · Verso Blueprint panel

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

def bandedSparseAccessResource (n l : Nat) : Resource :=
  Resource.ofCounts
    ((2 ^ l + 1) * (32 * n - 48))
    (25 * 2 ^ l * n - 36 * 2 ^ l + 32 * n - 48)
    (n - 1)

/-- Lemma 3 resource count for the sparse-amplitude oracle. -/

commit-pinned source · Verso Blueprint panel

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

def sparseAmplitudeOracleResource (l : Nat) : Resource :=
  Resource.ofCounts (2 ^ l) (2 ^ l) 0

/-- Appendix comparator/indicator resource count. -/

commit-pinned source · Verso Blueprint panel

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

def indicatorResource (n : Nat) : Resource :=
  Resource.ofCounts (16 * n + 34) (12 * n - 4) (n - 1)

commit-pinned source · Verso Blueprint panel