7.2. QuantumBlockEncoding/BandedSparseAccessPrimitive.lean🔗

13 explicit public declarations, in source order.

Definition7.2.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive word 3”. Decode three little-endian wires as an element of 'Fin 8'.

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. Decode three little-endian wires as an element of 'Fin 8'.

Declaration kind. def.

Source: QuantumBlockEncoding/BandedSparseAccessPrimitive.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.2.1●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (wire0 wire1 wire2 : Fin 7) : Fin 8

def QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (wire0 wire1 wire2 : Fin 7) : Fin 8

Decode three little-endian wires as an element of `Fin 8`.

Definition7.2.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive offset 3”. The concrete source loader used by the fixed witness: 's ↦ s XOR 3'.

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 concrete source loader used by the fixed witness: 's ↦ s XOR 3'.

Declaration kind. def.

Source: QuantumBlockEncoding/BandedSparseAccessPrimitive.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.2.2●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3
  (slot : Fin 8) : Fin 8

def QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3
  (slot : Fin 8) : Fin 8

The concrete source loader used by the fixed witness: `s ↦ s XOR 3`.

Theorem7.2.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive offset 3 table”; 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/BandedSparseAccessPrimitive.lean:32. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem7.2.3●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3_table :
  List.ofFn QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3 =
    [3, 2, 1, 0, 7, 6, 5, 4]

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3_table :
  List.ofFn
      QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3 =
    [3, 2, 1, 0, 7, 6, 5, 4]

Definition7.2.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive access 3 reversible program”. Wire order is 'address[0..2], row[0..2], work'.

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. Wire order is 'address[0..2], row[0..2], work'. Two 'X' gates implement the source loader and the existing exact three-bit adder implements modular SUM.

Declaration kind. def.

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

Lean code for Definition7.2.4●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3ReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 7

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3ReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 7

Wire order is `address[0..2], row[0..2], work`.  Two `X` gates implement the
source loader and the existing exact three-bit adder implements modular SUM.

Definition7.2.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive access 3 basis equiv”. Full-space reversible semantics of the fixed primitive witness.

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. Full-space reversible semantics of the fixed primitive witness.

Declaration kind. def.

Source: QuantumBlockEncoding/BandedSparseAccessPrimitive.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.2.5●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 7 ≃
    QuantumBlockEncoding.PrimitiveBasis 7

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 7 ≃
    QuantumBlockEncoding.PrimitiveBasis 7

Full-space reversible semantics of the fixed primitive witness.

Theorem7.2.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 clean action”; the hypotheses and conclusion in the code panel fix its exact scope. Exact clean-workspace action of the expanded access circuit.

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. Exact clean-workspace action of the expanded access circuit.

Declaration kind. theorem.

Source: QuantumBlockEncoding/BandedSparseAccessPrimitive.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.2.6●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_cleanAction
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  have output :=
    QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
      state;
  QuantumBlockEncoding.BandedSparseAccess.primitiveWord3 output 0 1 2 =
      ⟨(↑(QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3
                (QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
                  state 0 1 2)) +
            ↑(QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
                state 3 4 5)) %
          8,
        ⋯⟩ ∧
    QuantumBlockEncoding.BandedSparseAccess.primitiveWord3 output 3 4
          5 =
        QuantumBlockEncoding.BandedSparseAccess.primitiveWord3 state 3 4
          5 ∧
      output 6 = 0

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_cleanAction
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  have output :=
    QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
      state;
  QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
        output 0 1 2 =
      ⟨(↑(QuantumBlockEncoding.BandedSparseAccess.primitiveOffset3
                (QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
                  state 0 1 2)) +
            ↑(QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
                state 3 4 5)) %
          8,
        ⋯⟩ ∧
    QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
          output 3 4 5 =
        QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
          state 3 4 5 ∧
      output 6 = 0

Exact clean-workspace action of the expanded access circuit.

Theorem7.2.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 preserves row”; the hypotheses and conclusion in the code panel fix its exact scope. The row register is preserved by the primitive witness.

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 by the primitive witness.

Declaration kind. theorem.

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

Lean code for Theorem7.2.7●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_preserves_row
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
      (QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
        state)
      3 4 5 =
    QuantumBlockEncoding.BandedSparseAccess.primitiveWord3 state 3 4 5

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_preserves_row
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
      (QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
        state)
      3 4 5 =
    QuantumBlockEncoding.BandedSparseAccess.primitiveWord3
      state 3 4 5

The row register is preserved by the primitive witness.

Theorem7.2.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable work qubit is returned to zero.

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 reusable work qubit is returned to zero.

Declaration kind. theorem.

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

Lean code for Theorem7.2.8●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_workspaceClean
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
      state 6 =
    0

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_workspaceClean
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv
      state 6 =
    0

The reusable work qubit is returned to zero.

Definition7.2.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive access 3 program”. Primitive compilation contains no opaque oracle instruction.

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. Primitive compilation contains no opaque oracle instruction.

Declaration kind. def.

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

Lean code for Definition7.2.9●1 definition

defdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program :
  QuantumBlockEncoding.PrimitiveProgram 7

def QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program :
  QuantumBlockEncoding.PrimitiveProgram 7

Primitive compilation contains no opaque oracle instruction.

Theorem7.2.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 program eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix refinement from the emitted primitive list to the reversible map.

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. Exact matrix refinement from the emitted primitive list to the reversible map.

Declaration kind. theorem.

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

Lean code for Theorem7.2.10●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3BasisEquiv

Exact matrix refinement from the emitted primitive list to the reversible map.

Theorem7.2.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 program resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional: the score is computed from the gate list.

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. Resource ownership is definitional: the score is computed from the gate list.

Declaration kind. theorem.

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

Lean code for Theorem7.2.11●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_resource_faithful :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.resource =
    QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.circuit.resource

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_resource_faithful :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.resource =
    QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.circuit.resource

Resource ownership is definitional: the score is computed from the gate list.

Theorem7.2.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 program oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope. The expanded witness has zero unresolved oracle calls.

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 expanded witness has zero unresolved oracle calls.

Declaration kind. theorem.

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

Lean code for Theorem7.2.12●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_oracleCalls_eq_zero :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_oracleCalls_eq_zero :
  QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program.resource.oracleCalls =
    0

The expanded witness has zero unresolved oracle calls.

Theorem7.2.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive access 3 program unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The primitive matrix is unitary because every emitted instruction 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 primitive matrix is unitary because every emitted instruction is unitary.

Declaration kind. theorem.

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

Lean code for Theorem7.2.13●1 theorem

theoremdefined in QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

complete

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_unitary :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program ∈
    Matrix.unitaryGroup (QuantumBlockEncoding.PrimitiveBasis 7) ℂ

theorem QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_unitary :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
        7)
      ℂ

The primitive matrix is unitary because every emitted instruction is unitary.