7.3. QuantumBlockEncoding/BlockEncodingClassics.lean🔗

84 explicit public declarations, in source order.

Definition7.3.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “perm matrix”. Permutation-matrix entries for a finite basis map.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Permutation-matrix entries for a finite basis map.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:19. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.1●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.permMatrix {n : ℕ}
  (p : Fin n → Fin n) : QuantumBlockEncoding.Matrix n n ℚ

def QuantumBlockEncoding.BlockEncodingClassics.permMatrix
  {n : ℕ} (p : Fin n → Fin n) :
  QuantumBlockEncoding.Matrix n n ℚ

Permutation-matrix entries for a finite basis map.

Definition7.3.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “column inner”. Column inner products for rational matrix-level orthogonality checks.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Column inner products for rational matrix-level orthogonality checks.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:23. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.2●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.columnInner {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) (i j : Fin n) : ℚ

def QuantumBlockEncoding.BlockEncodingClassics.columnInner
  {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ)
  (i j : Fin n) : ℚ

Column inner products for rational matrix-level orthogonality checks.

Definition7.3.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “row inner”. Row inner products for rational matrix-level orthogonality checks.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Row inner products for rational matrix-level orthogonality checks.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:27. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.3●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.rowInner {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) (i j : Fin n) : ℚ

def QuantumBlockEncoding.BlockEncodingClassics.rowInner
  {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ)
  (i j : Fin n) : ℚ

Row inner products for rational matrix-level orthogonality checks.

Definition7.3.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “is rational orthogonal”. Rational orthogonality predicate for real-valued finite matrix backends: 'U^T U = I' and 'U U^T = I', expressed entrywise.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Rational orthogonality predicate for real-valued finite matrix backends: 'U^T U = I' and 'U U^T = I', expressed entrywise.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:34. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.4●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal {n : ℕ}
  (U : QuantumBlockEncoding.Matrix n n ℚ) : Prop

def QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
  {n : ℕ}
  (U :
    QuantumBlockEncoding.Matrix n n ℚ) :
  Prop

Rational orthogonality predicate for real-valued finite matrix backends:
`U^T U = I` and `U U^T = I`, expressed entrywise.

Definition7.3.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean block by”. Clean block induced by an embedding of the system basis into a larger basis.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Clean block induced by an embedding of the system basis into a larger basis.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:39. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.5●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.

Definition7.3.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “product index”. Canonical product-register embedding.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Canonical product-register embedding. If the full Hilbert basis is represented as 'ancilla × system', this maps '(a, s)' to the flattened index 'a * system + s'.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:48. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.6●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.productIndex
  {ancilla system : ℕ} (a : Fin ancilla) (s : Fin system) :
  Fin (ancilla * system)

def QuantumBlockEncoding.BlockEncodingClassics.productIndex
  {ancilla system : ℕ} (a : Fin ancilla)
  (s : Fin system) :
  Fin (ancilla * system)

Canonical product-register embedding.  If the full Hilbert basis is represented
as `ancilla × system`, this maps `(a, s)` to the flattened index
`a * system + s`.

Definition7.3.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean block product”. Clean block for a flattened 'ancilla × system' matrix.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Clean block for a flattened 'ancilla × system' matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:60. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.7●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
  {ancilla system : ℕ} (zero : Fin ancilla)
  (U :
    QuantumBlockEncoding.Matrix (ancilla * system) (ancilla * system)
      ℚ) :
  QuantumBlockEncoding.Matrix system system ℚ

def QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
  {ancilla system : ℕ}
  (zero : Fin ancilla)
  (U :
    QuantumBlockEncoding.Matrix
      (ancilla * system)
      (ancilla * system) ℚ) :
  QuantumBlockEncoding.Matrix system
    system ℚ

Clean block for a flattened `ancilla × system` matrix.

Theorem7.3.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean block by perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:69. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.8●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.

Theorem7.3.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean block product perm matrix entry”; the hypotheses and conclusion in the code panel fix its exact scope. Product-register version of 'cleanBlockBy_permMatrix_entry'.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Product-register version of 'cleanBlockBy_permMatrix_entry'. This is the standard entrywise bridge for block encodings whose clean ancilla is explicitly one register of a flattened product basis.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.9●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_permMatrix_entry
  {ancilla system : ℕ} (zero : Fin ancilla)
  (p : Fin (ancilla * system) → Fin (ancilla * system))
  (row col : Fin system) :
  QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct zero
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix p) row
      col =
    if
        QuantumBlockEncoding.BlockEncodingClassics.productIndex zero
            row =
          p
            (QuantumBlockEncoding.BlockEncodingClassics.productIndex
              zero col) then
      1
    else 0

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_permMatrix_entry
  {ancilla system : ℕ}
  (zero : Fin ancilla)
  (p :
    Fin (ancilla * system) →
      Fin (ancilla * system))
  (row col : Fin system) :
  QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
      zero
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
        p)
      row col =
    if
        QuantumBlockEncoding.BlockEncodingClassics.productIndex
            zero row =
          p
            (QuantumBlockEncoding.BlockEncodingClassics.productIndex
              zero col) then
      1
    else 0

