QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean

This definition gives the library's named construction or computation for “warm robin symmetry xor perm”.

def warmRobinSymmetryXorPerm (slot column : Fin 4) : Fin 4 :=
  ⟨slot.val ^^^ column.val, by
    simpa using Nat.xor_lt_two_pow (n := 2) slot.isLt column.isLt⟩

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin symmetry xor perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinSymmetryXorPerm_bijective (slot : Fin 4) :
    Function.Bijective (warmRobinSymmetryXorPerm slot) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin symmetry sector block”.

def warmRobinSymmetrySectorBlock
    (sector : Fin 2) : Matrix 4 4 Int :=
  if sector = 0 then warmRobinSymmetryPlusBlock else warmRobinSymmetryMinusBlock

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin symmetry xor weight”.

def warmRobinSymmetryXorWeight
    (sector : Fin 2) (slot column : Fin 4) : Int :=
  warmRobinSymmetrySectorBlock sector
    (warmRobinSymmetryXorPerm slot column) column

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin symmetry xor amplitude”.

def warmRobinSymmetryXorAmplitude
    (sector : Fin 2) (slot column : Fin 4) : Rat :=
  warmRobinSymmetryXorWeight sector slot column / 56

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin symmetry xor amplitude bounded”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinSymmetryXorAmplitude_bounded
    (sector : Fin 2) (slot column : Fin 4) :
    |warmRobinSymmetryXorAmplitude sector slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin symmetry xor decomposition”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinSymmetryXorDecomposition
    (sector : Fin 2) (row column : Fin 4) :
    warmRobinSymmetrySectorBlock sector row column =
      ∑ slot : Fin 4,
        if warmRobinSymmetryXorPerm slot column = row then
          warmRobinSymmetryXorWeight sector slot column
        else 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot system perm”.

def warmRobinXorFourSlotSystemPerm
    (slot : Fin 4) (index : WarmRobinSymmetrySystem) :
    WarmRobinSymmetrySystem :=
  (index.1, warmRobinSymmetryXorPerm slot index.2)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSystemPerm_bijective (slot : Fin 4) :
    Function.Bijective (warmRobinXorFourSlotSystemPerm slot) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot system equiv”.

noncomputable def warmRobinXorFourSlotSystemEquiv (slot : Fin 4) :
    WarmRobinSymmetrySystem ≃ WarmRobinSymmetrySystem :=
  Equiv.ofBijective (warmRobinXorFourSlotSystemPerm slot)
    (warmRobinXorFourSlotSystemPerm_bijective slot)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem warmRobinXorFourSlotSystemEquiv_apply
    (slot : Fin 4) (index : WarmRobinSymmetrySystem) :
    warmRobinXorFourSlotSystemEquiv slot index =
      warmRobinXorFourSlotSystemPerm slot index := rfl

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot coefficient”.

def warmRobinXorFourSlotCoefficient
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) : Real :=
  ((warmRobinSymmetryXorAmplitude column.1 slot column.2 : Rat) : Real)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot coefficient abs le one”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotCoefficient_abs_le_one
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    |warmRobinXorFourSlotCoefficient slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot rotation”.

noncomputable def warmRobinXorFourSlotRotation
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  amplitudeRotation (warmRobinXorFourSlotCoefficient slot column)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotRotation_unitary
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    warmRobinXorFourSlotRotation slot column ∈
      _root_.Matrix.unitaryGroup (Fin 2) ℂ :=
  amplitudeRotation_unitary _

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotRotation_cleanEntry
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    warmRobinXorFourSlotRotation slot column 0 0 =
      (warmRobinXorFourSlotCoefficient slot column : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot middle logical unitary”.

noncomputable def warmRobinXorFourSlotMiddleLogicalUnitary :
    _root_.Matrix
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem)
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ :=
  prepareAmplitudeSelectUnprepare
    warmRobinFourSlotSelectorPrepare
    warmRobinXorFourSlotRotation
    warmRobinXorFourSlotSystemEquiv

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotMiddleLogicalUnitary_unitary :
    warmRobinXorFourSlotMiddleLogicalUnitary ∈
      _root_.Matrix.unitaryGroup
        (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot sector clean formula”.

def warmRobinXorFourSlotSectorCleanFormula :
    _root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem Rat :=
  fun row column =>
    (1 / 4 : Rat) * ∑ slot : Fin 4,
      if warmRobinXorFourSlotSystemPerm slot column = row then
        warmRobinSymmetryXorAmplitude column.1 slot column.2
      else 0

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotCleanFormula_eq_target
    (row column : WarmRobinSymmetrySystem) :
    warmRobinXorFourSlotSectorCleanFormula row column =
      warmRobinFourSlotSectorTarget row column := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot middle logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotMiddleLogicalUnitary_cleanEntry
    (row column : WarmRobinSymmetrySystem) :
    warmRobinXorFourSlotMiddleLogicalUnitary
        (0, (0, row)) (0, (0, column)) =
      (warmRobinXorFourSlotSectorCleanFormula row column : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot middle logical unitary clean system block”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotMiddleLogicalUnitary_cleanSystemBlock :
    cleanSystemBlock warmRobinXorFourSlotMiddleLogicalUnitary 0 0 =
      fun row column => (warmRobinFourSlotSectorTarget row column : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot pair logical unitary”.

noncomputable def warmRobinXorFourSlotPairLogicalUnitary :
    _root_.Matrix
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem)
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ :=
  conjugateSystem warmRobinSymmetryBasisChange
    warmRobinXorFourSlotMiddleLogicalUnitary

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPairLogicalUnitary_unitary :
    warmRobinXorFourSlotPairLogicalUnitary ∈
      _root_.Matrix.unitaryGroup
        (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot pair logical unitary clean system block”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotPairLogicalUnitary_cleanSystemBlock :
    cleanSystemBlock warmRobinXorFourSlotPairLogicalUnitary 0 0 =
      warmRobinPairNormalizedTargetComplex := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot flat unitary”.

noncomputable def warmRobinXorFourSlotFlatUnitary :
    _root_.Matrix (Fin (gridSize 6)) (Fin (gridSize 6)) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFourSlotIndexEquiv
    warmRobinXorFourSlotPairLogicalUnitary

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotFlatUnitary_unitary :
    warmRobinXorFourSlotFlatUnitary ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 6)) ℂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotFlatUnitary_cleanBlock
    (row column : Fin 8) :
    warmRobinXorFourSlotFlatUnitary
        (warmRobinFourSlotCleanIndex row)
        (warmRobinFourSlotCleanIndex column) =
      ((RobinEvolution.warmRobinTarget row column /
        RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel