QuantumBlockEncoding/StatePreparationBellRoute.lean

This definition gives the library's named construction or computation for “bell ry angle”.

noncomputable def bellRyAngle : ExactAngle :=
  .piRational (1 / 2)

commit-pinned source · Verso Blueprint panel

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

theorem bellRyAngle_eval : bellRyAngle.eval = Real.pi / 2 := by

commit-pinned source · Verso Blueprint panel

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

theorem standardRyMatrix_bellRyAngle :
    standardRyMatrix bellRyAngle.eval = Robin.warmRobinUniformBitPrepare := by

commit-pinned source · Verso Blueprint panel

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

def bellControl : Fin 2 := 0

commit-pinned source · Verso Blueprint panel

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

def bellTargetWire : Fin 2 := 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bell control ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bellControl_ne_target : bellControl ≠ bellTargetWire := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def bellRyCircuit : PrimitiveCircuit 2 :=
  [PrimitiveGate.ry (0 : Fin 2) bellRyAngle]

commit-pinned source · Verso Blueprint panel

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

noncomputable def bellCxCircuit : PrimitiveCircuit 2 :=
  [PrimitiveGate.cx bellControl bellTargetWire bellControl_ne_target]

commit-pinned source · Verso Blueprint panel

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

noncomputable def bellPrimitiveCircuit : PrimitiveCircuit 2 :=
  bellRyCircuit ++ bellCxCircuit

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell after ry”.

noncomputable def bellAfterRy : StateVector (gridSize 2) ℂ :=
  bellAmplitude • basisKet (gridSize 2) (0 : Fin 4) +
    bellAmplitude • basisKet (gridSize 2) (1 : Fin 4)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem evalPrimitiveCircuitLE_singleton_cx_apply
    {qubits : Nat} (control target : Fin qubits) (distinct : control ≠ target)
    (row column : Fin (gridSize qubits)) :
    evalPrimitiveCircuitLE ([PrimitiveGate.cx control target distinct]) row column =
      if primitiveLEBits qubits row =
          cxBasisEquiv control target distinct (primitiveLEBits qubits column)
      then 1 else 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem bellRy_col_zero :
    (evalPrimitiveCircuitLE bellRyCircuit).col (0 : Fin 4) = bellAfterRy := by

commit-pinned source · Verso Blueprint panel

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

theorem bellRy_prepares :
    applyVec (evalPrimitiveCircuitLE bellRyCircuit) (zeroKet 2) = bellAfterRy := by

commit-pinned source · Verso Blueprint panel

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

theorem bellCx_on_afterRy :
    applyVec (evalPrimitiveCircuitLE bellCxCircuit) bellAfterRy = bellState := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bell primitive prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bellPrimitive_prepares_target :
    applyVec (evalPrimitiveCircuitLE bellPrimitiveCircuit) (zeroKet 2) =
      bellTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def bellPrimitiveRoute : ExactPrimitiveStatePreparationRoute 2 where
  target := bellTarget
  circuit := bellPrimitiveCircuit
  normalizationProof := bellTarget_normalized
  preparationProof := bellPrimitive_prepares_target

commit-pinned source · Verso Blueprint panel

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

theorem bellVerified_cost :
    bellPrimitiveRoute.cost =
      { auxiliaryQubits := 0, gateCount := 2, depth := 2, oracleCalls := 0 } := by

commit-pinned source · Verso Blueprint panel