QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean

This definition gives the library's named construction or computation for “warm robin paper seven amplitude control wires”.

def warmRobinPaperSevenAmplitudeControlWires : Fin 6 → Fin 8 := fun wire =>
  ⟨wire.val, by omega⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude control wires ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenAmplitudeControlWires_ne_target
    (wire : Fin 6) :
    warmRobinPaperSevenAmplitudeControlWires wire ≠ (6 : Fin 8) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude system”.

def warmRobinPaperSevenAmplitudeSystem
    (bits : PrimitiveBasis 6) : Fin 8 :=
  ⟨(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val, by omega⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude selector”.

def warmRobinPaperSevenAmplitudeSelector
    (bits : PrimitiveBasis 6) : Fin 8 :=
  ⟨(bits 3).val + 2 * (bits 4).val + 4 * (bits 5).val, by omega⟩

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude angle”.

noncomputable def warmRobinPaperSevenAmplitudeAngle
    (bits : PrimitiveBasis 6) : ExactAngle :=
  .twiceArccosRational
    (warmRobinPaperSevenCoefficientRat
      (warmRobinPaperSevenAmplitudeSelector bits)
      (warmRobinPaperSevenAmplitudeSystem bits))
    (by
      simpa [warmRobinPaperSevenCoefficient] using
        warmRobinPaperSevenCoefficient_abs_le_one
          (warmRobinPaperSevenAmplitudeSelector bits)
          (warmRobinPaperSevenAmplitudeSystem bits))

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenAmplitudeRy_eq_rotation
    (bits : PrimitiveBasis 6) :
    standardRyMatrix (warmRobinPaperSevenAmplitudeAngle bits).eval =
      warmRobinPaperSevenRotation
        (warmRobinPaperSevenAmplitudeSelector bits)
        (warmRobinPaperSevenAmplitudeSystem bits) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude context index”.

def warmRobinPaperSevenAmplitudeContextIndex
    (context : OtherPrimitiveWires (6 : Fin 8) → Fin 2) :
    Fin 8 × WarmRobinPaperSevenFullSystem :=
  let bit (wire : Fin 6) : Fin 2 :=
    context ⟨warmRobinPaperSevenAmplitudeControlWires wire,
      warmRobinPaperSevenAmplitudeControlWires_ne_target wire⟩
  let system : Fin 8 :=
    ⟨(bit 0).val + 2 * (bit 1).val + 4 * (bit 2).val, by omega⟩
  let selector : Fin 8 :=
    ⟨(bit 3).val + 2 * (bit 4).val + 4 * (bit 5).val, by omega⟩
  (selector, (system, context ⟨7, by decide⟩))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude context index bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenAmplitudeContextIndex_bijective :
    Function.Bijective warmRobinPaperSevenAmplitudeContextIndex := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude context equiv”.

noncomputable def warmRobinPaperSevenAmplitudeContextEquiv :
    (OtherPrimitiveWires (6 : Fin 8) → Fin 2) ≃
      Fin 8 × WarmRobinPaperSevenFullSystem :=
  Equiv.ofBijective warmRobinPaperSevenAmplitudeContextIndex
    warmRobinPaperSevenAmplitudeContextIndex_bijective

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude context equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinPaperSevenAmplitudeContextEquiv_apply
    (context : OtherPrimitiveWires (6 : Fin 8) → Fin 2) :
    warmRobinPaperSevenAmplitudeContextEquiv context =
      warmRobinPaperSevenAmplitudeContextIndex context := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude context iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenAmplitude_context_iff
    (row column : PrimitiveBasis 8) :
    (splitPrimitiveWire (6 : Fin 8) row).2 =
        (splitPrimitiveWire (6 : Fin 8) column).2 ↔
      (warmRobinPaperSevenBitsEquiv row).2 =
        (warmRobinPaperSevenBitsEquiv column).2 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven controlled ry eq amplitude lift”; the hypotheses and conclusion in the code panel fix its exact scope. Exact equality between the physical six-control RY block and the logical amplitude lift, including the otherwise dirty 'q7' workspace coordinate.

theorem warmRobinPaperSevenControlledRy_eq_amplitudeLift :
    controlledRyBlockMatrix warmRobinPaperSevenAmplitudeControlWires 6
        warmRobinPaperSevenAmplitudeControlWires_ne_target
        warmRobinPaperSevenAmplitudeAngle =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinPaperSevenBitsEquiv.symm
        (ComplexLCU.amplitudeLift warmRobinPaperSevenWorkspaceRotation) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude circuit”.

noncomputable def warmRobinPaperSevenAmplitudeCircuit : PrimitiveCircuit 8 :=
  compileUniformlyControlledRy 6 warmRobinPaperSevenAmplitudeControlWires 6
    warmRobinPaperSevenAmplitudeControlWires_ne_target
    warmRobinPaperSevenAmplitudeAngle

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven amplitude program”.

noncomputable def warmRobinPaperSevenAmplitudeProgram : PrimitiveProgram 8 where
  circuit := warmRobinPaperSevenAmplitudeCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude program eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenAmplitudeProgram_eval :
    evalPrimitiveProgram warmRobinPaperSevenAmplitudeProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinPaperSevenBitsEquiv.symm
        (ComplexLCU.amplitudeLift warmRobinPaperSevenWorkspaceRotation) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven amplitude program no oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenAmplitudeProgram_noOracleCalls :
    warmRobinPaperSevenAmplitudeProgram.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

commit-pinned source · Verso Blueprint panel