3. Reusable block-encoding routes🔗

Construction routes are proof patterns, not labels inferred from a matrix alone. Each route names the access model, normalization, cleanup requirement, and final reusable Lean leaf.

Theorem3.1

uses 0used by 1✓L∃∀N

For a finite map p, the permutation-matrix entry selected by an embedding e is U(e(i),e(j))=\begin{cases}1,&e(i)=p(e(j)),\\0,&\text{otherwise.}\end{cases} Concrete tasks reduce their block proof to a finite image calculation.

Lean code for Theorem3.1●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_entry
  {system total : ℕ} (embed : Fin system → Fin total)
  (p : Fin total → Fin total) (row col : Fin system) :
  QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy embed
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix p) row
      col =
    if embed row = p (embed col) then 1 else 0

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_entry
  {system total : ℕ}
  (embed : Fin system → Fin total)
  (p : Fin total → Fin total)
  (row col : Fin system) :
  QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
      embed
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
        p)
      row col =
    if embed row = p (embed col) then 1
    else 0

Core `BE.PermMatrix.CleanBlock` leaf: the clean block of a permutation matrix is
just the finite image predicate restricted to clean embedded rows and columns.

Theorem3.2

uses 1used by 1✓L∃∀N

If the finite image formula agrees with a target A at every pair of system indices, the whole selected block is pointwise equal to A.

Lean code for Theorem3.2●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_eq_target_of_entry
  {system total : ℕ} (embed : Fin system → Fin total)
  (p : Fin total → Fin total)
  (A : QuantumBlockEncoding.Matrix system system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if embed row = p (embed col) then 1 else 0) = A row col) :
  (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy embed
        (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
          p)).PointwiseEq
    A

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_permMatrix_eq_target_of_entry
  {system total : ℕ}
  (embed : Fin system → Fin total)
  (p : Fin total → Fin total)
  (A :
    QuantumBlockEncoding.Matrix system
      system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if embed row = p (embed col) then 1
        else 0) =
        A row col) :
  (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
        embed
        (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
          p)).PointwiseEq
    A

Entrywise bridge from a finite image calculation to an exact clean block.  This
is the leaf that converts a successful finite reversible construction into the
block-entry theorem lower agents usually need.

Definition3.3

uses 1used by 0✓L∃∀N

An embedding, a finite image map, a target matrix, and the entry theorem compile into an exact clean-block certificate. This is the preferred route for matrix units, projectors, resets on a subspace, and partial injections when the completion is explicit.

Lean code for Definition3.3●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
  {system total : ℕ} (embed : Fin system → Fin total)
  (p : Fin total → Fin total)
  (A : QuantumBlockEncoding.Matrix system system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if embed row = p (embed col) then 1 else 0) = A row col) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
    total

def QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
  {system total : ℕ}
  (embed : Fin system → Fin total)
  (p : Fin total → Fin total)
  (A :
    QuantumBlockEncoding.Matrix system
      system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if embed row = p (embed col) then 1
        else 0) =
        A row col) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
    system total

Abstract partial-permutation certificate.  A concrete task supplies the
embedding, finite image, target matrix, and image-entry theorem; this wrapper
returns a reusable exact clean-block certificate.

Definition3.4

uses 0used by 0✓L∃∀N

The one-sparse interface packages a support map and the proof that all target entries reduce to the corresponding Kronecker-delta support. It is appropriate when each column has at most one possible nonzero row.

Lean code for Definition3.4●1 definition

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

complete