Product-register version of `cleanBlockBy_permMatrix_entry`.  This is the
standard entrywise bridge for block encodings whose clean ancilla is explicitly
one register of a flattened product basis.

Theorem7.3.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean block by perm matrix eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise bridge from a finite image calculation to an exact clean block.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:93. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.10●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.

Theorem7.3.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean block product eq target of entry”; the hypotheses and conclusion in the code panel fix its exact scope. Pointwise extension principle for product-register clean blocks.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Pointwise extension principle for product-register clean blocks.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:104. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.11●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_eq_target_of_entry
  {ancilla system : ℕ} (zero : Fin ancilla)
  (p : Fin (ancilla * system) → Fin (ancilla * system))
  (A : QuantumBlockEncoding.Matrix system system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if
            QuantumBlockEncoding.BlockEncodingClassics.productIndex zero
                row =
              p
                (QuantumBlockEncoding.BlockEncodingClassics.productIndex
                  zero col) then
          1
        else 0) =
        A row col) :
  (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct zero
        (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
          p)).PointwiseEq
    A

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct_eq_target_of_entry
  {ancilla system : ℕ}
  (zero : Fin ancilla)
  (p :
    Fin (ancilla * system) →
      Fin (ancilla * system))
  (A :
    QuantumBlockEncoding.Matrix system
      system ℚ)
  (h :
    ∀ (row col : Fin system),
      (if
            QuantumBlockEncoding.BlockEncodingClassics.productIndex
                zero row =
              p
                (QuantumBlockEncoding.BlockEncodingClassics.productIndex
                  zero col) then
          1
        else 0) =
        A row col) :
  (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
        zero
        (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
          p)).PointwiseEq
    A

Pointwise extension principle for product-register clean blocks.

Definition7.3.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “kronecker rat”. Kronecker delta over the project-local rational matrix backend.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Kronecker delta over the project-local rational matrix backend.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:116. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.12●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.kroneckerRat {n : ℕ}
  (i j : Fin n) : ℚ

def QuantumBlockEncoding.BlockEncodingClassics.kroneckerRat
  {n : ℕ} (i j : Fin n) : ℚ

Kronecker delta over the project-local rational matrix backend.

Definition7.3.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “one sparse matrix”. Column one-sparse matrix with support map 'c': column 'j' has its possible nonzero entry at row 'c j', with amplitude 'amp j'.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Column one-sparse matrix with support map 'c': column 'j' has its possible nonzero entry at row 'c j', with amplitude 'amp j'.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:123. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.13●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix {n : ℕ}
  (c : Fin n → Fin n) (amp : Fin n → ℚ) :
  QuantumBlockEncoding.Matrix n n ℚ

def QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix
  {n : ℕ} (c : Fin n → Fin n)
  (amp : Fin n → ℚ) :
  QuantumBlockEncoding.Matrix n n ℚ

Column one-sparse matrix with support map `c`: column `j` has its possible
nonzero entry at row `c j`, with amplitude `amp j`.

