QuantumBlockEncoding/BlockEncoding.lean

This record groups the data and proof fields needed for “register layout”. A proposition-valued field is a requirement until a constructor supplies it.

structure RegisterLayout where
  systemQubits : Nat
  signalQubits : Nat
  pureAncillas : Nat
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “auxiliary qubits”. The auxiliary qubit count used by the block-encoding score.

def auxiliaryQubits (layout : RegisterLayout) : Nat :=
  layout.signalQubits + layout.pureAncillas

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “block encoding spec”. A proposition-valued field is a requirement until a constructor supplies it. A block-encoding candidate before semantic proofs are attached.

structure BlockEncodingSpec (α : Type u) (rows cols : Nat) where
  matrix : Matrix rows cols α
  normalizer : α
  error : α
  layout : RegisterLayout
  circuit : Circuit
  resource : Resource

/--
Resource score for comparing two candidate block encodings of the same
operator.  The search order is deliberately domain-specific:

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “block encoding cost”. A proposition-valued field is a requirement until a constructor supplies it. Resource score for comparing two candidate block encodings of the same operator.

structure BlockEncodingCost where
  auxiliaryQubits : Nat
  gateCount : Nat
  depth : Nat
  oracleCalls : Nat
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “from layout and resource”.

def fromLayoutAndResource (layout : RegisterLayout) (resource : Resource) :
    BlockEncodingCost where
  auxiliaryQubits := layout.auxiliaryQubits
  gateCount := resource.gates
  depth := resource.depth
  oracleCalls := resource.oracleCalls

commit-pinned source · Verso Blueprint panel

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

def fromSpec (spec : BlockEncodingSpec α rows cols) : BlockEncodingCost :=
  fromLayoutAndResource spec.layout spec.resource

/-- Strict lexicographic improvement used by candidate-population selection. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “better than”. Strict lexicographic improvement used by candidate-population selection.

def betterThan (x y : BlockEncodingCost) : Prop :=
  x.gateCount < y.gateCount ∨
  (x.gateCount = y.gateCount ∧
    (x.depth < y.depth ∨
      (x.depth = y.depth ∧
        (x.auxiliaryQubits < y.auxiliaryQubits ∨
          (x.auxiliaryQubits = y.auxiliaryQubits ∧
            x.oracleCalls < y.oracleCalls)))))

/-- Non-strict version for accepting a candidate as no worse than a baseline. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “no worse than”. Non-strict version for accepting a candidate as no worse than a baseline.

def noWorseThan (x y : BlockEncodingCost) : Prop :=
  x = y ∨ x.betterThan y

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “query operator target”. A proposition-valued field is a requirement until a constructor supplies it. The concrete input ABEIS is meant to solve: a user gives an operator/query oracle target, usually as a finite matrix together with a normalization contract and optional free parameters.

structure QueryOperatorTarget (α : Type u) (rows cols : Nat) where
  operator : Matrix rows cols α
  normalizer : α
  source : String
  semanticContract : String
  freeParameters : List String := []

/--
A candidate unitary for an `n`-qubit square operator.  The size of the unitary
is fixed by the chosen number of auxiliary qubits: if the target acts on
`N = 2^n` dimensions and the candidate uses `a` auxiliary qubits, then the

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. A candidate unitary for an 'n'-qubit square operator.

structure OperatorBlockEncodingCandidate (α : Type u) (systemQubits : Nat) where
  auxiliaryQubits : Nat
  target : QueryOperatorTarget α (gridSize systemQubits) (gridSize systemQubits)
  unitary :
    Matrix (gridSize (systemQubits + auxiliaryQubits))
      (gridSize (systemQubits + auxiliaryQubits)) α
  layout : RegisterLayout
  circuit : Circuit
  schedule : LayeredCircuit := []
  resource : Resource
  layoutMatches : layout.auxiliaryQubits = auxiliaryQubits

commit-pinned source · Verso Blueprint panel

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

def cost (candidate : OperatorBlockEncodingCandidate α systemQubits) :
    BlockEncodingCost :=
  {
    auxiliaryQubits := candidate.auxiliaryQubits
    gateCount := candidate.resource.gates
    depth := candidate.resource.depth
    oracleCalls := candidate.resource.oracleCalls
  }

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “verified operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified candidate with explicit proofs of unitarity and block containment.

