6.3. QuantumBlockEncoding/ModularAdder3.lean🔗

22 explicit public declarations, in source order.

Definition6.3.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “primitive x program”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:16. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.1●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.primitiveXProgram {qubits : ℕ}
  (target : Fin qubits) : QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.primitiveXProgram
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Theorem6.3.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “primitive x program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:21. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.2●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.primitiveXProgram_eval {qubits : ℕ}
  (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveXProgram target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.xBasisEquiv target)

theorem QuantumBlockEncoding.primitiveXProgram_eval
  {qubits : ℕ} (target : Fin qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.primitiveXProgram
        target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.xBasisEquiv
        target)

Definition6.3.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile reversible gate”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:31. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.3●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.compileReversibleGate {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleGate qubits →
    QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.compileReversibleGate
  {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleGate
      qubits →
    QuantumBlockEncoding.PrimitiveProgram
      qubits

Theorem6.3.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile reversible gate eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:40. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.4●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.compileReversibleGate_eval {qubits : ℕ}
  (gate : QuantumBlockEncoding.ReversibleGate qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.compileReversibleGate gate) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.evalReversibleGate gate)

theorem QuantumBlockEncoding.compileReversibleGate_eval
  {qubits : ℕ}
  (gate :
    QuantumBlockEncoding.ReversibleGate
      qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.compileReversibleGate
        gate) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.evalReversibleGate
        gate)

Definition6.3.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile reversible program”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.5●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.compileReversibleProgram {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleProgram qubits →
    QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.compileReversibleProgram
  {qubits : ℕ} :
  QuantumBlockEncoding.ReversibleProgram
      qubits →
    QuantumBlockEncoding.PrimitiveProgram
      qubits

Theorem6.3.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile reversible program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:58. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.6●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.compileReversibleProgram_eval {qubits : ℕ}
  (program : QuantumBlockEncoding.ReversibleProgram qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.compileReversibleProgram program) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.evalReversibleProgram program)

theorem QuantumBlockEncoding.compileReversibleProgram_eval
  {qubits : ℕ}
  (program :
    QuantumBlockEncoding.ReversibleProgram
      qubits) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.compileReversibleProgram
        program) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.evalReversibleProgram
        program)

Definition6.3.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean c 3 x reversible program”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:75. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.7●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.cleanC3XReversibleProgram {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.ReversibleProgram qubits

def QuantumBlockEncoding.cleanC3XReversibleProgram
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.ReversibleProgram
    qubits

Definition6.3.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean c 3 x basis equiv”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:88. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.8●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.cleanC3XBasisEquiv {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis qubits ≃
    QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.cleanC3XBasisEquiv
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.PrimitiveBasis
      qubits ≃
    QuantumBlockEncoding.PrimitiveBasis
      qubits

Definition6.3.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “c 3 x basis action”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:102. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.9●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.c3xBasisAction {qubits : ℕ}
  (control0 control1 control2 target : Fin qubits)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits) :
  QuantumBlockEncoding.PrimitiveBasis qubits

def QuantumBlockEncoding.c3xBasisAction
  {qubits : ℕ}
  (control0 control1 control2 target :
    Fin qubits)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits) :
  QuantumBlockEncoding.PrimitiveBasis
    qubits

Theorem6.3.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean c 3 x basis action”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:109. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.10●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.cleanC3XBasisAction {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) (c2_ne_target : control2 ≠ target)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits)
  (workClean : state work = 0) :
  (QuantumBlockEncoding.cleanC3XBasisEquiv control0 control1 control2
        target work c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)
      state =
    QuantumBlockEncoding.c3xBasisAction control0 control1 control2
      target state

theorem QuantumBlockEncoding.cleanC3XBasisAction
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target)
  (c2_ne_target : control2 ≠ target)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits)
  (workClean : state work = 0) :
  (QuantumBlockEncoding.cleanC3XBasisEquiv
        control0 control1 control2 target
        work c0_ne_c1 c0_ne_work
        c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)
      state =
    QuantumBlockEncoding.c3xBasisAction
      control0 control1 control2 target
      state

Theorem6.3.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean c 3 x workspace clean”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:143. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.11●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.cleanC3XWorkspaceClean {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target) (c2_ne_target : control2 ≠ target)
  (state : QuantumBlockEncoding.PrimitiveBasis qubits)
  (workClean : state work = 0) :
  (QuantumBlockEncoding.cleanC3XBasisEquiv control0 control1 control2
        target work c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)
      state work =
    0

theorem QuantumBlockEncoding.cleanC3XWorkspaceClean
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c0_ne_target : control0 ≠ target)
  (c1_ne_target : control1 ≠ target)
  (c2_ne_target : control2 ≠ target)
  (state :
    QuantumBlockEncoding.PrimitiveBasis
      qubits)
  (workClean : state work = 0) :
  (QuantumBlockEncoding.cleanC3XBasisEquiv
        control0 control1 control2 target
        work c0_ne_c1 c0_ne_work
        c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)
      state work =
    0

