7.1. QuantumBlockEncoding/BandedSparseAccess.lean🔗

17 explicit public declarations, in source order.

Definition7.1.1

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “word”. An 'n'-qubit computational-basis word, represented modulo '2^n'.

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. An 'n'-qubit computational-basis word, represented modulo '2^n'.

Declaration kind. abbrev.

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

Lean code for Definition7.1.1●1 definition

abbrevdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

abbrev QuantumBlockEncoding.BandedSparseAccess.Word (n : ℕ) : Type

abbrev QuantumBlockEncoding.BandedSparseAccess.Word
  (n : ℕ) : Type

An `n`-qubit computational-basis word, represented modulo `2^n`.

Definition7.1.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “slot word”. The sparse selector embedded in the clean 'n'-qubit address register.

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 sparse selector embedded in the clean 'n'-qubit address register.

Declaration kind. def.

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

Lean code for Definition7.1.2●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.slotWord (n : ℕ) {l : ℕ}
  (slot : Fin (2 ^ l)) : QuantumBlockEncoding.BandedSparseAccess.Word n

def QuantumBlockEncoding.BandedSparseAccess.slotWord
  (n : ℕ) {l : ℕ} (slot : Fin (2 ^ l)) :
  QuantumBlockEncoding.BandedSparseAccess.Word
    n

The sparse selector embedded in the clean `n`-qubit address register.

Definition7.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “modular sum equiv”. Reversible modular SUM: add the second register into the first and preserve the second register.

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. Reversible modular SUM: add the second register into the first and preserve the second register. This is Eq. (53) of arXiv:2405.12855.

Declaration kind. def.

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

Lean code for Definition7.1.3●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv (n : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n ≃
    QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n

def QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv
  (n : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n ≃
    QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n

Reversible modular SUM: add the second register into the first and preserve
the second register.  This is Eq. (53) of arXiv:2405.12855.

Definition7.1.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift loader equiv”. Lift a reversible first-row address loader while leaving the row register untouched.

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. Lift a reversible first-row address loader while leaving the row register untouched.

Declaration kind. def.

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

Lean code for Definition7.1.4●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.liftLoaderEquiv (n : ℕ)
  (loader :
    Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n)) :
  Equiv.Perm
    (QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n)

def QuantumBlockEncoding.BandedSparseAccess.liftLoaderEquiv
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n)) :
  Equiv.Perm
    (QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n)

Lift a reversible first-row address loader while leaving the row register
untouched.

Definition7.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “access equiv”. The exact arbitrary-size banded-sparse-access semantics: load 'r_(s,0)', then add the row modulo '2^n'.

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 exact arbitrary-size banded-sparse-access semantics: load 'r_(s,0)', then add the row modulo '2^n'.

Declaration kind. def.

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

Lean code for Definition7.1.5●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.accessEquiv (n : ℕ)
  (loader :
    Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n)) :
  Equiv.Perm
    (QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n)

def QuantumBlockEncoding.BandedSparseAccess.accessEquiv
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n)) :
  Equiv.Perm
    (QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n)

The exact arbitrary-size banded-sparse-access semantics: load `r_(s,0)`,
then add the row modulo `2^n`.

Theorem7.1.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular sum equiv apply”; 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/BandedSparseAccess.lean:48. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.1.6●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv_apply (n : ℕ)
  (address row : QuantumBlockEncoding.BandedSparseAccess.Word n) :
  (QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv n)
      (address, row) =
    (address + row, row)

theorem QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv_apply
  (n : ℕ)
  (address row :
    QuantumBlockEncoding.BandedSparseAccess.Word
      n) :
  (QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv
        n)
      (address, row) =
    (address + row, row)

Theorem7.1.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “access equiv apply”; 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/BandedSparseAccess.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.1.7●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_apply (n : ℕ)
  (loader : Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n))
  (address row : QuantumBlockEncoding.BandedSparseAccess.Word n) :
  (QuantumBlockEncoding.BandedSparseAccess.accessEquiv n loader)
      (address, row) =
    (loader address + row, row)

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_apply
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n))
  (address row :
    QuantumBlockEncoding.BandedSparseAccess.Word
      n) :
  (QuantumBlockEncoding.BandedSparseAccess.accessEquiv
        n loader)
      (address, row) =
    (loader address + row, row)

Theorem7.1.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “access equiv clean slot”; the hypotheses and conclusion in the code panel fix its exact scope. Definition 6 action on the clean sparse-selector input.

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. Definition 6 action on the clean sparse-selector input.

Declaration kind. theorem.

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

Lean code for Theorem7.1.8●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot (n : ℕ)
  {l : ℕ}
  (offset :
    Fin (2 ^ l) → QuantumBlockEncoding.BandedSparseAccess.Word n)
  (loader : Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n))
  (loader_spec :
    ∀ (slot : Fin (2 ^ l)),
      loader (QuantumBlockEncoding.BandedSparseAccess.slotWord n slot) =
        offset slot)
  (slot : Fin (2 ^ l))
  (row : QuantumBlockEncoding.BandedSparseAccess.Word n) :
  (QuantumBlockEncoding.BandedSparseAccess.accessEquiv n loader)
      (QuantumBlockEncoding.BandedSparseAccess.slotWord n slot, row) =
    (offset slot + row, row)

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot
  (n : ℕ) {l : ℕ}
  (offset :
    Fin (2 ^ l) →
      QuantumBlockEncoding.BandedSparseAccess.Word
        n)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n))
  (loader_spec :
    ∀ (slot : Fin (2 ^ l)),
      loader
          (QuantumBlockEncoding.BandedSparseAccess.slotWord
            n slot) =
        offset slot)
  (slot : Fin (2 ^ l))
  (row :
    QuantumBlockEncoding.BandedSparseAccess.Word
      n) :
  (QuantumBlockEncoding.BandedSparseAccess.accessEquiv
        n loader)
      (QuantumBlockEncoding.BandedSparseAccess.slotWord
          n slot,
        row) =
    (offset slot + row, row)