structure VerifiedOperatorBlockEncoding (α : Type u) (systemQubits : Nat) where
  candidate : OperatorBlockEncodingCandidate α systemQubits
  unitaryProof : candidate.isUnitary
  blockProof : candidate.blockContainsTarget

/--
An approximate block-encoding candidate for the same operator-first interface.

The mathematical backend should instantiate `approximationBound` with the
norm inequality

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “approximate operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. An approximate block-encoding candidate for the same operator-first interface.

structure ApproximateOperatorBlockEncodingCandidate
    (α : Type u) (systemQubits : Nat) where
  candidate : OperatorBlockEncodingCandidate α systemQubits
  epsilon : α
  approximationBound : Prop

/--
A verified approximate block encoding.  Exact block encodings are the special
case `epsilon = 0` when the backend proves that exact equality implies the
chosen norm bound.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “verified approximate operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified approximate block encoding.

structure VerifiedApproximateOperatorBlockEncoding
    (α : Type u) (systemQubits : Nat) where
  approxCandidate : ApproximateOperatorBlockEncodingCandidate α systemQubits
  unitaryProof : approxCandidate.candidate.isUnitary
  approximationProof : approxCandidate.approximationBound

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “as zero error approx”. Package an exact certificate as a zero-error approximate certificate when the chosen approximate proposition is the same exact block predicate.

def asZeroErrorApprox [OfNat α 0]
    (v : VerifiedOperatorBlockEncoding α systemQubits) :
    VerifiedApproximateOperatorBlockEncoding α systemQubits where
  approxCandidate := {
    candidate := v.candidate
    epsilon := 0
    approximationBound := v.candidate.blockContainsTarget
  }
  unitaryProof := v.unitaryProof
  approximationProof := v.blockProof

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “adaptive block encoding policy”. A proposition-valued field is a requirement until a constructor supplies it. User-level stopping and relaxation policy for operator block-encoding search.

structure AdaptiveBlockEncodingPolicy (α : Type u) where
  maxExactIterations : Nat
  exactStallIterations : Nat
  requiredCost : BlockEncodingCost
  requestedEpsilon : α
  allowRelaxedEpsilon : Bool
  maxUpperAgents : Nat
  maxMiddleAgents : Nat
  maxLowerAgents : Nat
deriving Repr

commit-pinned source · Verso Blueprint panel

This type lists the allowed alternatives for “block encoding search phase”; its constructors are the cases that downstream code must handle. High-level phase labels used by the candidate-population ledger.

inductive BlockEncodingSearchPhase where
  | exactSearch
  | exactConvergedApproxSearch
  | relaxedApproxSearch
  | stopped
deriving Repr, DecidableEq

/--
A verified block encoding.  The three proposition fields are intentionally
parameters of the certificate so that early project files can state workflows
without committing to a specific matrix norm or unitary semantics.  A mathlib

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “verified block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified block encoding.

structure VerifiedBlockEncoding (α : Type u) (rows cols : Nat) where
  spec : BlockEncodingSpec α rows cols
  isUnitary : Prop
  blockCorrect : Prop
  resourceBound : Prop
  unitaryProof : isUnitary
  blockProof : blockCorrect
  resourceProof : resourceBound

commit-pinned source · Verso Blueprint panel

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

theorem unitary {α : Type u} {rows cols : Nat}
    (v : VerifiedBlockEncoding α rows cols) : v.isUnitary :=
  v.unitaryProof

commit-pinned source · Verso Blueprint panel

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

theorem correct {α : Type u} {rows cols : Nat}
    (v : VerifiedBlockEncoding α rows cols) : v.blockCorrect :=
  v.blockProof

commit-pinned source · Verso Blueprint panel

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

theorem resource_ok {α : Type u} {rows cols : Nat}
    (v : VerifiedBlockEncoding α rows cols) : v.resourceBound :=
  v.resourceProof

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “construction claim”. A proposition-valued field is a requirement until a constructor supplies it. A high-level construction claim imported from a paper or generated by AI.

structure ConstructionClaim where
  name : String
  source : String
  target : String
  normalization : String
  layout : String
  resource : AsymptoticResource
deriving Repr, DecidableEq

commit-pinned source · Verso Blueprint panel