Definition6.3.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean c 3 x primitive program”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:165. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.12●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.cleanC3XPrimitiveProgram {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram qubits

def QuantumBlockEncoding.cleanC3XPrimitiveProgram
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.PrimitiveProgram
    qubits

Theorem6.3.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean c 3 x primitive program eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:178. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.13●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.cleanC3XPrimitiveProgram_eval {qubits : ℕ}
  (control0 control1 control2 target work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1) (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work) (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target) (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.cleanC3XPrimitiveProgram control0 control1
        control2 target work c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2
        work_ne_target c2_ne_target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.cleanC3XBasisEquiv control0 control1
        control2 target work c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)

theorem QuantumBlockEncoding.cleanC3XPrimitiveProgram_eval
  {qubits : ℕ}
  (control0 control1 control2 target
    work : Fin qubits)
  (c0_ne_c1 : control0 ≠ control1)
  (c0_ne_work : control0 ≠ work)
  (c1_ne_work : control1 ≠ work)
  (work_ne_c2 : work ≠ control2)
  (work_ne_target : work ≠ target)
  (c2_ne_target : control2 ≠ target) :
  QuantumBlockEncoding.evalPrimitiveProgram
      (QuantumBlockEncoding.cleanC3XPrimitiveProgram
        control0 control1 control2 target
        work c0_ne_c1 c0_ne_work
        c1_ne_work work_ne_c2
        work_ne_target c2_ne_target) =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (QuantumBlockEncoding.cleanC3XBasisEquiv
        control0 control1 control2 target
        work c0_ne_c1 c0_ne_work
        c1_ne_work work_ne_c2
        work_ne_target c2_ne_target)

Definition6.3.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “little endian 3 value”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:198. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.14●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.littleEndian3Value
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (wire0 wire1 wire2 : Fin 7) : ℕ

def QuantumBlockEncoding.littleEndian3Value
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (wire0 wire1 wire2 : Fin 7) : ℕ

Definition6.3.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “modular add 3 reversible program”. Wire order is 'a0,a1,a2,b0,b1,b2,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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Wire order is 'a0,a1,a2,b0,b1,b2,work'.

Declaration kind. def.

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

Lean code for Definition6.3.15●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.modularAdd3ReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 7

def QuantumBlockEncoding.modularAdd3ReversibleProgram :
  QuantumBlockEncoding.ReversibleProgram 7

Wire order is `a0,a1,a2,b0,b1,b2,work`.

Definition6.3.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “modular add 3 basis equiv”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:214. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.16●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.modularAdd3BasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 7 ≃
    QuantumBlockEncoding.PrimitiveBasis 7

def QuantumBlockEncoding.modularAdd3BasisEquiv :
  QuantumBlockEncoding.PrimitiveBasis 7 ≃
    QuantumBlockEncoding.PrimitiveBasis 7

Theorem6.3.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular add 3 clean action”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:217. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.17●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.modularAdd3_cleanAction
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  have output := QuantumBlockEncoding.modularAdd3BasisEquiv state;
  QuantumBlockEncoding.littleEndian3Value output 0 1 2 =
      (QuantumBlockEncoding.littleEndian3Value state 0 1 2 +
          QuantumBlockEncoding.littleEndian3Value state 3 4 5) %
        8 ∧
    output 3 = state 3 ∧
      output 4 = state 4 ∧ output 5 = state 5 ∧ output 6 = 0

theorem QuantumBlockEncoding.modularAdd3_cleanAction
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  have output :=
    QuantumBlockEncoding.modularAdd3BasisEquiv
      state;
  QuantumBlockEncoding.littleEndian3Value
        output 0 1 2 =
      (QuantumBlockEncoding.littleEndian3Value
            state 0 1 2 +
          QuantumBlockEncoding.littleEndian3Value
            state 3 4 5) %
        8 ∧
    output 3 = state 3 ∧
      output 4 = state 4 ∧
        output 5 = state 5 ∧ output 6 = 0

Definition6.3.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “modular add 3 primitive program”.

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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:227. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.3.18●1 definition

defdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

def QuantumBlockEncoding.modularAdd3PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 7

def QuantumBlockEncoding.modularAdd3PrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 7

Theorem6.3.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular add 3 primitive eval”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:230. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.19●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.modularAdd3Primitive_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.modularAdd3PrimitiveProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.modularAdd3BasisEquiv

theorem QuantumBlockEncoding.modularAdd3Primitive_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.modularAdd3PrimitiveProgram =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      QuantumBlockEncoding.modularAdd3BasisEquiv

Theorem6.3.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular add 3 primitive workspace clean”; 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:235. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.20●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.modularAdd3Primitive_workspaceClean
  (state : QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.modularAdd3BasisEquiv state 6 = 0

theorem QuantumBlockEncoding.modularAdd3Primitive_workspaceClean
  (state :
    QuantumBlockEncoding.PrimitiveBasis 7)
  (workClean : state 6 = 0) :
  QuantumBlockEncoding.modularAdd3BasisEquiv
      state 6 =
    0

Theorem6.3.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular add 3 primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. The resource is definitionally computed from the emitted primitive 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The resource is definitionally computed from the emitted primitive list.

Declaration kind. theorem.

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

Lean code for Theorem6.3.21●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.modularAdd3Primitive_resource_faithful :
  QuantumBlockEncoding.modularAdd3PrimitiveProgram.resource =
    QuantumBlockEncoding.modularAdd3PrimitiveProgram.circuit.resource

theorem QuantumBlockEncoding.modularAdd3Primitive_resource_faithful :
  QuantumBlockEncoding.modularAdd3PrimitiveProgram.resource =
    QuantumBlockEncoding.modularAdd3PrimitiveProgram.circuit.resource

The resource is definitionally computed from the emitted primitive list.

Theorem6.3.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “modular add 3 primitive oracle calls eq 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. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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/ModularAdder3.lean:245. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.3.22●1 theorem

theoremdefined in QuantumBlockEncoding/ModularAdder3.lean

complete

theorem QuantumBlockEncoding.modularAdd3Primitive_oracleCalls_eq_zero :
  QuantumBlockEncoding.modularAdd3PrimitiveProgram.resource.oracleCalls =
    0

theorem QuantumBlockEncoding.modularAdd3Primitive_oracleCalls_eq_zero :
  QuantumBlockEncoding.modularAdd3PrimitiveProgram.resource.oracleCalls =
    0