QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean

This abbreviation gives a shorter name to the type or expression used for “warm robin four slot bits”. Two binary selector wires before flattening to 'Fin 4'.

abbrev WarmRobinFourSlotBits := Fin 2 × Fin 2

/-- Flatten the two selector wires. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot bits equiv”. Flatten the two selector wires.

def warmRobinFourSlotBitsEquiv : WarmRobinFourSlotBits ≃ Fin 4 :=
  finProdFinEquiv

/-- Uniform two-bit selector PREPARE. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot bits prepare”. Uniform two-bit selector PREPARE.

noncomputable def warmRobinFourSlotBitsPrepare :
    _root_.Matrix WarmRobinFourSlotBits WarmRobinFourSlotBits ℂ :=
  warmRobinUniformBitPrepare ⊗ₖ warmRobinUniformBitPrepare

/-- The two-bit selector PREPARE is unitary. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot bits prepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The two-bit selector PREPARE is unitary.

theorem warmRobinFourSlotBitsPrepare_unitary :
    warmRobinFourSlotBitsPrepare ∈
      _root_.Matrix.unitaryGroup WarmRobinFourSlotBits ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot selector prepare”. Flattened four-slot selector PREPARE.

noncomputable def warmRobinFourSlotSelectorPrepare :
    _root_.Matrix (Fin 4) (Fin 4) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFourSlotBitsEquiv
    warmRobinFourSlotBitsPrepare

/-- Reindexing preserves selector unitarity. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot selector prepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves selector unitarity.

theorem warmRobinFourSlotSelectorPrepare_unitary :
    warmRobinFourSlotSelectorPrepare ∈
      _root_.Matrix.unitaryGroup (Fin 4) ℂ := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot bits prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform clean-column amplitude before selector flattening.

