QuantumBlockEncoding/PrimitiveMacros.lean

This definition gives the library's named construction or computation for “hadamard matrix”.

noncomputable def hadamardMatrix : _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  Complex.I •
    (standardRyMatrix (Real.pi / 2) * standardRzMatrix Real.pi)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “phase matrix”.

noncomputable def phaseMatrix (theta : Real) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  Complex.exp (((theta / 2 : Real) : ℂ) * Complex.I) •
    standardRzMatrix theta

commit-pinned source · Verso Blueprint panel

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

theorem hadamardMatrix_apply (row column : Fin 2) :
    hadamardMatrix row column =
      let scale : ℂ := (Real.sqrt 2 / 2 : Real)
      match row.val, column.val with
      | 0, 0 | 0, 1 | 1, 0 => scale
      | _, _ => -scale := by

commit-pinned source · Verso Blueprint panel

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

theorem phaseMatrix_apply (theta : Real) (row column : Fin 2) :
    phaseMatrix theta row column =
      if row = column then
        if row = 0 then 1 else Complex.exp ((theta : ℂ) * Complex.I)
      else 0 := by

commit-pinned source · Verso Blueprint panel

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

def primitiveHProgram {qubits : Nat} (target : Fin qubits) :
    PrimitiveProgram qubits where
  globalPhase := .piRational (1 / 2)
  circuit :=
    [.rz target (.piRational 1), .ry target (.piRational (1 / 2))]

commit-pinned source · Verso Blueprint panel

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

def primitiveTProgram {qubits : Nat} (target : Fin qubits) :
    PrimitiveProgram qubits where
  globalPhase := .piRational (1 / 8)
  circuit := [.rz target (.piRational (1 / 4))]

commit-pinned source · Verso Blueprint panel

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

