QuantumBlockEncoding/Robin/Hadamard8Verified.lean

This abbreviation gives a shorter name to the type or expression used for “warm robin hadamard bits”. Three binary selector wires before flattening to 'Fin 8'.

abbrev WarmRobinHadamardBits := Fin 2 × (Fin 2 × Fin 2)

/-- Signal-register order used by the eight-slot selector. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard bits equiv”. Signal-register order used by the eight-slot selector.

def warmRobinHadamardBitsEquiv : WarmRobinHadamardBits ≃ Fin 8 :=
  (Equiv.prodCongr (Equiv.refl (Fin 2)) finProdFinEquiv).trans
    finProdFinEquiv

/-- One uniform binary PREPARE rotation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin uniform bit prepare”. One uniform binary PREPARE rotation.

noncomputable def warmRobinUniformBitPrepare :
    _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  realOrthogonalRotation (Real.sqrt 2 / 2) (Real.sqrt 2 / 2)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinUniformBitPrepare_unitary :
    warmRobinUniformBitPrepare ∈
      _root_.Matrix.unitaryGroup (Fin 2) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard bits prepare”. Tensor product PREPARE on three binary selector wires.

noncomputable def warmRobinHadamardBitsPrepare :
    _root_.Matrix WarmRobinHadamardBits WarmRobinHadamardBits ℂ :=
  warmRobinUniformBitPrepare ⊗ₖ
    (warmRobinUniformBitPrepare ⊗ₖ warmRobinUniformBitPrepare)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinHadamardBitsPrepare_unitary :
    warmRobinHadamardBitsPrepare ∈
      _root_.Matrix.unitaryGroup WarmRobinHadamardBits ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard 8 selector prepare”. The eight-dimensional selector PREPARE in the flattened selector basis.

noncomputable def warmRobinHadamard8SelectorPrepare :
    _root_.Matrix (Fin 8) (Fin 8) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinHadamardBitsEquiv
    warmRobinHadamardBitsPrepare

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinHadamard8SelectorPrepare_unitary :
    warmRobinHadamard8SelectorPrepare ∈
      _root_.Matrix.unitaryGroup (Fin 8) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard 8 coefficient”. Real clean amplitude used by selector slot and system column.

def warmRobinHadamard8Coefficient (slot column : Fin 8) : Real :=
  ((warmRobinEightSlotAmplitude slot column : Rat) : Real)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinHadamard8Coefficient_abs_le_one
    (slot column : Fin 8) :
    |warmRobinHadamard8Coefficient slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard 8 rotation”. Controlled two-dimensional amplitude block.

noncomputable def warmRobinHadamard8Rotation
    (slot column : Fin 8) : _root_.Matrix (Fin 2) (Fin 2) ℂ :=
  amplitudeRotation (warmRobinHadamard8Coefficient slot column)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinHadamard8Rotation_unitary (slot column : Fin 8) :
    warmRobinHadamard8Rotation slot column ∈
      _root_.Matrix.unitaryGroup (Fin 2) ℂ :=
  amplitudeRotation_unitary _

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinHadamard8Rotation_cleanEntry (slot column : Fin 8) :
    warmRobinHadamard8Rotation slot column 0 0 =
      (warmRobinHadamard8Coefficient slot column : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard 8 system equiv”. Each certified system permutation is packaged as an equivalence.

noncomputable def warmRobinHadamard8SystemEquiv (slot : Fin 8) :
    Fin 8 ≃ Fin 8 :=
  Equiv.ofBijective (warmRobinEightSlotPerm slot)
    (warmRobinEightSlotPerm_bijective slot)

/-- Product-register matrix before flattening to seven qubits. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin hadamard 8 logical unitary”. Product-register matrix before flattening to seven qubits.

noncomputable def warmRobinHadamard8LogicalUnitary :
    _root_.Matrix
      (LCUIndex (Fin 2) (Fin 8) (Fin 8))
      (LCUIndex (Fin 2) (Fin 8) (Fin 8)) ℂ :=
  prepareAmplitudeSelectUnprepare
    warmRobinHadamard8SelectorPrepare
    warmRobinHadamard8Rotation
    warmRobinHadamard8SystemEquiv

/-- The complete Hadamard-8 logical matrix is a standard complex unitary. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete Hadamard-8 logical matrix is a standard complex unitary.

theorem warmRobinHadamard8LogicalUnitary_unitary :
    warmRobinHadamard8LogicalUnitary ∈
      _root_.Matrix.unitaryGroup
        (LCUIndex (Fin 2) (Fin 8) (Fin 8)) ℂ := by

commit-pinned source · Verso Blueprint panel