QuantumBlockEncoding/PrimitiveSemantics.lean

This definition gives the library's named construction or computation for “standard ry matrix”. Standard 'RY(theta)' in the convention used by Qiskit and OpenQASM 3.

noncomputable def standardRyMatrix (theta : Real) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  realRotation (theta / 2)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem standardRyMatrix_zero : standardRyMatrix 0 = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “standard ry matrix add”; the hypotheses and conclusion in the code panel fix its exact scope. Standard rotations compose by adding their physical angles.

theorem standardRyMatrix_add (left right : Real) :
    standardRyMatrix (left + right) =
      standardRyMatrix right * standardRyMatrix left := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “star complex cos of real”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem star_complex_cos_ofReal (theta : Real) :
    star (Complex.cos (theta : ℂ)) = Complex.cos (theta : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “conj complex cos of real”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem conj_complex_cos_ofReal (theta : Real) :
    (starRingEnd ℂ) (Complex.cos (theta : ℂ)) =
      Complex.cos (theta : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “star complex sin of real”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem star_complex_sin_ofReal (theta : Real) :
    star (Complex.sin (theta : ℂ)) = Complex.sin (theta : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “conj complex sin of real”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem conj_complex_sin_ofReal (theta : Real) :
    (starRingEnd ℂ) (Complex.sin (theta : ℂ)) =
      Complex.sin (theta : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “complex of real div two”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem complex_ofReal_div_two (theta : Real) :
    (theta : ℂ) / 2 = ((theta / 2 : Real) : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “conj complex cos of real div two”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem conj_complex_cos_ofReal_div_two (theta : Real) :
    (starRingEnd ℂ) (Complex.cos ((theta : ℂ) / 2)) =
      Complex.cos ((theta : ℂ) / 2) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “conj complex sin of real div two”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem conj_complex_sin_ofReal_div_two (theta : Real) :
    (starRingEnd ℂ) (Complex.sin ((theta : ℂ) / 2)) =
      Complex.sin ((theta : ℂ) / 2) := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem standardRyMatrix_neg (theta : Real) :
    standardRyMatrix (-theta) = star (standardRyMatrix theta) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “x matrix”. Pauli X in the same two-dimensional basis as 'standardRyMatrix'.

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

commit-pinned source · Verso Blueprint panel

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

theorem xMatrix_conjugates_standardRy (theta : Real) :
    xMatrix * standardRyMatrix theta * xMatrix = standardRyMatrix (-theta) := by

commit-pinned source · Verso Blueprint panel

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

theorem standardRyMatrix_unitary (theta : Real) :
    standardRyMatrix theta ∈ _root_.Matrix.unitaryGroup (Fin 2) ℂ :=
  realRotation_unitary _

/-- The exact half-angle correction from standard `RY` to the logical loader. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “standard ry matrix two arccos eq amplitude rotation”; the hypotheses and conclusion in the code panel fix its exact scope. The exact half-angle correction from standard 'RY' to the logical loader.

theorem standardRyMatrix_two_arccos_eq_amplitudeRotation
    (coefficient : Real) (_lower : -1 ≤ coefficient)
    (_upper : coefficient ≤ 1) :
    standardRyMatrix (2 * Real.arccos coefficient) =
      amplitudeRotation coefficient := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “standard ry matrix pi div two eq warm robin uniform bit prepare”; the hypotheses and conclusion in the code panel fix its exact scope. The symmetry PREPARE is exactly a standard 'RY(pi/2)', not an opaque H.

theorem standardRyMatrix_pi_div_two_eq_warmRobinUniformBitPrepare :
    standardRyMatrix (Real.pi / 2) =
      QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “primitive basis”. Computational-basis bit strings with one named coordinate per qubit.

abbrev PrimitiveBasis (qubits : Nat) := Fin qubits → Fin 2

commit-pinned source · Verso Blueprint panel

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

def flipBit (bit : Fin 2) : Fin 2 := if bit = 0 then 1 else 0

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem flipBit_flipBit (bit : Fin 2) : flipBit (flipBit bit) = bit := by

commit-pinned source · Verso Blueprint panel

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

def xBasisAction {qubits : Nat} (target : Fin qubits)
    (state : PrimitiveBasis qubits) : PrimitiveBasis qubits :=
  Function.update state target (flipBit (state target))

commit-pinned source · Verso Blueprint panel

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

theorem xBasisAction_involutive {qubits : Nat} (target : Fin qubits) :
    Function.Involutive (xBasisAction target) := by

commit-pinned source · Verso Blueprint panel

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

def xBasisEquiv {qubits : Nat} (target : Fin qubits) :
    PrimitiveBasis qubits ≃ PrimitiveBasis qubits where
  toFun := xBasisAction target
  invFun := xBasisAction target
  left_inv := xBasisAction_involutive target
  right_inv := xBasisAction_involutive target

commit-pinned source · Verso Blueprint panel

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

def cxBasisAction {qubits : Nat} (control target : Fin qubits)
    (state : PrimitiveBasis qubits) : PrimitiveBasis qubits :=
  if state control = 0 then state else xBasisAction target state

commit-pinned source · Verso Blueprint panel

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

theorem cxBasisAction_involutive {qubits : Nat}
    (control target : Fin qubits) (distinct : control ≠ target) :
    Function.Involutive (cxBasisAction control target) := by

commit-pinned source · Verso Blueprint panel

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

def cxBasisEquiv {qubits : Nat} (control target : Fin qubits)
    (distinct : control ≠ target) :
    PrimitiveBasis qubits ≃ PrimitiveBasis qubits where
  toFun := cxBasisAction control target
  invFun := cxBasisAction control target
  left_inv := cxBasisAction_involutive control target distinct
  right_inv := cxBasisAction_involutive control target distinct

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “other primitive wires”.

abbrev OtherPrimitiveWires {qubits : Nat} (target : Fin qubits) :=
  {wire : Fin qubits // wire ≠ target}

commit-pinned source · Verso Blueprint panel

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

def splitPrimitiveWire {qubits : Nat} (target : Fin qubits) :
    PrimitiveBasis qubits ≃
      Fin 2 × (OtherPrimitiveWires target → Fin 2) where
  toFun state := (state target, fun wire => state wire.1)
  invFun pair wire :=
    if same : wire = target then pair.1 else pair.2 ⟨wire, same⟩
  left_inv state := by

commit-pinned source · Verso Blueprint panel

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

theorem splitPrimitiveWire_other_apply {qubits : Nat}
    (target : Fin qubits) (state : PrimitiveBasis qubits)
    (wire : OtherPrimitiveWires target) :
    (splitPrimitiveWire target state).2 wire = state wire.1 := rfl

/-- Lift a one-qubit matrix to a named wire, leaving every other wire fixed. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “lift primitive one qubit”. Lift a one-qubit matrix to a named wire, leaving every other wire fixed.

noncomputable def liftPrimitiveOneQubit {qubits : Nat} (target : Fin qubits)
    (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (splitPrimitiveWire target).symm
    (gate ⊗ₖ (1 : _root_.Matrix
      (OtherPrimitiveWires target → Fin 2)
      (OtherPrimitiveWires target → Fin 2) ℂ))

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem liftPrimitiveOneQubit_apply {qubits : Nat}
    (target : Fin qubits) (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ)
    (row column : PrimitiveBasis qubits) :
    liftPrimitiveOneQubit target gate row column =
      if (splitPrimitiveWire target row).2 =
          (splitPrimitiveWire target column).2 then
        gate (row target) (column target)
      else 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem liftPrimitiveOneQubit_unitary {qubits : Nat} (target : Fin qubits)
    (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ)
    (unitary : gate ∈ _root_.Matrix.unitaryGroup (Fin 2) ℂ) :
    liftPrimitiveOneQubit target gate ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis qubits) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “standard rz matrix”. Standard exact 'RZ(theta)' matrix, including its phase convention.

noncomputable def standardRzMatrix (theta : Real) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ := fun row column =>
  if row = column then
    if row = 0 then
      (Real.cos (theta / 2) : ℂ) - (Real.sin (theta / 2) : ℂ) * Complex.I
    else
      (Real.cos (theta / 2) : ℂ) + (Real.sin (theta / 2) : ℂ) * Complex.I
  else 0

commit-pinned source · Verso Blueprint panel

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

theorem standardRzMatrix_unitary (theta : Real) :
    standardRzMatrix theta ∈ _root_.Matrix.unitaryGroup (Fin 2) ℂ := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem standardRzMatrix_neg (theta : Real) :
    standardRzMatrix (-theta) = star (standardRzMatrix theta) := by

commit-pinned source · Verso Blueprint panel

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

theorem star_equivPermutationMatrix
    {index : Type*} [Fintype index] [DecidableEq index]
    (equiv : index ≃ index) :
    star (equivPermutationMatrix equiv) =
      equivPermutationMatrix equiv.symm := by

commit-pinned source · Verso Blueprint panel

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

theorem star_liftPrimitiveOneQubit {qubits : Nat} (target : Fin qubits)
    (gate : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
    star (liftPrimitiveOneQubit target gate) =
      liftPrimitiveOneQubit target (star gate) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “eval primitive gate”. Exact matrix denotation of one primitive instruction.

noncomputable def evalPrimitiveGate {qubits : Nat} : PrimitiveGate qubits →
    _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
  | .x target => equivPermutationMatrix (xBasisEquiv target)
  | .ry target angle => liftPrimitiveOneQubit target (standardRyMatrix angle.eval)
  | .rz target angle => liftPrimitiveOneQubit target (standardRzMatrix angle.eval)
  | .cx control target distinct =>
      equivPermutationMatrix (cxBasisEquiv control target distinct)

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveGate_unitary {qubits : Nat} (gate : PrimitiveGate qubits) :
    evalPrimitiveGate gate ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis qubits) ℂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “x basis equiv symm”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem xBasisEquiv_symm {qubits : Nat} (target : Fin qubits) :
    (xBasisEquiv target).symm = xBasisEquiv target := by

commit-pinned source · Verso Blueprint panel

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

theorem cxBasisEquiv_symm {qubits : Nat} (control target : Fin qubits)
    (distinct : control ≠ target) :
    (cxBasisEquiv control target distinct).symm =
      cxBasisEquiv control target distinct := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveGate_dagger {qubits : Nat}
    (gate : PrimitiveGate qubits) :
    evalPrimitiveGate gate.dagger = star (evalPrimitiveGate gate) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “eval primitive circuit”. Chronological circuit evaluation: later instructions multiply on the left.

noncomputable def evalPrimitiveCircuit {qubits : Nat} : PrimitiveCircuit qubits →
    _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
  | [] => 1
  | gate :: rest => evalPrimitiveCircuit rest * evalPrimitiveGate gate

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveCircuit_unitary {qubits : Nat}
    (circuit : PrimitiveCircuit qubits) :
    evalPrimitiveCircuit circuit ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis qubits) ℂ := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveCircuit_append {qubits : Nat}
    (left right : PrimitiveCircuit qubits) :
    evalPrimitiveCircuit (left ++ right) =
      evalPrimitiveCircuit right * evalPrimitiveCircuit left := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveCircuit_dagger {qubits : Nat}
    (circuit : PrimitiveCircuit qubits) :
    evalPrimitiveCircuit (circuit.reverse.map PrimitiveGate.dagger) =
      star (evalPrimitiveCircuit circuit) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “eval global phase”. Unit-modulus scalar represented by an exact global phase.

noncomputable def evalGlobalPhase (angle : ExactAngle) : ℂ :=
  Complex.exp ((angle.eval : ℂ) * Complex.I)

commit-pinned source · Verso Blueprint panel

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

theorem evalGlobalPhase_unitary (angle : ExactAngle) :
    evalGlobalPhase angle ∈ unitary ℂ := by

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalGlobalPhase_neg (angle : ExactAngle) :
    evalGlobalPhase (.neg angle) = star (evalGlobalPhase angle) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “eval primitive program”. Exact program semantics, with the same 'exp(i phase)' convention used by Qiskit and OpenQASM 3.

noncomputable def evalPrimitiveProgram {qubits : Nat}
    (program : PrimitiveProgram qubits) :
    _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ :=
  evalGlobalPhase program.globalPhase • evalPrimitiveCircuit program.circuit

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalPrimitiveProgram_identity (qubits : Nat) :
    evalPrimitiveProgram (PrimitiveProgram.identity qubits) = 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveProgram_seq {qubits : Nat}
    (left right : PrimitiveProgram qubits) :
    evalPrimitiveProgram (PrimitiveProgram.seq left right) =
      evalPrimitiveProgram right * evalPrimitiveProgram left := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveProgram_unitary {qubits : Nat}
    (program : PrimitiveProgram qubits) :
    evalPrimitiveProgram program ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis qubits) ℂ := by

commit-pinned source · Verso Blueprint panel

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

theorem evalPrimitiveProgram_dagger {qubits : Nat}
    (program : PrimitiveProgram qubits) :
    evalPrimitiveProgram program.dagger = star (evalPrimitiveProgram program) := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “primitive refinement”. A proposition-valued field is a requirement until a constructor supplies it. A typed primitive refinement records exact equality, not equality up to phase.

structure PrimitiveRefinement (qubits : Nat) where
  circuit : PrimitiveCircuit qubits
  target : _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
  exact : evalPrimitiveCircuit circuit = target

commit-pinned source · Verso Blueprint panel