Definition 6 action on the clean sparse-selector input.

Theorem7.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “access equiv preserves row”; the hypotheses and conclusion in the code panel fix its exact scope. The row register is preserved for every basis input, not only clean sparse selectors.

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 row register is preserved for every basis input, not only clean sparse selectors.

Declaration kind. theorem.

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

Lean code for Theorem7.1.9●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_preserves_row
  (n : ℕ)
  (loader : Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n))
  (input :
    QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n) :
  ((QuantumBlockEncoding.BandedSparseAccess.accessEquiv n loader)
        input).2 =
    input.2

theorem QuantumBlockEncoding.BandedSparseAccess.accessEquiv_preserves_row
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n))
  (input :
    QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n) :
  ((QuantumBlockEncoding.BandedSparseAccess.accessEquiv
          n loader)
        input).2 =
    input.2

The row register is preserved for every basis input, not only clean sparse
selectors.

Definition7.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “access matrix”. Exact matrix semantics induced by the reversible access 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. Exact matrix semantics induced by the reversible access map.

Declaration kind. def.

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

Lean code for Definition7.1.10●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.accessMatrix (n : ℕ)
  (loader :
    Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n)) :
  Matrix
    (QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n)
    (QuantumBlockEncoding.BandedSparseAccess.Word n ×
      QuantumBlockEncoding.BandedSparseAccess.Word n)
    ℂ

def QuantumBlockEncoding.BandedSparseAccess.accessMatrix
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n)) :
  Matrix
    (QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n)
    (QuantumBlockEncoding.BandedSparseAccess.Word
        n ×
      QuantumBlockEncoding.BandedSparseAccess.Word
        n)
    ℂ

Exact matrix semantics induced by the reversible access map.

Theorem7.1.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “access matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The arbitrary-size semantic access construction is unitary.

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 arbitrary-size semantic access construction is unitary.

Declaration kind. theorem.

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

Lean code for Theorem7.1.11●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary (n : ℕ)
  (loader :
    Equiv.Perm (QuantumBlockEncoding.BandedSparseAccess.Word n)) :
  QuantumBlockEncoding.BandedSparseAccess.accessMatrix n loader ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.BandedSparseAccess.Word n ×
        QuantumBlockEncoding.BandedSparseAccess.Word n)
      ℂ

theorem QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary
  (n : ℕ)
  (loader :
    Equiv.Perm
      (QuantumBlockEncoding.BandedSparseAccess.Word
        n)) :
  QuantumBlockEncoding.BandedSparseAccess.accessMatrix
      n loader ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.BandedSparseAccess.Word
          n ×
        QuantumBlockEncoding.BandedSparseAccess.Word
          n)
      ℂ

The arbitrary-size semantic access construction is unitary.

Definition7.1.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “paper single qubit upper bound”. Source-facing single-qubit upper bound printed in Lemma 1 of arXiv:2405.12855v3.

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. Source-facing single-qubit upper bound printed in Lemma 1 of arXiv:2405.12855v3. Natural subtraction is appropriate only in the paper's stated nontrivial register regime.

Declaration kind. def.

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

Lean code for Definition7.1.12●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound
  (n l : ℕ) : ℕ

def QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound
  (n l : ℕ) : ℕ

Source-facing single-qubit upper bound printed in Lemma 1 of
arXiv:2405.12855v3.  Natural subtraction is appropriate only in the paper's
stated nontrivial register regime.

Definition7.1.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “paper cnot upper bound”. Source-facing CNOT upper bound printed in the same lemma.

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. Source-facing CNOT upper bound printed in the same lemma.

Declaration kind. def.

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

Lean code for Definition7.1.13●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound (n l : ℕ) :
  ℕ

def QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound
  (n l : ℕ) : ℕ

Source-facing CNOT upper bound printed in the same lemma.

Definition7.1.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “paper pure ancilla upper bound”. Source-facing clean-ancilla upper bound printed in the same lemma.

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. Source-facing clean-ancilla upper bound printed in the same lemma.

Declaration kind. def.

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

Lean code for Definition7.1.14●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound
  (n : ℕ) : ℕ

def QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound
  (n : ℕ) : ℕ

Source-facing clean-ancilla upper bound printed in the same lemma.

Theorem7.1.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “paper single qubit upper bound eq”; 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/BandedSparseAccess.lean:101. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.1.15●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound_eq
  (n l : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound n
      l =
    (2 ^ l + 1) * (32 * n - 48)

theorem QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound_eq
  (n l : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperSingleQubitUpperBound
      n l =
    (2 ^ l + 1) * (32 * n - 48)

Theorem7.1.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “paper cnot upper bound eq”; 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/BandedSparseAccess.lean:105. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.1.16●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound_eq
  (n l : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound n l =
    25 * 2 ^ l * n - 36 * 2 ^ l + 32 * n - 48

theorem QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound_eq
  (n l : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperCnotUpperBound
      n l =
    25 * 2 ^ l * n - 36 * 2 ^ l + 32 * n -
      48

Theorem7.1.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “paper pure ancilla upper bound eq”; 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/BandedSparseAccess.lean:110. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.1.17●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccess.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound_eq
  (n : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound n =
    n - 1

theorem QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound_eq
  (n : ℕ) :
  QuantumBlockEncoding.BandedSparseAccess.paperPureAncillaUpperBound
      n =
    n - 1