QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean

This abbreviation gives a shorter name to the type or expression used for “warm robin figure 4 full system”.

abbrev WarmRobinFigure4FullSystem := Fin 8 × (Fin 2 × Fin 2)

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4EncodeBits
    (coefficient : Fin 2) (selector : Fin 8)
    (system : WarmRobinFigure4FullSystem) : PrimitiveBasis 9
  | ⟨0, _⟩ => primitiveBits3LE selector 0
  | ⟨1, _⟩ => primitiveBits3LE selector 1
  | ⟨2, _⟩ => primitiveBits3LE selector 2
  | ⟨3, _⟩ => primitiveBits3LE system.1 0
  | ⟨4, _⟩ => primitiveBits3LE system.1 1
  | ⟨5, _⟩ => primitiveBits3LE system.1 2
  | ⟨6, _⟩ => coefficient
  | ⟨7, _⟩ => system.2.1

commit-pinned source · Verso Blueprint panel

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

def warmRobinFigure4BitsIndex (bits : PrimitiveBasis 9) :
    ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinFigure4FullSystem :=
  (bits 6, (warmRobinFigure4AddressBits bits,
    (warmRobinFigure4SystemBits bits, (bits 7, bits 8))))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bits index bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4BitsIndex_bijective :
    Function.Bijective warmRobinFigure4BitsIndex := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinFigure4BitsEquiv :
    PrimitiveBasis 9 ≃
      ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinFigure4FullSystem :=
  Equiv.ofBijective warmRobinFigure4BitsIndex
    warmRobinFigure4BitsIndex_bijective

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bits equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BitsEquiv_apply (bits : PrimitiveBasis 9) :
    warmRobinFigure4BitsEquiv bits = warmRobinFigure4BitsIndex bits := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 bits equiv encode”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4BitsEquiv_encode
    (coefficient : Fin 2) (selector : Fin 8)
    (system : WarmRobinFigure4FullSystem) :
    warmRobinFigure4BitsEquiv
        (warmRobinFigure4EncodeBits coefficient selector system) =
      (coefficient, (selector, system)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 prepare middle wires”.

def warmRobinFigure4PrepareMiddleWires : Fin 1 → Fin 9 := fun _ => 2

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinFigure4PrepareMiddleWires_ne_target (wire : Fin 1) :
    warmRobinFigure4PrepareMiddleWires wire ≠ (1 : Fin 9) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 prepare low wires”.

def warmRobinFigure4PrepareLowWires : Fin 2 → Fin 9
  | 0 => 1
  | _ => 2

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinFigure4PrepareLowWires_ne_target (wire : Fin 2) :
    warmRobinFigure4PrepareLowWires wire ≠ (0 : Fin 9) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 selector bits decode”; the hypotheses and conclusion in the code panel fix its exact scope.

@[simp] theorem warmRobinFigure4SelectorBits_decode
    (bits : PrimitiveBasis 9) (wire : Fin 3) :
    primitiveBits3LE (warmRobinFigure4AddressBits bits) wire =
      bits ⟨wire.val, by omega⟩ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare high context iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareHighContext_iff
    (row column : PrimitiveBasis 9) :
    (splitPrimitiveWire (2 : Fin 9) row).2 =
        (splitPrimitiveWire (2 : Fin 9) column).2 ↔
      row 6 = column 6 ∧
        (splitPrimitiveWire (2 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits row))).2 =
          (splitPrimitiveWire (2 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits column))).2 ∧
        (warmRobinFigure4SystemBits row, (row 7, row 8)) =
          (warmRobinFigure4SystemBits column, (column 7, column 8)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare high physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareHighPhysical_eval :
    evalPrimitiveGate (.ry (2 : Fin 9) warmRobinUniformSevenHighAngle) =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinFigure4BitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinFigure4FullSystem)
          warmRobinPaperSevenSelectorHighMatrix) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare middle context iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareMiddleContext_iff
    (row column : PrimitiveBasis 9) :
    (splitPrimitiveWire (1 : Fin 9) row).2 =
        (splitPrimitiveWire (1 : Fin 9) column).2 ↔
      row 6 = column 6 ∧
        (splitPrimitiveWire (1 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits row))).2 =
          (splitPrimitiveWire (1 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits column))).2 ∧
        (warmRobinFigure4SystemBits row, (row 7, row 8)) =
          (warmRobinFigure4SystemBits column, (column 7, column 8)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare middle physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareMiddlePhysical_eval :
    controlledRyBlockMatrix warmRobinFigure4PrepareMiddleWires 1
        warmRobinFigure4PrepareMiddleWires_ne_target
        warmRobinUniformSevenMiddleAngles =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinFigure4BitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinFigure4FullSystem)
          warmRobinPaperSevenSelectorMiddleMatrix) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare low context iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareLowContext_iff
    (row column : PrimitiveBasis 9) :
    (splitPrimitiveWire (0 : Fin 9) row).2 =
        (splitPrimitiveWire (0 : Fin 9) column).2 ↔
      row 6 = column 6 ∧
        (splitPrimitiveWire (0 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits row))).2 =
          (splitPrimitiveWire (0 : Fin 3)
            (primitiveBits3LE (warmRobinFigure4AddressBits column))).2 ∧
        (warmRobinFigure4SystemBits row, (row 7, row 8)) =
          (warmRobinFigure4SystemBits column, (column 7, column 8)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 prepare low physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4PrepareLowPhysical_eval :
    controlledRyBlockMatrix warmRobinFigure4PrepareLowWires 0
        warmRobinFigure4PrepareLowWires_ne_target
        warmRobinUniformSevenLowAngles =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinFigure4BitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinFigure4FullSystem)
          warmRobinPaperSevenSelectorLowMatrix) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 selector prepare circuit”.

noncomputable def warmRobinFigure4SelectorPrepareCircuit : PrimitiveCircuit 9 :=
  [.ry 2 warmRobinUniformSevenHighAngle] ++
    compileUniformlyControlledRy 1 warmRobinFigure4PrepareMiddleWires 1
      warmRobinFigure4PrepareMiddleWires_ne_target
      warmRobinUniformSevenMiddleAngles ++
    compileUniformlyControlledRy 2 warmRobinFigure4PrepareLowWires 0
      warmRobinFigure4PrepareLowWires_ne_target
      warmRobinUniformSevenLowAngles

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 selector prepare program”.

noncomputable def warmRobinFigure4SelectorPrepareProgram : PrimitiveProgram 9 where
  circuit := warmRobinFigure4SelectorPrepareCircuit
  globalPhase := .rational 0

/-- Required stage root: the physical first stage is the exact selector lift. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 after prepare”; the hypotheses and conclusion in the code panel fix its exact scope. Required stage root: the physical first stage is the exact selector lift.

theorem warmRobinFigure4_after_prepare :
    evalPrimitiveProgram warmRobinFigure4SelectorPrepareProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinFigure4BitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinFigure4FullSystem)
          warmRobinPaperSevenSelectorPrepare) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin figure 4 selector unprepare program”.

noncomputable def warmRobinFigure4SelectorUnprepareProgram : PrimitiveProgram 9 :=
  warmRobinFigure4SelectorPrepareProgram.dagger

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin figure 4 after unprepare”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinFigure4_after_unprepare :
    evalPrimitiveProgram warmRobinFigure4SelectorUnprepareProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinFigure4BitsEquiv.symm
        (star (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinFigure4FullSystem)
          warmRobinPaperSevenSelectorPrepare)) := by

commit-pinned source · Verso Blueprint panel