QuantumBlockEncoding/BandedSparseAccess.lean

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

abbrev Word (n : Nat) := ZMod (2 ^ n)

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

commit-pinned source · Verso Blueprint panel

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

def slotWord (n : Nat) {l : Nat} (slot : Fin (2 ^ l)) : Word n :=
  slot.val

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

commit-pinned source · Verso Blueprint panel

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.

def modularSumEquiv (n : Nat) :
    (Word n × Word n) ≃ (Word n × Word n) where
  toFun pair := (pair.1 + pair.2, pair.2)
  invFun pair := (pair.1 - pair.2, pair.2)
  left_inv pair := by simp

commit-pinned source · Verso Blueprint panel

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.

def liftLoaderEquiv (n : Nat) (loader : Equiv.Perm (Word n)) :
    Equiv.Perm (Word n × Word n) :=
  Equiv.prodCongr loader (Equiv.refl _)

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

commit-pinned source · Verso Blueprint panel

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'.

def accessEquiv (n : Nat) (loader : Equiv.Perm (Word n)) :
    Equiv.Perm (Word n × Word n) :=
  (liftLoaderEquiv n loader).trans (modularSumEquiv n)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “modular sum equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem modularSumEquiv_apply (n : Nat) (address row : Word n) :
    modularSumEquiv n (address, row) = (address + row, row) :=
  rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “access equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem accessEquiv_apply (n : Nat)
    (loader : Equiv.Perm (Word n)) (address row : Word n) :
    accessEquiv n loader (address, row) = (loader address + row, row) :=
  rfl

/-- Definition 6 action on the clean sparse-selector input. -/

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

@[simp] theorem accessEquiv_preserves_row
    (n : Nat) (loader : Equiv.Perm (Word n))
    (input : Word n × Word n) :
    (accessEquiv n loader input).2 = input.2 :=
  rfl

/-- Exact matrix semantics induced by the reversible access map. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “access matrix”. Exact matrix semantics induced by the reversible access map.

def accessMatrix (n : Nat) (loader : Equiv.Perm (Word n)) :
    _root_.Matrix (Word n × Word n) (Word n × Word n) ℂ :=
  Robin.ComplexLCU.equivPermutationMatrix (accessEquiv n loader)

/-- The arbitrary-size semantic access construction is unitary. -/

commit-pinned source · Verso Blueprint panel

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.

theorem accessMatrix_unitary (n : Nat) (loader : Equiv.Perm (Word n)) :
    accessMatrix n loader ∈
      _root_.Matrix.unitaryGroup (Word n × Word n) ℂ :=
  Robin.ComplexLCU.equivPermutationMatrix_unitary _

/-- 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. -/

commit-pinned source · Verso Blueprint panel

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.

def paperSingleQubitUpperBound (n l : Nat) : Nat :=
  (2 ^ l + 1) * (32 * n - 48)

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

commit-pinned source · Verso Blueprint panel

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.

def paperCnotUpperBound (n l : Nat) : Nat :=
  25 * 2 ^ l * n - 36 * 2 ^ l + 32 * n - 48

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

commit-pinned source · Verso Blueprint panel

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.

def paperPureAncillaUpperBound (n : Nat) : Nat :=
  n - 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “paper single qubit upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem paperSingleQubitUpperBound_eq (n l : Nat) :
    paperSingleQubitUpperBound n l = (2 ^ l + 1) * (32 * n - 48) :=
  rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “paper cnot upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem paperCnotUpperBound_eq (n l : Nat) :
    paperCnotUpperBound n l =
      25 * 2 ^ l * n - 36 * 2 ^ l + 32 * n - 48 :=
  rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “paper pure ancilla upper bound eq”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem paperPureAncillaUpperBound_eq (n : Nat) :
    paperPureAncillaUpperBound n = n - 1 :=
  rfl

commit-pinned source · Verso Blueprint panel