1.2. Evidence pipeline🔗

ASPBE evidence pipeline from user contract to public formal evidence

The diagram makes the promotion boundary explicit. Search agents may propose or repair a candidate, and finite execution can reveal a counterexample, but neither action establishes a symbolic theorem. Promotion occurs only when Lean accepts the named declaration under the stated contract. Documentation and executable exports remain downstream evidence with their own scopes.

Definition1.2.1

uses 0used by 1✓L∃∀N

For n qubits, a state-preparation target stores amplitudes indexed by \operatorname{Fin}(2^n) and an explicit normalization proposition. The source field records where the target came from; it is metadata and cannot replace the normalization proof.

Lean code for Definition1.2.1●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StatePreparation.lean

complete

structure QuantumBlockEncoding.StatePreparationTarget.{u} (α : Type u)
  (qubits : ℕ) : Type u

structure QuantumBlockEncoding.StatePreparationTarget.{u}
  (α : Type u) (qubits : ℕ) : Type u

A normalized state requested by the user.

Fields

amplitudes : Fin (QuantumBlockEncoding.gridSize qubits) → α

normalization : Prop

source : String

Definition1.2.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 1.2.3

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

A state-preparation candidate supplies a matrix, a circuit transcript, a schedule, resources, and a unitarity proposition. Promotion to a verified certificate requires proofs of normalization, unitarity, and first-column equality. Thus the user-level condition is U|0^n\rangle=|\psi\rangle.

Lean code for Definition1.2.2●1 definition

structure(4 fields)defined in QuantumBlockEncoding/StatePreparation.lean

complete

structure QuantumBlockEncoding.VerifiedStatePreparation.{u} (α : Type u)
  (qubits : ℕ) : Type u

structure QuantumBlockEncoding.VerifiedStatePreparation.{u}
  (α : Type u) (qubits : ℕ) : Type u

A candidate promoted by proofs of normalization, unitarity, and state action.

Fields

candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits

normalizationProof : self.candidate.target.normalization

unitaryProof : self.candidate.isUnitary

preparationProof : self.candidate.preparesTarget

Theorem1.2.3

uses 1used by 0✓L∃∀N

The Mathlib swap matrix supplies the Pauli X gate. Its self-inverse property proves unitarity, and its zero-input column is |1\rangle. The resulting certificate includes the logical circuit, schedule, and one-gate resource record.

Lean code for Theorem1.2.3●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.target.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate.target.amplitudes

The certified Pauli X example states the familiar textbook equation.

Theorem1.2.4

uses 1used by 0✓L∃∀N

The standard Hadamard matrix is proved unitary over \mathbb C, its equal-superposition target is proved normalized, and concrete matrix-vector action gives H|0\rangle=(|0\rangle+|1\rangle)/\sqrt 2.

Lean code for Theorem1.2.4●1 theorem

theoremdefined in QuantumBlockEncoding/TextbookStatePreparation.lean

complete

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 1) =
    QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.target.amplitudes

theorem QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        1) =
    QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate.target.amplitudes

The certified Hadamard example prepares the equal superposition.

Definition1.2.5

uses 0used by 1✓L∃∀N

An operator task records a finite matrix A, a normalizer \alpha, its provenance, its semantic contract, and any free parameters. The access model and normalization remain visible inputs rather than hidden assumptions.

Lean code for Definition1.2.5●1 definition

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

complete

structure QuantumBlockEncoding.QueryOperatorTarget.{u} (α : Type u)
  (rows cols : ℕ) : Type u

structure QuantumBlockEncoding.QueryOperatorTarget.{u}
  (α : Type u) (rows cols : ℕ) : Type u

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.

Fields

operator : QuantumBlockEncoding.Matrix rows cols α

normalizer : α

source : String

semanticContract : String

freeParameters : List String

Definition1.2.6

uses 1used by 1✓L∃∀N

For an n-qubit target and a auxiliaries, the candidate matrix acts on 2^{n+a} dimensions. It carries the register layout, circuit, schedule, resource count, and two separate propositions: unitarity and containment of the normalized target in the selected block.