@[simp] theorem warmRobinFourSlotBitsPrepare_cleanColumn
    (bits : WarmRobinFourSlotBits) :
    warmRobinFourSlotBitsPrepare bits (0, 0) =
      (((Real.sqrt 2 / 2 : Real) : ℂ) *
        ((Real.sqrt 2 / 2 : Real) : ℂ)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot selector prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform clean-column amplitude after selector flattening.

@[simp] theorem warmRobinFourSlotSelectorPrepare_cleanColumn (slot : Fin 4) :
    warmRobinFourSlotSelectorPrepare slot 0 =
      (((Real.sqrt 2 / 2 : Real) : ℂ) *
        ((Real.sqrt 2 / 2 : Real) : ℂ)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot selector prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. Every selector slot has probability exactly '1/4' in the clean column.

@[simp] theorem warmRobinFourSlotSelectorPrepare_probability (slot : Fin 4) :
    star (warmRobinFourSlotSelectorPrepare slot 0) *
        warmRobinFourSlotSelectorPrepare slot 0 = (1 / 4 : ℂ) := by

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “warm robin symmetry system”. Sector and reversal-pair coordinate used by the middle logical unitary.

abbrev WarmRobinSymmetrySystem := Fin 2 × Fin 4

/-- A four-shift SELECT preserves the symmetry sector. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot system perm”. A four-shift SELECT preserves the symmetry sector.

def warmRobinFourSlotSystemPerm
    (slot : Fin 4) (index : WarmRobinSymmetrySystem) :
    WarmRobinSymmetrySystem :=
  (index.1, warmRobinSymmetryFourShiftPerm slot index.2)

/-- Each sector-preserving four-shift SELECT is a basis bijection. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot system perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Each sector-preserving four-shift SELECT is a basis bijection.

theorem warmRobinFourSlotSystemPerm_bijective (slot : Fin 4) :
    Function.Bijective (warmRobinFourSlotSystemPerm slot) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot system equiv”. Package the sector-preserving SELECT as an equivalence.

noncomputable def warmRobinFourSlotSystemEquiv (slot : Fin 4) :
    WarmRobinSymmetrySystem ≃ WarmRobinSymmetrySystem :=
  Equiv.ofBijective (warmRobinFourSlotSystemPerm slot)
    (warmRobinFourSlotSystemPerm_bijective slot)

/-- Real amplitude encoded by a selector slot and sector-system column. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot coefficient”. Real amplitude encoded by a selector slot and sector-system column.

def warmRobinFourSlotCoefficient
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) : Real :=
  ((warmRobinSymmetryFourShiftAmplitude column.1 slot column.2 : Rat) : Real)

/-- Every four-slot real amplitude lies in `[-1,1]`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot coefficient abs le one”; the hypotheses and conclusion in the code panel fix its exact scope. Every four-slot real amplitude lies in '[-1,1]'.

theorem warmRobinFourSlotCoefficient_abs_le_one
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    |warmRobinFourSlotCoefficient slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

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

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

/-- Every controlled coefficient rotation is unitary. -/

commit-pinned source · Verso Blueprint panel

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

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

/-- The clean coefficient entry is the desired signed amplitude. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot rotation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The clean coefficient entry is the desired signed amplitude.

theorem warmRobinFourSlotRotation_cleanEntry
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    warmRobinFourSlotRotation slot column 0 0 =
      (warmRobinFourSlotCoefficient slot column : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot coefficient complex”; the hypotheses and conclusion in the code panel fix its exact scope. Rational and real-complex views of the four-slot coefficient agree.

theorem warmRobinFourSlotCoefficient_complex
    (slot : Fin 4) (column : WarmRobinSymmetrySystem) :
    (warmRobinFourSlotCoefficient slot column : ℂ) =
      (warmRobinSymmetryFourShiftAmplitude
        column.1 slot column.2 : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot middle logical unitary”. Product-register logical unitary in the symmetry-sector system basis.

noncomputable def warmRobinFourSlotMiddleLogicalUnitary :
    _root_.Matrix
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem)
      (LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ :=
  prepareAmplitudeSelectUnprepare
    warmRobinFourSlotSelectorPrepare
    warmRobinFourSlotRotation
    warmRobinFourSlotSystemEquiv

/-- The complete four-slot middle construction is exactly unitary. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot middle logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete four-slot middle construction is exactly unitary.

theorem warmRobinFourSlotMiddleLogicalUnitary_unitary :
    warmRobinFourSlotMiddleLogicalUnitary ∈
      _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 four slot sector clean formula”. Structural clean formula on the full sector-system basis.

noncomputable def warmRobinFourSlotSectorCleanFormula :
    _root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem Rat :=
  fun row column =>
    (1 / 4 : Rat) * ∑ slot : Fin 4,
      if warmRobinFourSlotSystemEquiv slot column = row then
        warmRobinSymmetryFourShiftAmplitude
          column.1 slot column.2
      else 0

/-- On one sector, the full-system formula is the existing four-shift formula. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot sector clean formula same”; the hypotheses and conclusion in the code panel fix its exact scope. On one sector, the full-system formula is the existing four-shift formula.

theorem warmRobinFourSlotSectorCleanFormula_same
    (sector : Fin 2) (row column : Fin 4) :
    warmRobinFourSlotSectorCleanFormula
        (sector, row) (sector, column) =
      warmRobinSymmetryFourShiftCleanFormula sector row column := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot sector clean formula cross”; the hypotheses and conclusion in the code panel fix its exact scope. Cross-sector clean entries vanish because SELECT preserves the sector.

theorem warmRobinFourSlotSectorCleanFormula_cross
    {rowSector columnSector : Fin 2} (sectorMismatch : rowSector ≠ columnSector)
    (row column : Fin 4) :
    warmRobinFourSlotSectorCleanFormula
        (rowSector, row) (columnSector, column) = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin four slot sector target”. Direct-sum normalized target in the symmetry-sector basis.

def warmRobinFourSlotSectorTarget :
    _root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem Rat :=
  fun row column =>
    if row.1 = column.1 then
      if row.1.val = 0 then
        (warmRobinSymmetryPlusBlock row.2 column.2 : Rat) / 224
      else
        (warmRobinSymmetryMinusBlock row.2 column.2 : Rat) / 224
    else 0

/-- The structural clean formula is exactly the normalized direct sum. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot sector clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The structural clean formula is exactly the normalized direct sum.

theorem warmRobinFourSlotSectorCleanFormula_eq_target
    (row column : WarmRobinSymmetrySystem) :
    warmRobinFourSlotSectorCleanFormula row column =
      warmRobinFourSlotSectorTarget row column := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot middle logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable clean-entry expansion specializes to the four-slot sector formula.

theorem warmRobinFourSlotMiddleLogicalUnitary_cleanEntry
    (row column : WarmRobinSymmetrySystem) :
    warmRobinFourSlotMiddleLogicalUnitary
        (0, (0, row)) (0, (0, column)) =
      (warmRobinFourSlotSectorCleanFormula row column : ℂ) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin four slot middle logical unitary clean entry eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The middle logical clean block is exactly the normalized sector target.

theorem warmRobinFourSlotMiddleLogicalUnitary_cleanEntry_eq_target
    (row column : WarmRobinSymmetrySystem) :
    warmRobinFourSlotMiddleLogicalUnitary
        (0, (0, row)) (0, (0, column)) =
      (warmRobinFourSlotSectorTarget row column : ℂ) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinFourSlotMiddleLogicalUnitary_cleanSystemBlock :
    cleanSystemBlock warmRobinFourSlotMiddleLogicalUnitary 0 0 =
      fun row column =>
        (warmRobinFourSlotSectorTarget row column : ℂ) := by

commit-pinned source · Verso Blueprint panel