QuantumBlockEncoding/PrimitiveWireRename.lean

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

def basisEquiv {m n : Nat} (e : Fin m ≃ Fin n) : PrimitiveBasis m ≃ PrimitiveBasis n where
  toFun b := fun w => b (e.symm w)
  invFun b := fun w => b (e w)
  left_inv b := by funext w; simp

commit-pinned source · Verso Blueprint panel

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

def gate {m n : Nat} (e : Fin m ≃ Fin n) : PrimitiveGate m → PrimitiveGate n
  | .x t => .x (e t)
  | .ry t a => .ry (e t) a
  | .rz t a => .rz (e t) a
  | .cx c t h => .cx (e c) (e t) (fun he => h (e.injective he))

commit-pinned source · Verso Blueprint panel

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

def circuit {m n : Nat} (e : Fin m ≃ Fin n) (c : PrimitiveCircuit m) : PrimitiveCircuit n :=
  c.map (gate e)

commit-pinned source · Verso Blueprint panel

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

noncomputable def matrix {m n : Nat} (e : Fin m ≃ Fin n)
    (M : _root_.Matrix (PrimitiveBasis m) (PrimitiveBasis m) ℂ) :
    _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (basisEquiv e) M

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem matrix_apply {m n : Nat} (e : Fin m ≃ Fin n)
    (M : _root_.Matrix (PrimitiveBasis m) (PrimitiveBasis m) ℂ)
    (a b : PrimitiveBasis n) :
    matrix e M a b = M (fun w => a (e w)) (fun w => b (e w)) := rfl

commit-pinned source · Verso Blueprint panel

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

theorem matrix_mul {m n : Nat} (e : Fin m ≃ Fin n)
    (M N : _root_.Matrix (PrimitiveBasis m) (PrimitiveBasis m) ℂ) :
    matrix e (M * N) = matrix e M * matrix e N :=
  map_mul (_root_.Matrix.reindexAlgEquiv ℂ ℂ (basisEquiv e)) M N

commit-pinned source · Verso Blueprint panel

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

theorem oneQubit {m n : Nat} (e : Fin m ≃ Fin n) (t : Fin m)
    (M : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    liftPrimitiveOneQubit (e t) M = matrix e (liftPrimitiveOneQubit t M) := by

commit-pinned source · Verso Blueprint panel

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

theorem eval_gate {m n : Nat} (e : Fin m ≃ Fin n) (g : PrimitiveGate m) :
    evalPrimitiveGate (gate e g) = matrix e (evalPrimitiveGate g) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “eval circuit”; the hypotheses and conclusion in the code panel fix its exact scope. One actual renamed primitive list, with both boundary index maps exposed.

theorem eval_circuit {m n : Nat} (e : Fin m ≃ Fin n) (c : PrimitiveCircuit m) :
    evalPrimitiveCircuit (circuit e c) = matrix e (evalPrimitiveCircuit c) := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem gateCount {m n : Nat} (e : Fin m ≃ Fin n) (c : PrimitiveCircuit m) :
    (circuit e c).gateCount = c.gateCount := by simp [circuit]

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem ryCount {m n : Nat} (e : Fin m ≃ Fin n) (c : PrimitiveCircuit m) :
    (circuit e c).ryCount = c.ryCount := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem cxCount {m n : Nat} (e : Fin m ≃ Fin n) (c : PrimitiveCircuit m) :
    (circuit e c).cxCount = c.cxCount := by

commit-pinned source · Verso Blueprint panel