Lean code for Definition1.2.6●1 definition

structure(10 fields)defined in QuantumBlockEncoding/BlockEncoding.lean

complete

structure QuantumBlockEncoding.OperatorBlockEncodingCandidate.{u} (α : Type u)
  (systemQubits : ℕ) : Type u

structure QuantumBlockEncoding.OperatorBlockEncodingCandidate.{u}
  (α : Type u) (systemQubits : ℕ) : Type u

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
unitary acts on `2^(n+a)` dimensions.

Fields

auxiliaryQubits : ℕ

target : QuantumBlockEncoding.QueryOperatorTarget α (QuantumBlockEncoding.gridSize systemQubits)
  (QuantumBlockEncoding.gridSize systemQubits)

unitary : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.gridSize (systemQubits + self.auxiliaryQubits))
  (QuantumBlockEncoding.gridSize (systemQubits + self.auxiliaryQubits)) α

layout : QuantumBlockEncoding.RegisterLayout

circuit : QuantumBlockEncoding.Circuit

schedule : QuantumBlockEncoding.LayeredCircuit

resource : QuantumBlockEncoding.Resource

layoutMatches : self.layout.auxiliaryQubits = self.auxiliaryQubits

isUnitary : Prop

blockContainsTarget : Prop

Definition1.2.7

uses 1used by 1✓L∃∀N

The verified record contains proofs of the candidate's unitarity and block predicate. It is the smallest user-facing certificate that closes both semantic leaves. A clean-block-only package is a reusable intermediate result, not automatically this full certificate.

Lean code for Definition1.2.7●1 definition

structure(3 fields)defined in QuantumBlockEncoding/BlockEncoding.lean

complete

structure QuantumBlockEncoding.VerifiedOperatorBlockEncoding.{u} (α : Type u)
  (systemQubits : ℕ) : Type u

structure QuantumBlockEncoding.VerifiedOperatorBlockEncoding.{u}
  (α : Type u) (systemQubits : ℕ) : Type u

A verified candidate with explicit proofs of unitarity and block containment.

Fields

candidate : QuantumBlockEncoding.OperatorBlockEncodingCandidate α systemQubits

unitaryProof : self.candidate.isUnitary

blockProof : self.candidate.blockContainsTarget

Definition1.2.8

uses 0used by 0✓L∃∀N

Candidates at the same semantic tier are compared lexicographically by gate count, circuit depth, auxiliary qubits, and unresolved oracle calls. Normalizer quality and proof status are assessed before this concrete score.

Lean code for Definition1.2.8●1 definition

structure(4 fields)defined in QuantumBlockEncoding/BlockEncoding.lean

complete

structure QuantumBlockEncoding.BlockEncodingCost : Type

structure QuantumBlockEncoding.BlockEncodingCost :
  Type

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

1. fewer gates,
2. smaller circuit depth,
3. fewer auxiliary qubits,
4. fewer unresolved oracle calls.

Fields

auxiliaryQubits : ℕ

gateCount : ℕ

depth : ℕ

oracleCalls : ℕ

Theorem1.2.9

uses 1used by 0✓L∃∀N

When the approximate backend uses exact block containment as its zero-error proposition, every verified exact certificate can seed approximate search with \varepsilon=0. This is an adapter, not a claim about an unstated operator norm.

Lean code for Theorem1.2.9●1 definition

defdefined in QuantumBlockEncoding/BlockEncoding.lean

complete

def QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox.{u_1}
  {α : Type u_1} {systemQubits : ℕ} [OfNat α 0]
  (v :
    QuantumBlockEncoding.VerifiedOperatorBlockEncoding α systemQubits) :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding α
    systemQubits

def QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  [OfNat α 0]
  (v :
    QuantumBlockEncoding.VerifiedOperatorBlockEncoding
      α systemQubits) :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding
    α systemQubits

Package an exact certificate as a zero-error approximate certificate when the
chosen approximate proposition is the same exact block predicate.  Analytic
backends can later replace this with a theorem connecting exact block equality
to a concrete operator-norm inequality.