QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

This definition gives the library's named construction or computation for “warm robin paper seven system perm”.

def warmRobinPaperSevenSystemPerm (slot column : Fin 8) : Fin 8 :=
  warmRobinSourceDTRow slot column

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenSystemPerm_bijective (slot : Fin 8) :
    Function.Bijective (warmRobinPaperSevenSystemPerm slot) :=
  warmRobinSourceDTRow_bijective_in_column slot

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven system equiv”.

noncomputable def warmRobinPaperSevenSystemEquiv (slot : Fin 8) :
    Fin 8 ≃ Fin 8 :=
  Equiv.ofBijective (warmRobinPaperSevenSystemPerm slot)
    (warmRobinPaperSevenSystemPerm_bijective slot)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem warmRobinPaperSevenSystemEquiv_apply
    (slot column : Fin 8) :
    warmRobinPaperSevenSystemEquiv slot column =
      warmRobinSourceDTRow slot column := rfl

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven coefficient rat”.

def warmRobinPaperSevenCoefficientRat (slot column : Fin 8) : Rat :=
  warmRobinSourceSevenPaddedCoefficient slot column

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenCoefficientRat_abs_le_one
    (slot column : Fin 8) :
    |warmRobinPaperSevenCoefficientRat slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven coefficient”.

def warmRobinPaperSevenCoefficient (slot column : Fin 8) : Real :=
  ((warmRobinPaperSevenCoefficientRat slot column : Rat) : Real)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenCoefficient_abs_le_one
    (slot column : Fin 8) :
    |warmRobinPaperSevenCoefficient slot column| ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven rotation”.

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

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenRotation_cleanEntry (slot column : Fin 8) :
    warmRobinPaperSevenRotation slot column 0 0 =
      (warmRobinPaperSevenCoefficient slot column : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven logical unitary”.

noncomputable def warmRobinPaperSevenLogicalUnitary :
    _root_.Matrix
      (LCUIndex (Fin 2) (Fin 8) (Fin 8))
      (LCUIndex (Fin 2) (Fin 8) (Fin 8)) ℂ :=
  prepareAmplitudeSelectUnprepare
    warmRobinPaperSevenSelectorPrepare
    warmRobinPaperSevenRotation
    warmRobinPaperSevenSystemEquiv

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenLogicalUnitary_cleanEntry
    (row column : Fin 8) :
    warmRobinPaperSevenLogicalUnitary
        (0, (0, row)) (0, (0, column)) =
      (warmRobinSourceSevenCleanFormula row column : ℂ) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenLogicalUnitary_cleanBlock :
    cleanSystemBlock warmRobinPaperSevenLogicalUnitary 0 0 =
      fun row column =>
        ((RobinEvolution.warmRobinTarget row column /
          RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven index equiv”. Flatten coefficient, selector, and system registers to seven qubits.

def warmRobinPaperSevenIndexEquiv :
    LCUIndex (Fin 2) (Fin 8) (Fin 8) ≃ Fin (gridSize 7) :=
  (Equiv.prodCongr (Equiv.refl (Fin 2)) finProdFinEquiv).trans
    finProdFinEquiv

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven clean index”.

noncomputable def warmRobinPaperSevenCleanIndex
    (system : Fin 8) : Fin (gridSize 7) :=
  warmRobinPaperSevenIndexEquiv (0, (0, system))

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven flat unitary”.

noncomputable def warmRobinPaperSevenFlatUnitary :
    _root_.Matrix (Fin (gridSize 7)) (Fin (gridSize 7)) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinPaperSevenIndexEquiv
    warmRobinPaperSevenLogicalUnitary

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenFlatUnitary_unitary :
    warmRobinPaperSevenFlatUnitary ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 7)) ℂ := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenFlatUnitary_cleanBlock
    (row column : Fin 8) :
    warmRobinPaperSevenFlatUnitary
        (warmRobinPaperSevenCleanIndex row)
        (warmRobinPaperSevenCleanIndex column) =
      ((RobinEvolution.warmRobinTarget row column /
        RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven block contains target”.

def warmRobinPaperSevenBlockContainsTarget : Prop :=
  ∀ row column : Fin 8,
    warmRobinPaperSevenFlatUnitary
        (warmRobinPaperSevenCleanIndex row)
        (warmRobinPaperSevenCleanIndex column) =
      warmRobinQueryTarget.operator row column /
        warmRobinQueryTarget.normalizer

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinPaperSevenBlockContainsTarget_proof :
    warmRobinPaperSevenBlockContainsTarget := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven t 2 schedule”.

def warmRobinPaperSevenT2Schedule : LayeredCircuit :=
  [ [ Gate.oracleCall "paper-seven PREPARE" ]
  , [ Gate.oracleCall "paper-seven amplitude loader" ]
  , [ Gate.oracleCall "paper-seven SELECT" ]
  , [ Gate.oracleCall "paper-seven PREPARE dagger" ] ]

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven t 2 circuit”.

def warmRobinPaperSevenT2Circuit : Circuit :=
  warmRobinPaperSevenT2Schedule.flatten

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven t 2 resource”.

def warmRobinPaperSevenT2Resource : Resource :=
  warmRobinPaperSevenT2Schedule.resource

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven operator candidate”.

noncomputable def warmRobinPaperSevenOperatorCandidate :
    OperatorBlockEncodingCandidate ℂ 3 where
  auxiliaryQubits := 4
  target := warmRobinQueryTarget
  unitary := warmRobinPaperSevenFlatUnitary
  layout := {
    systemQubits := 3
    signalQubits := 4
    pureAncillas := 0
  }
  circuit := warmRobinPaperSevenT2Circuit

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin paper seven verified block encoding”.

noncomputable def warmRobinPaperSevenVerifiedBlockEncoding :
    VerifiedOperatorBlockEncoding ℂ 3 where
  candidate := warmRobinPaperSevenOperatorCandidate
  unitaryProof := warmRobinPaperSevenFlatUnitary_unitary
  blockProof := warmRobinPaperSevenBlockContainsTarget_proof

commit-pinned source · Verso Blueprint panel