QuantumBlockEncoding/ModularAdder3.lean

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

def primitiveXProgram {qubits : Nat} (target : Fin qubits) :
    PrimitiveProgram qubits where
  circuit := [.x target]
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive x program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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

noncomputable def compileReversibleGate {qubits : Nat} :
    ReversibleGate qubits → PrimitiveProgram qubits
  | .x target => primitiveXProgram target
  | .cx control target distinct =>
      primitiveCxProgram control target distinct
  | .ccx control0 control1 target c0_ne_c1 c0_ne_target c1_ne_target =>
      primitiveCCXProgram control0 control1 target c0_ne_c1
        c0_ne_target c1_ne_target

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile reversible gate eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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

noncomputable def compileReversibleProgram {qubits : Nat} :
    ReversibleProgram qubits → PrimitiveProgram qubits
  | [] => PrimitiveProgram.identity qubits
  | gate :: rest =>
      (compileReversibleGate gate).seq (compileReversibleProgram rest)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile reversible program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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

def cleanC3XReversibleProgram {qubits : Nat}
    (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) : ReversibleProgram qubits :=
  [ .ccx control0 control1 work c0_ne_c1 c0_ne_work c1_ne_work
  , .ccx work control2 target work_ne_c2 work_ne_target c2_ne_target
  , .ccx control0 control1 work c0_ne_c1 c0_ne_work c1_ne_work

commit-pinned source · Verso Blueprint panel

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

def cleanC3XBasisEquiv {qubits : Nat}
    (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) :
    PrimitiveBasis qubits ≃ PrimitiveBasis qubits :=
  evalReversibleProgram
    (cleanC3XReversibleProgram control0 control1 control2 target work

commit-pinned source · Verso Blueprint panel

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

def c3xBasisAction {qubits : Nat}
    (control0 control1 control2 target : Fin qubits)
    (state : PrimitiveBasis qubits) : PrimitiveBasis qubits :=
  if state control0 = 1 ∧ state control1 = 1 ∧ state control2 = 1 then
    xBasisAction target state
  else state

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean c 3 x basis action”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cleanC3XBasisAction {qubits : Nat}
    (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 : PrimitiveBasis qubits) (workClean : state work = 0) :

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean c 3 x workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cleanC3XWorkspaceClean {qubits : Nat}
    (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 : PrimitiveBasis qubits) (workClean : state work = 0) :

commit-pinned source · Verso Blueprint panel

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

noncomputable def cleanC3XPrimitiveProgram {qubits : Nat}
    (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) : PrimitiveProgram qubits :=
  compileReversibleProgram
    (cleanC3XReversibleProgram control0 control1 control2 target work
      c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2 work_ne_target

commit-pinned source · Verso Blueprint panel

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.

theorem cleanC3XPrimitiveProgram_eval {qubits : Nat}
    (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) :
    evalPrimitiveProgram
        (cleanC3XPrimitiveProgram control0 control1 control2 target work
          c0_ne_c1 c0_ne_work c1_ne_work work_ne_c2 work_ne_target

commit-pinned source · Verso Blueprint panel

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

def littleEndian3Value (state : PrimitiveBasis 7)
    (wire0 wire1 wire2 : Fin 7) : Nat :=
  (state wire0).val + 2 * (state wire1).val + 4 * (state wire2).val

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

commit-pinned source · Verso Blueprint panel

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

def modularAdd3ReversibleProgram : ReversibleProgram 7 :=
  [ .ccx 3 0 6 (by decide) (by decide) (by decide)
  , .ccx 6 1 2 (by decide) (by decide) (by decide)
  , .ccx 3 0 6 (by decide) (by decide) (by decide)
  , .ccx 3 0 1 (by decide) (by decide) (by decide)
  , .cx 3 0 (by decide)
  , .ccx 4 1 2 (by decide) (by decide) (by decide)
  , .cx 4 1 (by decide)
  , .cx 5 2 (by decide)
  ]

commit-pinned source · Verso Blueprint panel

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

def modularAdd3BasisEquiv : PrimitiveBasis 7 ≃ PrimitiveBasis 7 :=
  evalReversibleProgram modularAdd3ReversibleProgram

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “modular add 3 clean action”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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

noncomputable def modularAdd3PrimitiveProgram : PrimitiveProgram 7 :=
  compileReversibleProgram modularAdd3ReversibleProgram

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “modular add 3 primitive eval”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “modular add 3 primitive workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope.

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

/-- The resource is definitionally computed from the emitted primitive list. -/

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

theorem modularAdd3Primitive_oracleCalls_eq_zero :
    modularAdd3PrimitiveProgram.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

commit-pinned source · Verso Blueprint panel