QuantumBlockEncoding/Robin/PaperSevenPrepare.lean

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

def warmRobinUniformSevenHighAngle : ExactAngle :=
  .twiceArccosSqrtRational (4 / 7) (by norm_num)

commit-pinned source · Verso Blueprint panel

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

def warmRobinUniformSevenTailAngle : ExactAngle :=
  .twiceArccosSqrtRational (2 / 3) (by norm_num)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform seven middle angles”.

def warmRobinUniformSevenMiddleAngles
    (bits : PrimitiveBasis 1) : ExactAngle :=
  if bits 0 = 0 then .piRational (1 / 2)
  else warmRobinUniformSevenTailAngle

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform seven low angles”.

def warmRobinUniformSevenLowAngles
    (bits : PrimitiveBasis 2) : ExactAngle :=
  if bits 0 = 1 ∧ bits 1 = 1 then .rational 0
  else .piRational (1 / 2)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform seven middle wires”.

def warmRobinUniformSevenMiddleWires : Fin 1 → Fin 3 := fun _ => 2

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinUniformSevenMiddleWires_ne_target
    (wire : Fin 1) : warmRobinUniformSevenMiddleWires wire ≠ (1 : Fin 3) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform seven low wires”.

def warmRobinUniformSevenLowWires : Fin 2 → Fin 3
  | 0 => 1
  | _ => 2

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinUniformSevenLowWires_ne_target
    (wire : Fin 2) : warmRobinUniformSevenLowWires wire ≠ (0 : Fin 3) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinUniformSevenPrepareCircuit : PrimitiveCircuit 3 :=
  [.ry 2 warmRobinUniformSevenHighAngle] ++
    compileUniformlyControlledRy 1 warmRobinUniformSevenMiddleWires 1
      warmRobinUniformSevenMiddleWires_ne_target
      warmRobinUniformSevenMiddleAngles ++
    compileUniformlyControlledRy 2 warmRobinUniformSevenLowWires 0
      warmRobinUniformSevenLowWires_ne_target warmRobinUniformSevenLowAngles

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinUniformSevenPrepareProgram : PrimitiveProgram 3 where
  circuit := warmRobinUniformSevenPrepareCircuit
  globalPhase := .rational 0

/-- Independent stagewise matrix specification for the padded selector. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform seven prepare matrix”. Independent stagewise matrix specification for the padded selector.

noncomputable def warmRobinUniformSevenPrepareMatrix :
    _root_.Matrix (PrimitiveBasis 3) (PrimitiveBasis 3) ℂ :=
  controlledRyBlockMatrix warmRobinUniformSevenLowWires 0
      warmRobinUniformSevenLowWires_ne_target warmRobinUniformSevenLowAngles *
    (controlledRyBlockMatrix warmRobinUniformSevenMiddleWires 1
        warmRobinUniformSevenMiddleWires_ne_target
        warmRobinUniformSevenMiddleAngles *
      evalPrimitiveGate (.ry 2 warmRobinUniformSevenHighAngle))

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinUniformSevenPrepareProgram_eval :
    evalPrimitiveProgram warmRobinUniformSevenPrepareProgram =
      warmRobinUniformSevenPrepareMatrix := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenSelectorPrepare_unitary :
    warmRobinUniformSevenPrepareMatrix ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis 3) ℂ := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinUniformSevenPrepare_noOracleCalls :
    warmRobinUniformSevenPrepareProgram.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin uniform seven prepare counts”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinUniformSevenPrepare_counts :
    warmRobinUniformSevenPrepareCircuit.ryCount = 7 ∧
      warmRobinUniformSevenPrepareCircuit.cxCount = 8 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven padded slot”. The source selector has eight physical states even though only seven are active.

def warmRobinPaperSevenPaddedSlot (slot : Fin 8) : Option (Fin 7) :=
  if h : slot.val < 7 then some ⟨slot.val, h⟩ else none

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenPaddedSlot_seven :
    warmRobinPaperSevenPaddedSlot 7 = none := by decide

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven selector prepare”. The physical three-qubit PREPARE, flattened with the repository's declared little-endian convention.

noncomputable def warmRobinPaperSevenSelectorPrepare :
    _root_.Matrix (Fin 8) (Fin 8) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 3)
    warmRobinUniformSevenPrepareMatrix

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin paper seven selector prepare unitary flat”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinPaperSevenSelectorPrepare_unitary_flat :
    warmRobinPaperSevenSelectorPrepare ∈
      _root_.Matrix.unitaryGroup (Fin 8) ℂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin uniform seven prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem uses probabilities directly, so no arbitrary clean-column phase convention for '1 / sqrt 7' enters the LCU proof.

theorem warmRobinUniformSevenPrepare_probability (slot : Fin 8) :
    star (warmRobinPaperSevenSelectorPrepare slot 0) *
        warmRobinPaperSevenSelectorPrepare slot 0 =
      if slot.val < 7 then (1 / 7 : ℂ) else 0 := by

commit-pinned source · Verso Blueprint panel