ASPBE Lean Blueprint

2. Foundations: matrices, circuits, and semantic tiers🔗

The foundational layer is intentionally finite and explicit. Matrices are functions on finite indices; circuits are syntax; gate matrices and whole-circuit semantics are separate data. This keeps an entrywise matrix theorem from silently becoming a hardware claim.

Definition2.1
uses 0used by 0✓L∃∀N

The project-local matrix type represents an m-by-n matrix over \alpha as a function \operatorname{Fin}(m)\to\operatorname{Fin}(n)\to\alpha. Finite indexing makes clean-block equalities suitable for extensional and decision procedures.

Lean code for Definition2.1●1 definition
  • abbrevdefined in QuantumBlockEncoding/Core.lean
    complete
    abbrev QuantumBlockEncoding.Matrix.{u} (rows cols : ℕ) (α : Type u) : Type u
    abbrev QuantumBlockEncoding.Matrix.{u}
  (rows cols : ℕ) (α : Type u) : Type u
    A finite matrix represented by its entries.
Definition2.2
uses 0used by 0✓L∃∀N

The resource record separates gates, depth, oracle calls, and measurement calls. Its fields describe the chosen semantic tier; an unexpanded oracle call is not counted as a free physical gate.

Lean code for Definition2.2●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 : ℕ
Definition2.3
uses 0used by 0✓L∃∀N

A gate is a named one-qubit operation, a controlled gate, or a parallel composition. A circuit is a sequential list of gates. This syntax is lightweight enough for generated candidates while still retaining the register-level intent of each operation.

Lean code for Definition2.3●2 definitions
  • 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
  • abbrevdefined in QuantumBlockEncoding/Circuit.lean
    complete
    abbrev QuantumBlockEncoding.Circuit : Type
    abbrev QuantumBlockEncoding.Circuit : Type
Definition2.4
uses 0used by 0✓L∃∀N

A gate-matrix value couples one syntactic gate to a concrete matrix and a unitary-contract record. The coupling prevents a proof about a matrix from being advertised as a proof about an unrelated gate label.

Lean code for Definition2.4●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean
    complete
    structure QuantumBlockEncoding.GateMatrix.{u} (α : Type u) (qubits : ℕ) : Type u
    structure QuantumBlockEncoding.GateMatrix.{u}
  (α : Type u) (qubits : ℕ) : Type u
    One gate together with its matrix on the full `qubits`-qubit Hilbert space.
The matrix is supplied by a lower-level certificate for the gate family.

    Fields

    gate : QuantumBlockEncoding.Gate
    matrix : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.qubitDim qubits) (QuantumBlockEncoding.qubitDim qubits) α
    unitary : QuantumBlockEncoding.SemanticObligation
Definition2.5
uses 0used by 0✓L∃∀N

Whole-circuit semantics records the gate matrices, their alignment with the circuit transcript, the evaluated product matrix, and the semantic obligations needed by the chosen backend.

Lean code for Definition2.5●1 definition
  • structure(5 fields)defined in QuantumBlockEncoding/CircuitSemantics.lean
    complete
    structure QuantumBlockEncoding.CircuitMatrixSemantics.{u} (α : Type u) [OfNat α 0]
  [OfNat α 1] [HAdd α α α] [HMul α α α] (qubits : ℕ) : Type u
    structure QuantumBlockEncoding.CircuitMatrixSemantics.{u}
  (α : Type u) [OfNat α 0] [OfNat α 1]
  [HAdd α α α] [HMul α α α] (qubits : ℕ) :
  Type u
    Circuit-level matrix semantics assembled from gate-level matrices.

This does not certify that individual oracle matrices are correct; it gives the
project a stable Lean target for composing those certificates once they exist.

    Fields

    circuit : QuantumBlockEncoding.Circuit
    gateMatrices : List (QuantumBlockEncoding.GateMatrix α qubits)
    gateListMatches : QuantumBlockEncoding.gateMatricesMatchCircuit self.circuit self.gateMatrices = true
    matrix : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.qubitDim qubits) (QuantumBlockEncoding.qubitDim qubits) α
    matrix_eq_eval : self.matrix.PointwiseEq (QuantumBlockEncoding.evalGateMatrices self.gateMatrices)
Definition2.6
uses 0used by 1✓L∃∀N

Given an embedding e : \operatorname{Fin}(s)\to\operatorname{Fin}(t) and a full matrix U, the selected clean block is the s-dimensional matrix (i,j)\longmapsto U(e(i),e(j)). This definition states exactly which ancilla slice is projected.

Lean code for Definition2.6●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean
    complete
    def QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
  {system total : ℕ} (embed : Fin system → Fin total)
  (U : QuantumBlockEncoding.Matrix total total ℚ) :
  QuantumBlockEncoding.Matrix system system ℚ
    def QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
  {system total : ℕ}
  (embed : Fin system → Fin total)
  (U :
    QuantumBlockEncoding.Matrix total
      total ℚ) :
  QuantumBlockEncoding.Matrix system
    system ℚ
    Clean block induced by an embedding of the system basis into a larger basis.
Definition2.7
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 2.8
Loading preview
Reverse dependency preview content is loaded from the Blueprint HTML cache.
✓L∃∀N

The reusable arithmetic certificate packages U, its target A, the clean embedding, and a pointwise proof that the selected block equals A. It intentionally does not include unitarity, circuit realization, or resource optimality.

Lean code for Definition2.7●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/BlockEncodingClassics.lean
    complete
    structure QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
  (system total : ℕ) : Type
    structure QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
  (system total : ℕ) : Type
    Proof-carrying exact clean-block package.  This is smaller than the full
operator-candidate record and is intended for reusable theorem arithmetic.

    Fields

    U : QuantumBlockEncoding.Matrix total total ℚ
    A : QuantumBlockEncoding.Matrix system system ℚ
    embed : Fin system → Fin total
    blockProof : (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy self.embed self.U).PointwiseEq self.A
Theorem2.8
uses 1used by 0✓L∃∀N

For every exact clean-block package, its computed clean matrix is pointwise equal to its stored target matrix. Downstream LCU and product proofs consume this theorem rather than reopening the original finite-index calculation.

Lean code for Theorem2.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean
    complete
    theorem QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean_eq_target
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  cert.clean.PointwiseEq cert.A
    theorem QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean_eq_target
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  cert.clean.PointwiseEq cert.A
Definition2.9
uses 0used by 0XL∃∀N

ASPBE distinguishes four layers: (1) clean-entry or clean-block equality, (2) unitarity, permutation, or inverse correctness, (3) circuit realization and gate-matrix alignment, and (4) a resource score at a named implementation level. Claims are compared only after their layer is made explicit.