structure QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate
  (n : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate
  (n : ℕ) : Type

Proof-carrying one-sparse certificate.  This is the exact finite leaf behind
the textbook one-sparse block-encoding route after the amplitude and location
oracles have been reduced to a support map.

Fields

supportMap : Fin n → Fin n

target : QuantumBlockEncoding.Matrix n n ℚ

supportProof : ∀ (row col : Fin n), row ≠ self.supportMap col → self.target row col = 0

Definition3.5

uses 0used by 0✓L∃∀N

Sparse certificates expose the finite slot sum that must collapse. They do not assume uniqueness: the task must supply the no-hit or unique-hit proof and, for the general route, correct row and column access.

Lean code for Definition3.5●2 definitions

structure(6 fields)defined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

structure QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate
  (rows cols slots : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate
  (rows cols slots : ℕ) : Type

Proof-carrying sparse-column contract.  The contract is not a theorem by
itself; it records the exact clean-entry theorem a paper-specific lower agent
must supply.

Fields

cleanBlock : QuantumBlockEncoding.Matrix rows cols ℚ

target : QuantumBlockEncoding.Matrix rows cols ℚ

normalizer : ℚ

locationOracle : String

valueOracle : String

blockProof : self.cleanBlock.PointwiseEq self.target

structure(7 fields)defined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

structure QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate
  (rows cols slots : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate
  (rows cols slots : ℕ) : Type

Proof-carrying row/column sparse contract for the general sparse route.

Fields

cleanBlock : QuantumBlockEncoding.Matrix rows cols ℚ

target : QuantumBlockEncoding.Matrix rows cols ℚ

normalizer : ℚ

columnOracle : String

rowOracle : String

valueOracle : String

blockProof : self.cleanBlock.PointwiseEq self.target

Definition3.6

uses 0used by 0✓L∃∀N

A reversible value oracle may feed a controlled rotation only when the amplitude entry and workspace cleanup are both proved. The record prevents compute-rotate-uncompute from hiding a dirty ancilla.

Lean code for Definition3.6●1 definition

structure(7 fields)defined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

structure QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract
  (rows cols : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract
  (rows cols : ℕ) : Type

Value-to-amplitude oracle contract.  A task may use this only after it supplies
both cleanup and amplitude-entry proofs; the record cannot close a proof by
itself.

Fields

cleanAmplitude : QuantumBlockEncoding.Matrix rows cols ℚ

targetAmplitude : QuantumBlockEncoding.Matrix rows cols ℚ

valueOracleDescription : String

rotationDescription : String

cleanupStatement : Prop

cleanupProof : self.cleanupStatement

amplitudeProof : self.cleanAmplitude.PointwiseEq self.targetAmplitude

Definition3.7

uses 0used by 1✓L∃∀N

At the arithmetic layer, an LCU certificate stores the extracted clean block, target, normalizer, term count, and pointwise equality. PREPARE-SELECT semantics must be proved before a physical circuit is identified with this arithmetic object.

Lean code for Definition3.7●1 definition

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

complete

structure QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate (system : ℕ) :
  Type

structure QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
  (system : ℕ) : Type

Proof-carrying LCU contract.  Full PREPARE-SELECT algebra can later instantiate
`cleanBlock`; downstream arithmetic should only depend on the exposed
`blockProof`.

Fields

cleanBlock : QuantumBlockEncoding.Matrix system system ℚ

target : QuantumBlockEncoding.Matrix system system ℚ

normalizer : ℚ

termCount : ℕ

blockProof : self.cleanBlock.PointwiseEq self.target

Theorem3.8

uses 1used by 0✓L∃∀N

Once both input blocks are certified, the two-term constructor proves each output entry equals w_L A_L(i,j)+w_R A_R(i,j). The normalizer and term count are carried by the certificate.

Lean code for Theorem3.8●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate_cleanBlock_entry
  {system : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system)
  (leftWeight rightWeight : ℚ) (row col : Fin system) :
  (QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate left
          right leftWeight rightWeight).cleanBlock
      row col =
    leftWeight * left.target row col +
      rightWeight * right.target row col

theorem QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate_cleanBlock_entry
  {system : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
      system)
  (leftWeight rightWeight : ℚ)
  (row col : Fin system) :
  (QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate
          left right leftWeight
          rightWeight).cleanBlock
      row col =
    leftWeight * left.target row col +
      rightWeight * right.target row col

Theorem3.9

uses 1used by 1✓L∃∀N

Pointwise-equal component matrices remain pointwise equal after finite matrix multiplication. This is the common compiled leaf for product composition after the embedded blocks have been extracted.

Lean code for Theorem3.9●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.matrix_mul_congr_pointwise
  {rows mid cols : ℕ} {A A' : QuantumBlockEncoding.Matrix rows mid ℚ}
  {B B' : QuantumBlockEncoding.Matrix mid cols ℚ}
  (hA : A.PointwiseEq A') (hB : B.PointwiseEq B') :
  (A.mul B).PointwiseEq (A'.mul B')

theorem QuantumBlockEncoding.BlockEncodingClassics.matrix_mul_congr_pointwise
  {rows mid cols : ℕ}
  {A A' :
    QuantumBlockEncoding.Matrix rows mid
      ℚ}
  {B B' :
    QuantumBlockEncoding.Matrix mid cols
      ℚ}
  (hA : A.PointwiseEq A')
  (hB : B.PointwiseEq B') :
  (A.mul B).PointwiseEq (A'.mul B')

Definition3.10

uses 1used by 0✓L∃∀N

Two exact clean-block packages are promoted to the arithmetic interface and combined into a certificate for the product of their targets. Circuit depth and gate counts require separate resource proofs.

Lean code for Definition3.10●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate
  {system totalLeft totalRight : ℕ}
  (left :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      totalLeft)
  (right :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      totalRight) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system

def QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate
  {system totalLeft totalRight : ℕ}
  (left :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system totalLeft)
  (right :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system totalRight) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
    system

Product bridge for exact clean-block certificates via the arithmetic layer.

Definition3.11

uses 0used by 0✓L∃∀N

A non-Hermitian input is converted to a named doubled target with an explicit entry formula. The record exists to prevent later polynomial-transform arguments from silently assuming Hermiticity.

Lean code for Definition3.11●1 definition

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

complete

structure QuantumBlockEncoding.BlockEncodingClassics.HermitianDilationContract
  (n : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.HermitianDilationContract
  (n : ℕ) : Type

Hermitian-dilation target shape.  The complete block-matrix construction will
live in a richer matrix backend; the important reusable Lean leaf is that a
non-Hermitian target is explicitly converted into a named downstream target,
not silently treated as Hermitian.

Fields

source : QuantumBlockEncoding.Matrix n n ℚ

dilation : QuantumBlockEncoding.Matrix (2 * n) (2 * n) ℚ

entryFormula : Prop

entryProof : self.entryFormula

Definition3.12

uses 1used by 0✓L∃∀N

QSVT is downstream of a proved input block. The consumer record cannot be formed without that certificate and explicit polynomial side conditions; it is not a shortcut for constructing the original data-loading oracle.

Lean code for Definition3.12●1 definition

structure(6 fields)defined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

structure QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
  (system total : ℕ) : Type

structure QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
  (system total : ℕ) : Type

QSVT consumer contract.  QSVT is deliberately downstream of a proved block
encoding: this record cannot be built without an input block certificate.

Fields

input : QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system total

polynomialDescription : String

sideConditions : Prop

outputStatement : Prop

sideConditionProof : self.sideConditions

outputProof : self.outputStatement

Theorem3.13

uses 1used by 0✓L∃∀N

Every exact clean-block certificate supplies a zero-error incumbent for approximate search at the same semantic layer. A stronger operator-norm statement still requires its named norm bridge.

Lean code for Theorem3.13●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock_bound
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  (QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock
      cert).approximationBound

theorem QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock_bound
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  (QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock
      cert).approximationBound