Theorem7.3.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one sparse matrix entry if”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:127. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.14●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix_entry_if
  {n : ℕ} (c : Fin n → Fin n) (amp : Fin n → ℚ) (row col : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix c amp row
      col =
    if row = c col then amp col else 0

theorem QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix_entry_if
  {n : ℕ} (c : Fin n → Fin n)
  (amp : Fin n → ℚ) (row col : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix
      c amp row col =
    if row = c col then amp col else 0

Theorem7.3.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one sparse from support”; the hypotheses and conclusion in the code panel fix its exact scope. One-sparse reconstruction leaf.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. One-sparse reconstruction leaf. If a target matrix is supported only at 'row = c col', then its support map and column amplitudes reconstruct it entrywise.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:139. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.15●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.oneSparse_from_support
  {n : ℕ} (A : QuantumBlockEncoding.Matrix n n ℚ) (c : Fin n → Fin n)
  (hSupport : ∀ (row col : Fin n), row ≠ c col → A row col = 0) :
  (QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix c
        fun col => A (c col) col).PointwiseEq
    A

theorem QuantumBlockEncoding.BlockEncodingClassics.oneSparse_from_support
  {n : ℕ}
  (A : QuantumBlockEncoding.Matrix n n ℚ)
  (c : Fin n → Fin n)
  (hSupport :
    ∀ (row col : Fin n),
      row ≠ c col → A row col = 0) :
  (QuantumBlockEncoding.BlockEncodingClassics.oneSparseMatrix
        c fun col =>
        A (c col) col).PointwiseEq
    A

One-sparse reconstruction leaf.  If a target matrix is supported only at
`row = c col`, then its support map and column amplitudes reconstruct it
entrywise.

Definition7.3.16

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “one sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying one-sparse certificate.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:155. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.16●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

Definition7.3.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean block”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:163. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.17●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.cleanBlock
  {n : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate n) :
  QuantumBlockEncoding.Matrix n n ℚ

def QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.cleanBlock
  {n : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate
      n) :
  QuantumBlockEncoding.Matrix n n ℚ

Theorem7.3.18

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:166. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.18●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.correct
  {n : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate n) :
  cert.cleanBlock.PointwiseEq cert.target

theorem QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate.correct
  {n : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.OneSparseCertificate
      n) :
  cert.cleanBlock.PointwiseEq cert.target

Definition7.3.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sparse column clean entry”. Column sparse clean-entry expression: a finite sum over slot indices of value oracle entries times location deltas.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Column sparse clean-entry expression: a finite sum over slot indices of value oracle entries times location deltas. This is the entrywise target for Lin-style sparse column proofs before a task attaches its uniqueness lemmas.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:177. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.19●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry
  {rows cols slots : ℕ} (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

def QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry
  {rows cols slots : ℕ}
  (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

Column sparse clean-entry expression: a finite sum over slot indices of value
oracle entries times location deltas.  This is the entrywise target for
Lin-style sparse column proofs before a task attaches its uniqueness lemmas.

Theorem7.3.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “perm matrix column inner of injective”; the hypotheses and conclusion in the code panel fix its exact scope. Column Gram entries of a permutation matrix collapse by injectivity.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Column Gram entries of a permutation matrix collapse by injectivity.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:283. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.20●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_columnInner_of_injective
  {n : ℕ} (p : Fin n → Fin n) (hp : Function.Injective p)
  (i j : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.columnInner
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix p) i j =
    QuantumBlockEncoding.Matrix.identity n ℚ i j

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_columnInner_of_injective
  {n : ℕ} (p : Fin n → Fin n)
  (hp : Function.Injective p)
  (i j : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.columnInner
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
        p)
      i j =
    QuantumBlockEncoding.Matrix.identity n
      ℚ i j

Column Gram entries of a permutation matrix collapse by injectivity.

Theorem7.3.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “perm matrix row inner of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Row Gram entries of a permutation matrix collapse by bijectivity.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Row Gram entries of a permutation matrix collapse by bijectivity.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:330. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.21●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_rowInner_of_bijective
  {n : ℕ} (p : Fin n → Fin n)
  (hp : Function.Injective p ∧ Function.Surjective p) (i j : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.rowInner
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix p) i j =
    QuantumBlockEncoding.Matrix.identity n ℚ i j

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_rowInner_of_bijective
  {n : ℕ} (p : Fin n → Fin n)
  (hp :
    Function.Injective p ∧
      Function.Surjective p)
  (i j : Fin n) :
  QuantumBlockEncoding.BlockEncodingClassics.rowInner
      (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
        p)
      i j =
    QuantumBlockEncoding.Matrix.identity n
      ℚ i j

Row Gram entries of a permutation matrix collapse by bijectivity.

Theorem7.3.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “perm matrix is rational orthogonal of bijective”; the hypotheses and conclusion in the code panel fix its exact scope. A bijective finite image induces a rational orthogonal permutation matrix.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. A bijective finite image induces a rational orthogonal permutation matrix. This is the reusable bridge from finite permutation certificates to the matrix-level unitarity proxy used by the exploratory block-encoding tasks.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:389. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.22●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_isRationalOrthogonal_of_bijective
  {n : ℕ} (p : Fin n → Fin n)
  (hp : Function.Injective p ∧ Function.Surjective p) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    (QuantumBlockEncoding.BlockEncodingClassics.permMatrix p)

theorem QuantumBlockEncoding.BlockEncodingClassics.permMatrix_isRationalOrthogonal_of_bijective
  {n : ℕ} (p : Fin n → Fin n)
  (hp :
    Function.Injective p ∧
      Function.Surjective p) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
    (QuantumBlockEncoding.BlockEncodingClassics.permMatrix
      p)

A bijective finite image induces a rational orthogonal permutation matrix.
This is the reusable bridge from finite permutation certificates to the
matrix-level unitarity proxy used by the exploratory block-encoding tasks.

Theorem7.3.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse column clean entry no hit”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:396. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.23●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_no_hit
  {rows cols slots : ℕ} (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ) (row : Fin rows) (col : Fin cols)
  (hmiss : ∀ (slot : Fin slots), row ≠ loc col slot) :
  QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry loc
      value row col =
    0

theorem QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_no_hit
  {rows cols slots : ℕ}
  (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ)
  (row : Fin rows) (col : Fin cols)
  (hmiss :
    ∀ (slot : Fin slots),
      row ≠ loc col slot) :
  QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry
      loc value row col =
    0

Theorem7.3.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse column clean entry unique slot”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:409. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.24●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_unique_slot
  {rows cols slots : ℕ} (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ) (row : Fin rows) (col : Fin cols)
  (hit : Fin slots) (hhit : row = loc col hit)
  (hmiss : ∀ (slot : Fin slots), slot ≠ hit → row ≠ loc col slot) :
  QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry loc
      value row col =
    value hit col

theorem QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry_unique_slot
  {rows cols slots : ℕ}
  (loc : Fin cols → Fin slots → Fin rows)
  (value : Fin slots → Fin cols → ℚ)
  (row : Fin rows) (col : Fin cols)
  (hit : Fin slots)
  (hhit : row = loc col hit)
  (hmiss :
    ∀ (slot : Fin slots),
      slot ≠ hit → row ≠ loc col slot) :
  QuantumBlockEncoding.BlockEncodingClassics.sparseColumnCleanEntry
      loc value row col =
    value hit col

Definition7.3.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “row column sparse delta entry”. General row/column sparse delta expression.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. General row/column sparse delta expression. A paper-specific route must prove that row-location and column-location uniqueness collapse this finite double sum to the target entry divided by the sparsity normalizer.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:434. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.25●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.rowColumnSparseDeltaEntry
  {rows cols slots : ℕ} (colLoc : Fin cols → Fin slots → Fin rows)
  (rowLoc : Fin rows → Fin slots → Fin cols)
  (value : Fin rows → Fin cols → ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

def QuantumBlockEncoding.BlockEncodingClassics.rowColumnSparseDeltaEntry
  {rows cols slots : ℕ}
  (colLoc :
    Fin cols → Fin slots → Fin rows)
  (rowLoc :
    Fin rows → Fin slots → Fin cols)
  (value : Fin rows → Fin cols → ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

General row/column sparse delta expression.  A paper-specific route must prove
that row-location and column-location uniqueness collapse this finite double
sum to the target entry divided by the sparsity normalizer.

Definition7.3.26

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “sparse column certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying sparse-column contract.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:456. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.26●1 definition

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

Theorem7.3.27

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:466. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.27●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate.correct
  {rows cols slots : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate
      rows cols slots) :
  cert.cleanBlock.PointwiseEq cert.target

theorem QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate.correct
  {rows cols slots : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.SparseColumnCertificate
      rows cols slots) :
  cert.cleanBlock.PointwiseEq cert.target

Definition7.3.28

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “row column sparse certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying row/column sparse contract for the general sparse route.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

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

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:475. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.28●1 definition

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

Theorem7.3.29

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:486. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.29●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate.correct
  {rows cols slots : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate
      rows cols slots) :
  cert.cleanBlock.PointwiseEq cert.target

theorem QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate.correct
  {rows cols slots : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.RowColumnSparseCertificate
      rows cols slots) :
  cert.cleanBlock.PointwiseEq cert.target

Definition7.3.30

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “value to amplitude contract”. A proposition-valued field is a requirement until a constructor supplies it. Value-to-amplitude oracle contract.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:498. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.30●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

Theorem7.3.31

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:509. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.31●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract.correct
  {rows cols : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract
      rows cols) :
  cert.cleanAmplitude.PointwiseEq cert.targetAmplitude

theorem QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract.correct
  {rows cols : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ValueToAmplitudeContract
      rows cols) :
  cert.cleanAmplitude.PointwiseEq
    cert.targetAmplitude

Definition7.3.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “is symmetric”. Symmetric matrix predicate for the rational backend.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Symmetric matrix predicate for the rational backend.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:516. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.32●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric {n : ℕ}
  (A : QuantumBlockEncoding.Matrix n n ℚ) : Prop

def QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric
  {n : ℕ}
  (A :
    QuantumBlockEncoding.Matrix n n ℚ) :
  Prop

Symmetric matrix predicate for the rational backend.

Theorem7.3.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean block by symmetric of symmetric”; the hypotheses and conclusion in the code panel fix its exact scope. A symmetric full matrix has a symmetric clean block under any embedding.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. A symmetric full matrix has a symmetric clean block under any embedding.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:520. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.33●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_symmetric_of_symmetric
  {system total : ℕ} (embed : Fin system → Fin total)
  (U : QuantumBlockEncoding.Matrix total total ℚ)
  (hU : QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric U) :
  QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy embed U)

theorem QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy_symmetric_of_symmetric
  {system total : ℕ}
  (embed : Fin system → Fin total)
  (U :
    QuantumBlockEncoding.Matrix total
      total ℚ)
  (hU :
    QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric
      U) :
  QuantumBlockEncoding.BlockEncodingClassics.IsSymmetric
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
      embed U)

A symmetric full matrix has a symmetric clean block under any embedding.

Definition7.3.34

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “fin 2 zero”. Two-by-two scalar dilation block.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Two-by-two scalar dilation block. Unitarity requires a separate norm proof.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:528. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.34●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.fin2Zero : Fin 2

def QuantumBlockEncoding.BlockEncodingClassics.fin2Zero :
  Fin 2

Two-by-two scalar dilation block.  Unitarity requires a separate norm proof.

Definition7.3.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “fin 2 one”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:530. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.35●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.fin2One : Fin 2

def QuantumBlockEncoding.BlockEncodingClassics.fin2One :
  Fin 2

Definition7.3.36

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “scalar dilation”.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:532. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.36●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.scalarDilation (x y : ℚ) :
  QuantumBlockEncoding.Matrix 2 2 ℚ

def QuantumBlockEncoding.BlockEncodingClassics.scalarDilation
  (x y : ℚ) :
  QuantumBlockEncoding.Matrix 2 2 ℚ

Theorem7.3.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:539. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.37●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_cleanEntry
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    x

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_cleanEntry
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    x

Theorem7.3.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation offdiag 01”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:543. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.38●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag01
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    y

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag01
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    y

Theorem7.3.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation offdiag 10”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:547. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.39●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag10
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    y

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_offdiag10
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    y

Theorem7.3.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation diag 11”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:551. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.40●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_diag11
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    -x

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_diag11
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilation
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    -x

Definition7.3.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “scalar dilation row dot”. Two-entry row dot product for the scalar dilation block.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Two-entry row dot product for the scalar dilation block.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:556. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.41●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
  (x y : ℚ) (rowA rowB : Fin 2) : ℚ

def QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
  (x y : ℚ) (rowA rowB : Fin 2) : ℚ

Two-entry row dot product for the scalar dilation block.

Theorem7.3.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation row 0 norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:560. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.42●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_normSq
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    x * x + y * y

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_normSq
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    x * x + y * y

Theorem7.3.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation row 1 norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:564. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.43●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_normSq
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    x * x + y * y

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_normSq
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    x * x + y * y

Theorem7.3.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation row 0 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:573. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.44●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_unit_norm_of
  (x y : ℚ) (hunit : x * x + y * y = 1) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    1

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row0_unit_norm_of
  (x y : ℚ) (hunit : x * x + y * y = 1) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    1

Theorem7.3.45

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation row 1 unit norm of”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:578. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.45●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_unit_norm_of
  (x y : ℚ) (hunit : x * x + y * y = 1) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    1

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_row1_unit_norm_of
  (x y : ℚ) (hunit : x * x + y * y = 1) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    1

Theorem7.3.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation rows 01 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:583. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.46●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows01_orthogonal
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    0

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows01_orthogonal
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero
      QuantumBlockEncoding.BlockEncodingClassics.fin2One =
    0

Theorem7.3.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar dilation rows 10 orthogonal”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:590. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.47●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows10_orthogonal
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    0

theorem QuantumBlockEncoding.BlockEncodingClassics.scalarDilation_rows10_orthogonal
  (x y : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.scalarDilationRowDot
      x y
      QuantumBlockEncoding.BlockEncodingClassics.fin2One
      QuantumBlockEncoding.BlockEncodingClassics.fin2Zero =
    0

Definition7.3.48

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “chebyshev t”. Chebyshev polynomial values, kept as a small executable recurrence.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Chebyshev polynomial values, kept as a small executable recurrence.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:598. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.48●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.chebyshevT : ℕ → ℚ → ℚ

def QuantumBlockEncoding.BlockEncodingClassics.chebyshevT :
  ℕ → ℚ → ℚ

Chebyshev polynomial values, kept as a small executable recurrence.

Theorem7.3.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t zero”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:603. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.49●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_zero (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 0 x = 1

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_zero
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      0 x =
    1

Theorem7.3.50

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t one”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:605. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.50●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_one (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 1 x = x

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_one
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      1 x =
    x

Theorem7.3.51

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t two”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:607. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.51●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_two (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 2 x =
    2 * x * x - 1

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_two
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      2 x =
    2 * x * x - 1

Theorem7.3.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t succ succ”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:609. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.52●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_succ_succ (n : ℕ)
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT (n + 2) x =
    2 * x *
        QuantumBlockEncoding.BlockEncodingClassics.chebyshevT (n + 1)
          x -
      QuantumBlockEncoding.BlockEncodingClassics.chebyshevT n x

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_succ_succ
  (n : ℕ) (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      (n + 2) x =
    2 * x *
        QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
          (n + 1) x -
      QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
        n x

Theorem7.3.53

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t three recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:613. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.53●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_three_recurrence
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 3 x =
    2 * x * (2 * x * x - 1) - x

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_three_recurrence
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      3 x =
    2 * x * (2 * x * x - 1) - x

Theorem7.3.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “chebyshev t four recurrence”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:616. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.54●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_four_recurrence
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 4 x =
    2 * x * QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 3 x -
      QuantumBlockEncoding.BlockEncodingClassics.chebyshevT 2 x

theorem QuantumBlockEncoding.BlockEncodingClassics.chebyshevT_four_recurrence
  (x : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
      4 x =
    2 * x *
        QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
          3 x -
      QuantumBlockEncoding.BlockEncodingClassics.chebyshevT
        2 x

Definition7.3.55

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “exact clean block”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying exact clean-block package.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Proof-carrying exact clean-block package. This is smaller than the full operator-candidate record and is intended for reusable theorem arithmetic.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:623. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.55●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

Definition7.3.56

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean”. The certified clean block associated with a proof-carrying package.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The certified clean block associated with a proof-carrying package.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:632. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.56●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  QuantumBlockEncoding.Matrix system system ℚ

def QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.clean
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  QuantumBlockEncoding.Matrix system
    system ℚ

The certified clean block associated with a proof-carrying package.

Theorem7.3.57

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:636. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.57●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

Definition7.3.58

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “qubitization chebyshev contract”. A proposition-valued field is a requirement until a constructor supplies it. Qubitization/Chebyshev proof-carrying contract.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Qubitization/Chebyshev proof-carrying contract. The full qubitization theorem will instantiate this after the two-dimensional invariant-subspace calculation is formalized.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:648. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.58●1 definition

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

complete

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

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

Qubitization/Chebyshev proof-carrying contract.  The full qubitization theorem
will instantiate this after the two-dimensional invariant-subspace calculation
is formalized.

Fields

input : QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system total

degree : ℕ

output : QuantumBlockEncoding.Matrix system system ℚ

sideConditions : Prop

chebyshevStatement : Prop

sideConditionProof : self.sideConditions

chebyshevProof : self.chebyshevStatement

Definition7.3.59

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “partial permutation certificate”. Abstract partial-permutation certificate.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:662. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.59●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.

Definition7.3.60

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “one term lcu”. One-term LCU leaf.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. One-term LCU leaf. It is mathematically trivial, but useful for proof-DAG normalization: when an LCU population collapses to one term, the selected block is just that term.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:679. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.60●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU {system : ℕ}
  (A : QuantumBlockEncoding.Matrix system system ℚ) :
  QuantumBlockEncoding.Matrix system system ℚ

def QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU
  {system : ℕ}
  (A :
    QuantumBlockEncoding.Matrix system
      system ℚ) :
  QuantumBlockEncoding.Matrix system
    system ℚ

One-term LCU leaf.  It is mathematically trivial, but useful for proof-DAG
normalization: when an LCU population collapses to one term, the selected block
is just that term.

Theorem7.3.61

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one term lcu clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:682. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.61●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU_cleanBlock
  {system : ℕ} (A : QuantumBlockEncoding.Matrix system system ℚ) :
  (QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU A).PointwiseEq
    A

theorem QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU_cleanBlock
  {system : ℕ}
  (A :
    QuantumBlockEncoding.Matrix system
      system ℚ) :
  (QuantumBlockEncoding.BlockEncodingClassics.oneTermLCU
        A).PointwiseEq
    A

Definition7.3.62

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “matrix scale”. Pointwise scalar multiplication for the project-local matrix backend.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Pointwise scalar multiplication for the project-local matrix backend.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:689. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.62●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.matrixScale {rows cols : ℕ}
  (c : ℚ) (A : QuantumBlockEncoding.Matrix rows cols ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

def QuantumBlockEncoding.BlockEncodingClassics.matrixScale
  {rows cols : ℕ} (c : ℚ)
  (A :
    QuantumBlockEncoding.Matrix rows cols
      ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

Pointwise scalar multiplication for the project-local matrix backend.

Definition7.3.63

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “matrix add”. Pointwise addition for the project-local matrix backend.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Pointwise addition for the project-local matrix backend.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:693. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.63●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.matrixAdd {rows cols : ℕ}
  (A B : QuantumBlockEncoding.Matrix rows cols ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

def QuantumBlockEncoding.BlockEncodingClassics.matrixAdd
  {rows cols : ℕ}
  (A B :
    QuantumBlockEncoding.Matrix rows cols
      ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

Pointwise addition for the project-local matrix backend.

Definition7.3.64

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “weighted sum 2”. Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:697. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.64●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.weightedSum2 {rows cols : ℕ}
  (leftWeight rightWeight : ℚ)
  (left right : QuantumBlockEncoding.Matrix rows cols ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

def QuantumBlockEncoding.BlockEncodingClassics.weightedSum2
  {rows cols : ℕ}
  (leftWeight rightWeight : ℚ)
  (left right :
    QuantumBlockEncoding.Matrix rows cols
      ℚ) :
  QuantumBlockEncoding.Matrix rows cols ℚ

Two-term weighted sum, the finite clean-block algebra behind a 2-term LCU.

Theorem7.3.65

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “weighted sum 2 entry”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:701. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.65●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_entry
  {rows cols : ℕ} (leftWeight rightWeight : ℚ)
  (left right : QuantumBlockEncoding.Matrix rows cols ℚ)
  (row : Fin rows) (col : Fin cols) :
  QuantumBlockEncoding.BlockEncodingClassics.weightedSum2 leftWeight
      rightWeight left right row col =
    leftWeight * left row col + rightWeight * right row col

theorem QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_entry
  {rows cols : ℕ}
  (leftWeight rightWeight : ℚ)
  (left right :
    QuantumBlockEncoding.Matrix rows cols
      ℚ)
  (row : Fin rows) (col : Fin cols) :
  QuantumBlockEncoding.BlockEncodingClassics.weightedSum2
      leftWeight rightWeight left right
      row col =
    leftWeight * left row col +
      rightWeight * right row col

Theorem7.3.66

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “weighted sum 2 congr pointwise”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:707. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.66●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_congr_pointwise
  {rows cols : ℕ} {A A' B B' : QuantumBlockEncoding.Matrix rows cols ℚ}
  (leftWeight rightWeight : ℚ) (hA : A.PointwiseEq A')
  (hB : B.PointwiseEq B') :
  (QuantumBlockEncoding.BlockEncodingClassics.weightedSum2 leftWeight
        rightWeight A B).PointwiseEq
    (QuantumBlockEncoding.BlockEncodingClassics.weightedSum2 leftWeight
      rightWeight A' B')

theorem QuantumBlockEncoding.BlockEncodingClassics.weightedSum2_congr_pointwise
  {rows cols : ℕ}
  {A A' B B' :
    QuantumBlockEncoding.Matrix rows cols
      ℚ}
  (leftWeight rightWeight : ℚ)
  (hA : A.PointwiseEq A')
  (hB : B.PointwiseEq B') :
  (QuantumBlockEncoding.BlockEncodingClassics.weightedSum2
        leftWeight rightWeight A
        B).PointwiseEq
    (QuantumBlockEncoding.BlockEncodingClassics.weightedSum2
      leftWeight rightWeight A' B')

Definition7.3.67

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “lcu certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying LCU contract.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

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

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:722. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.67●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

Theorem7.3.68

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:731. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.68●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate.correct
  {system : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system) :
  cert.cleanBlock.PointwiseEq cert.target

theorem QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate.correct
  {system : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
      system) :
  cert.cleanBlock.PointwiseEq cert.target

Definition7.3.69

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “two term lcu certificate”. Two-term LCU arithmetic after both selected clean blocks have already been proved.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Two-term LCU arithmetic after both selected clean blocks have already been proved. Full PREPARE-SELECT-PREPARE dagger semantics should instantiate this leaf after proving the selected clean block equals the weighted sum.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:743. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.69●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate
  {system : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system)
  (leftWeight rightWeight : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system

def QuantumBlockEncoding.BlockEncodingClassics.twoTermLCUCertificate
  {system : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
      system)
  (leftWeight rightWeight : ℚ) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
    system

Two-term LCU arithmetic after both selected clean blocks have already been
proved.  Full PREPARE-SELECT-PREPARE dagger semantics should instantiate this
leaf after proving the selected clean block equals the weighted sum.

Theorem7.3.70

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “two term lcu certificate clean block entry”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:754. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.70●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

Definition7.3.71

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “to lcu certificate”. Promote an exact clean-block certificate to the LCU-style arithmetic layer.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Promote an exact clean-block certificate to the LCU-style arithmetic layer.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:764. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.71●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.toLCUCertificate
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total)
  (normalizer : ℚ := 1) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate system

def QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock.toLCUCertificate
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total)
  (normalizer : ℚ := 1) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
    system

Promote an exact clean-block certificate to the LCU-style arithmetic layer.

Theorem7.3.72

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “matrix mul congr pointwise”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:792. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.72●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')

Definition7.3.73

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “product clean block certificate”. Exact product certificate for already-extracted clean blocks.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Exact product certificate for already-extracted clean blocks.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:800. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.73●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.productCleanBlockCertificate
  {rows : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate rows) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate rows

def QuantumBlockEncoding.BlockEncodingClassics.productCleanBlockCertificate
  {rows : ℕ}
  (left right :
    QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
      rows) :
  QuantumBlockEncoding.BlockEncodingClassics.LCUCertificate
    rows

Exact product certificate for already-extracted clean blocks.

Definition7.3.74

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “product exact clean block certificate”. Product bridge for exact clean-block certificates via the arithmetic layer.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

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

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:811. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.74●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.

Definition7.3.75

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tensor resource cost”. Tensor-style resource score: parallel depth is the maximum of two depths.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Tensor-style resource score: parallel depth is the maximum of two depths.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:819. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.75●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost
  (x y : QuantumBlockEncoding.BlockEncodingCost) :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  QuantumBlockEncoding.BlockEncodingCost

Tensor-style resource score: parallel depth is the maximum of two depths.

Theorem7.3.76

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tensor resource cost gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:825. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.76●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_gateCount
  (x y : QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost x
        y).gateCount =
    x.gateCount + y.gateCount

theorem QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_gateCount
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost
        x y).gateCount =
    x.gateCount + y.gateCount

Theorem7.3.77

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tensor resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:828. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.77●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_depth
  (x y : QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost x
        y).depth =
    max x.depth y.depth

theorem QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost_depth
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.tensorResourceCost
        x y).depth =
    max x.depth y.depth

Definition7.3.78

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “product resource cost”. Product-style resource score: sequential depth adds.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Product-style resource score: sequential depth adds.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:832. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.78●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.productResourceCost
  (x y : QuantumBlockEncoding.BlockEncodingCost) :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.BlockEncodingClassics.productResourceCost
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  QuantumBlockEncoding.BlockEncodingCost

Product-style resource score: sequential depth adds.

Theorem7.3.79

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “product resource cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:838. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.79●1 theorem

theoremdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.productResourceCost_depth
  (x y : QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.productResourceCost x
        y).depth =
    x.depth + y.depth

theorem QuantumBlockEncoding.BlockEncodingClassics.productResourceCost_depth
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  (QuantumBlockEncoding.BlockEncodingClassics.productResourceCost
        x y).depth =
    x.depth + y.depth

Definition7.3.80

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “hermitian dilation contract”. A proposition-valued field is a requirement until a constructor supplies it. Hermitian-dilation target shape.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. 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.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:847. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.80●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

Definition7.3.81

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “qsvt consumer contract”. A proposition-valued field is a requirement until a constructor supplies it. QSVT consumer contract.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

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

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:857. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.81●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

Definition7.3.82

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “zero error approx clean block”. A proposition-valued field is a requirement until a constructor supplies it. Zero-error approximate incumbent at the clean-block level.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Zero-error approximate incumbent at the clean-block level.

Declaration kind. structure.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:866. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.82●1 definition

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

complete

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

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

Zero-error approximate incumbent at the clean-block level.

Fields

exact : QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system total

epsilon : ℚ

approximationBound : Prop

approximationProof : self.approximationBound

Definition7.3.83

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “exact as zero error approx clean block”. Any exact clean-block certificate can be used as a zero-error approximate incumbent in the adaptive exact-to-approximate ABEIS policy.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. Any exact clean-block certificate can be used as a zero-error approximate incumbent in the adaptive exact-to-approximate ABEIS policy.

Declaration kind. def.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:877. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition7.3.83●1 definition

defdefined in QuantumBlockEncoding/BlockEncodingClassics.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  QuantumBlockEncoding.BlockEncodingClassics.ZeroErrorApproxCleanBlock
    system total

def QuantumBlockEncoding.BlockEncodingClassics.exactAsZeroErrorApproxCleanBlock
  {system total : ℕ}
  (cert :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  QuantumBlockEncoding.BlockEncodingClassics.ZeroErrorApproxCleanBlock
    system total

Any exact clean-block certificate can be used as a zero-error approximate
incumbent in the adaptive exact-to-approximate ABEIS policy.

Theorem7.3.84

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exact as zero error approx clean block bound”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Reusable band-address, permutation, sparse, LCU, product, dilation, and QSVT-facing block-encoding routes.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BlockEncodingClassics.lean:885. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.3.84●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