def primitiveTdgProgram {qubits : Nat} (target : Fin qubits) :
    PrimitiveProgram qubits where
  globalPhase := .piRational (-1 / 8)
  circuit := [.rz target (.piRational (-1 / 4))]

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval global phase pi div two”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem evalGlobalPhase_pi_div_two :
    evalGlobalPhase (.piRational (1 / 2)) = Complex.I := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “lift primitive one qubit mul”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem liftPrimitiveOneQubit_mul {qubits : Nat} (target : Fin qubits)
    (left right : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    liftPrimitiveOneQubit target (left * right) =
      liftPrimitiveOneQubit target left * liftPrimitiveOneQubit target right := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “smul lift primitive one qubit”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem smul_liftPrimitiveOneQubit {qubits : Nat} (target : Fin qubits)
    (scalar : ℂ) (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    scalar • liftPrimitiveOneQubit target gate =
      liftPrimitiveOneQubit target (scalar • gate) := by

commit-pinned source · Verso Blueprint panel

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

theorem primitiveHProgram_eval {qubits : Nat} (target : Fin qubits) :
    evalPrimitiveProgram (primitiveHProgram target) =
      liftPrimitiveOneQubit target hadamardMatrix := by

commit-pinned source · Verso Blueprint panel

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

theorem primitiveTProgram_eval {qubits : Nat} (target : Fin qubits) :
    evalPrimitiveProgram (primitiveTProgram target) =
      liftPrimitiveOneQubit target (phaseMatrix (Real.pi / 4)) := by

commit-pinned source · Verso Blueprint panel

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

theorem primitiveTdgProgram_eval {qubits : Nat} (target : Fin qubits) :
    evalPrimitiveProgram (primitiveTdgProgram target) =
      liftPrimitiveOneQubit target (phaseMatrix (-Real.pi / 4)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “phase permutation matrix”.

noncomputable def phasePermutationMatrix {index : Type*}
    [Fintype index] [DecidableEq index]
    (phase : index → ℂ) (permutation : index ≃ index) :
    _root_.Matrix index index ℂ := fun row column =>
  if row = permutation column then phase column else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “phase permutation matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem phasePermutationMatrix_mul {index : Type*}
    [Fintype index] [DecidableEq index]
    (leftPhase rightPhase : index → ℂ)
    (leftPerm rightPerm : index ≃ index) :
    phasePermutationMatrix rightPhase rightPerm *
        phasePermutationMatrix leftPhase leftPerm =
      phasePermutationMatrix
        (fun state => leftPhase state * rightPhase (leftPerm state))
        (leftPerm.trans rightPerm) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval primitive cx eq phase permutation matrix”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem evalPrimitiveCx_eq_phasePermutationMatrix {qubits : Nat}
    (control target : Fin qubits) (distinct : control ≠ target) :
    evalPrimitiveGate (.cx control target distinct) =
      phasePermutationMatrix (fun _ => 1)
        (cxBasisEquiv control target distinct) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “lift phase matrix eq phase permutation matrix”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem liftPhaseMatrix_eq_phasePermutationMatrix {qubits : Nat}
    (target : Fin qubits) (theta : Real) :
    liftPrimitiveOneQubit target (phaseMatrix theta) =
      phasePermutationMatrix
        (fun state => if state target = 0 then 1
          else Complex.exp ((theta : ℂ) * Complex.I))
        (Equiv.refl _) := by

commit-pinned source · Verso Blueprint panel

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

def primitiveCxProgram {qubits : Nat} (control target : Fin qubits)
    (distinct : control ≠ target) : PrimitiveProgram qubits where
  circuit := [.cx control target distinct]
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

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

theorem primitiveCxProgram_eval {qubits : Nat}
    (control target : Fin qubits) (distinct : control ≠ target) :
    evalPrimitiveProgram (primitiveCxProgram control target distinct) =
      phasePermutationMatrix (fun _ => 1)
        (cxBasisEquiv control target distinct) := by

commit-pinned source · Verso Blueprint panel

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

theorem primitiveTProgram_eval_monomial {qubits : Nat}
    (target : Fin qubits) :
    evalPrimitiveProgram (primitiveTProgram target) =
      phasePermutationMatrix
        (fun state => if state target = 0 then 1
          else Complex.exp (((Real.pi / 4 : Real) : ℂ) * Complex.I))
        (Equiv.refl _) := by

commit-pinned source · Verso Blueprint panel

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

theorem primitiveTdgProgram_eval_monomial {qubits : Nat}
    (target : Fin qubits) :
    evalPrimitiveProgram (primitiveTdgProgram target) =
      phasePermutationMatrix
        (fun state => if state target = 0 then 1
          else Complex.exp (((-Real.pi / 4 : Real) : ℂ) * Complex.I))
        (Equiv.refl _) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “monomial program”. A proposition-valued field is a requirement until a constructor supplies it.

structure MonomialProgram (qubits : Nat) where
  program : PrimitiveProgram qubits
  phase : PrimitiveBasis qubits → ℂ
  permutation : PrimitiveBasis qubits ≃ PrimitiveBasis qubits
  exact : evalPrimitiveProgram program =
    phasePermutationMatrix phase permutation

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “seq”.

def seq {qubits : Nat} (left right : MonomialProgram qubits) :
    MonomialProgram qubits where
  program := left.program.seq right.program
  phase := fun state => left.phase state * right.phase (left.permutation state)
  permutation := left.permutation.trans right.permutation
  exact := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cx”.

def cx {qubits : Nat} (control target : Fin qubits)
    (distinct : control ≠ target) : MonomialProgram qubits where
  program := primitiveCxProgram control target distinct
  phase := fun _ => 1
  permutation := cxBasisEquiv control target distinct
  exact := primitiveCxProgram_eval control target distinct

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “t”.

noncomputable def t {qubits : Nat} (target : Fin qubits) : MonomialProgram qubits where
  program := primitiveTProgram target
  phase := fun state => if state target = 0 then 1
    else Complex.exp (((Real.pi / 4 : Real) : ℂ) * Complex.I)
  permutation := Equiv.refl _
  exact := primitiveTProgram_eval_monomial target

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tdg”.

noncomputable def tdg {qubits : Nat} (target : Fin qubits) : MonomialProgram qubits where
  program := primitiveTdgProgram target
  phase := fun state => if state target = 0 then 1
    else Complex.exp (((-Real.pi / 4 : Real) : ℂ) * Complex.I)
  permutation := Equiv.refl _
  exact := primitiveTdgProgram_eval_monomial target

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive ccx middle”. The phase-only middle of the standard exact Toffoli decomposition.

noncomputable def primitiveCCXMiddle {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) : MonomialProgram qubits :=
  let cxBT := MonomialProgram.cx b target b_ne_target
  let cxAT := MonomialProgram.cx a target a_ne_target
  let cxAB := MonomialProgram.cx a b a_ne_b
  cxBT |>.seq (MonomialProgram.tdg target)
    |>.seq cxAT
    |>.seq (MonomialProgram.t target)
    |>.seq cxBT

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “primitive ccx program”. The exact primitive program uses the requested H/T/Tdg/CX chronology.

noncomputable def primitiveCCXProgram {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) : PrimitiveProgram qubits :=
  (primitiveHProgram target).seq
    ((primitiveCCXMiddle a b target a_ne_b a_ne_target b_ne_target).program.seq
      (primitiveHProgram target))

set_option maxHeartbeats 2000000 in

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive ccx middle permutation eq refl”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveCCXMiddle_permutation_eq_refl {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) :
    (primitiveCCXMiddle a b target a_ne_b a_ne_target b_ne_target).permutation =
      Equiv.refl _ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive ccx middle phase eq ccz”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem primitiveCCXMiddle_phase_eq_ccz {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) (state : PrimitiveBasis qubits) :
    (primitiveCCXMiddle a b target a_ne_b a_ne_target b_ne_target).phase state =
      if state a = 1 ∧ state b = 1 ∧ state target = 1 then -1 else 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “ccz matrix”.

noncomputable def cczMatrix {qubits : Nat}
    (a b target : Fin qubits) :
    _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ :=
  phasePermutationMatrix
    (fun state => if state a = 1 ∧ state b = 1 ∧ state target = 1
      then -1 else 1)
    (Equiv.refl _)

commit-pinned source · Verso Blueprint panel

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

theorem primitiveCCXMiddle_eval {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) :
    evalPrimitiveProgram
        (primitiveCCXMiddle a b target a_ne_b a_ne_target b_ne_target).program =
      cczMatrix a b target := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “z matrix”.

def zMatrix : _root_.Matrix (Fin 2) (Fin 2) ℂ := fun row column =>
  if row = column then if row = 0 then 1 else -1 else 0

commit-pinned source · Verso Blueprint panel

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

theorem hadamard_mul_hadamard : hadamardMatrix * hadamardMatrix = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard mul z mul hadamard”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamard_mul_z_mul_hadamard :
    hadamardMatrix * zMatrix * hadamardMatrix = xMatrix := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “lift primitive one qubit eq block diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem liftPrimitiveOneQubit_eq_blockDiagonal {qubits : Nat}
    (target : Fin qubits) (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    liftPrimitiveOneQubit target gate =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ (splitPrimitiveWire target).symm
        (_root_.Matrix.blockDiagonal
          (fun _ : OtherPrimitiveWires target → Fin 2 => gate)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “ccz target block”.

noncomputable def cczTargetBlock {qubits : Nat}
    (a b target : Fin qubits) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target)
    (context : OtherPrimitiveWires target → Fin 2) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  if context ⟨a, a_ne_target⟩ = 1 ∧ context ⟨b, b_ne_target⟩ = 1
  then zMatrix else 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “ccz matrix eq block diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem cczMatrix_eq_blockDiagonal {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_target : a ≠ target) (b_ne_target : b ≠ target) :
    cczMatrix a b target =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ (splitPrimitiveWire target).symm
        (_root_.Matrix.blockDiagonal
          (cczTargetBlock a b target a_ne_target b_ne_target)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “ccx target block”.

noncomputable def ccxTargetBlock {qubits : Nat}
    (a b target : Fin qubits) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target)
    (context : OtherPrimitiveWires target → Fin 2) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  if context ⟨a, a_ne_target⟩ = 1 ∧ context ⟨b, b_ne_target⟩ = 1
  then xMatrix else 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “equiv permutation matrix ccx eq block diagonal”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem equivPermutationMatrix_ccx_eq_blockDiagonal {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_target : a ≠ target) (b_ne_target : b ≠ target) :
    Robin.ComplexLCU.equivPermutationMatrix
        (ccxBasisEquiv a b target a_ne_target b_ne_target) =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ (splitPrimitiveWire target).symm
        (_root_.Matrix.blockDiagonal
          (ccxTargetBlock a b target a_ne_target b_ne_target)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “hadamard conjugates ccz”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem hadamard_conjugates_ccz {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_target : a ≠ target) (b_ne_target : b ≠ target) :
    liftPrimitiveOneQubit target hadamardMatrix *
        cczMatrix a b target *
        liftPrimitiveOneQubit target hadamardMatrix =
      Robin.ComplexLCU.equivPermutationMatrix
        (ccxBasisEquiv a b target a_ne_target b_ne_target) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “primitive ccx program eval”; the hypotheses and conclusion in the code panel fix its exact scope. The requested H/T/Tdg/CX decomposition is exactly Toffoli, including its global phase.

theorem primitiveCCXProgram_eval {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) :
    evalPrimitiveProgram
        (primitiveCCXProgram a b target a_ne_b a_ne_target b_ne_target) =
      Robin.ComplexLCU.equivPermutationMatrix
        (ccxBasisEquiv a b target a_ne_target b_ne_target) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def primitiveCCXProgramRefinement {qubits : Nat}
    (a b target : Fin qubits)
    (a_ne_b : a ≠ b) (a_ne_target : a ≠ target)
    (b_ne_target : b ≠ target) : PrimitiveProgramRefinement qubits where
  program := primitiveCCXProgram a b target a_ne_b a_ne_target b_ne_target
  target := Robin.ComplexLCU.equivPermutationMatrix
    (ccxBasisEquiv a b target a_ne_target b_ne_target)
  exact := primitiveCCXProgram_eval a b target a_ne_b a_ne_target b_ne_target

commit-pinned source · Verso Blueprint panel