QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean

This definition gives the library's named construction or computation for “warm robin pair coordinate circuit”. System-wire order is '(p0, p1, sector)'.

def warmRobinPairCoordinateCircuit : PrimitiveCircuit 3 :=
  [ .cx 2 1 (by decide), .cx 2 0 (by decide) ]

commit-pinned source · Verso Blueprint panel

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

def warmRobinPairCoordinateBasisEquiv :
    PrimitiveBasis 3 ≃ PrimitiveBasis 3 :=
  (cxBasisEquiv (2 : Fin 3) (1 : Fin 3) (by decide)).trans
    (cxBasisEquiv (2 : Fin 3) (0 : Fin 3) (by decide))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin pair coordinate circuit eval eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPairCoordinateCircuit_eval_eq :
    evalPrimitiveCircuit warmRobinPairCoordinateCircuit =
      ComplexLCU.equivPermutationMatrix warmRobinPairCoordinateBasisEquiv := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin pair bits”.

def warmRobinPairBits (index : WarmRobinSymmetrySystem) : PrimitiveBasis 3 :=
  fun wire =>
    match wire.val with
    | 0 => ⟨index.2.val % 2, Nat.mod_lt _ (by decide)⟩
    | 1 => ⟨index.2.val / 2, by omega⟩
    | _ => index.1

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin original bits value”.

def warmRobinOriginalBitsValue (state : PrimitiveBasis 3) : Nat :=
  state 0 + 2 * state 1 + 4 * state 2

/-- The two CX gates implement the non-free pair-coordinate reindex exactly. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin pair coordinate circuit image”; the hypotheses and conclusion in the code panel fix its exact scope. The two CX gates implement the non-free pair-coordinate reindex exactly.

theorem warmRobinPairCoordinateCircuit_image
    (index : WarmRobinSymmetrySystem) :
    warmRobinOriginalBitsValue
        (warmRobinPairCoordinateBasisEquiv (warmRobinPairBits index)) =
      (warmRobinPairSystemEquiv index).val := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin pair coordinate circuit bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPairCoordinateCircuit_bijective :
    Function.Bijective warmRobinPairCoordinateBasisEquiv :=
  warmRobinPairCoordinateBasisEquiv.bijective

/-- Lean-owned exact standard-RY angle for one loader branch. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot exact angle”. Lean-owned exact standard-RY angle for one loader branch.

noncomputable def warmRobinFourSlotExactAngle
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) : ExactAngle :=
  .twiceArccosRational
    (warmRobinSymmetryFourShiftAmplitude column.1 slot column.2)
    (by
      simpa [warmRobinFourSlotCoefficient] using
        warmRobinFourSlotCoefficient_abs_le_one slot column)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot exact angle eval”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFourSlotExactAngle_eval
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    (warmRobinFourSlotExactAngle slot column).eval =
      2 * Real.arccos (warmRobinFourSlotCoefficient slot column) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot exact ry eq rotation”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFourSlotExactRy_eq_rotation
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    standardRyMatrix (warmRobinFourSlotExactAngle slot column).eval =
      warmRobinFourSlotRotation slot column := by

commit-pinned source · Verso Blueprint panel