QuantumBlockEncoding/Robin/SymmetryXorFourSlotPrimitive.lean

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

def warmRobinXorFourSlotSelectCircuit : PrimitiveCircuit 6 :=
  [ .cx 3 0 (by decide), .cx 4 1 (by decide) ]

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotSelectBasisEquiv :
    PrimitiveBasis 6 ≃ PrimitiveBasis 6 :=
  (cxBasisEquiv (3 : Fin 6) (0 : Fin 6) (by decide)).trans
    (cxBasisEquiv (4 : Fin 6) (1 : Fin 6) (by decide))

/-- The two selected system bits are XORed with the selector, while the sector,
selector, and coefficient wires are unchanged. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot select basis action eq perm”; the hypotheses and conclusion in the code panel fix its exact scope. The two selected system bits are XORed with the selector, while the sector, selector, and coefficient wires are unchanged.

theorem warmRobinXorFourSlotSelectBasisAction_eq_perm :
    ∀ bits : PrimitiveBasis 6,
      let selected := warmRobinXorFourSlotSelectBasisEquiv bits
      (selected 0).val + 2 * (selected 1).val =
          ((bits 0).val + 2 * (bits 1).val) ^^^
            ((bits 3).val + 2 * (bits 4).val) ∧
        selected 2 = bits 2 ∧ selected 3 = bits 3 ∧
        selected 4 = bits 4 ∧ selected 5 = bits 5 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot select program eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact matrix semantics of the physical XOR SELECT program.

theorem warmRobinXorFourSlotSelectProgram_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotSelectCircuit =
      ComplexLCU.equivPermutationMatrix warmRobinXorFourSlotSelectBasisEquiv := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot select program no oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotSelectProgram_noOracleCalls :
    warmRobinXorFourSlotSelectCircuit.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotControlWires : Fin 5 → Fin 6 := fun wire =>
  ⟨wire.val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotControlWires_ne_target
    (wire : Fin 5) : warmRobinXorFourSlotControlWires wire ≠ (5 : Fin 6) := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotControlPair
    (bits : PrimitiveBasis 5) : Fin 4 :=
  ⟨(bits 0).val + 2 * (bits 1).val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotControlSector
    (bits : PrimitiveBasis 5) : Fin 2 := bits 2

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotControlSelector
    (bits : PrimitiveBasis 5) : Fin 4 :=
  ⟨(bits 3).val + 2 * (bits 4).val, by omega⟩

/-- Exact standard-RY angle for each of the 32 multiplexor branches. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot amplitude angle”. Exact standard-RY angle for each of the 32 multiplexor branches.

noncomputable def warmRobinXorFourSlotAmplitudeAngle
    (bits : PrimitiveBasis 5) : ExactAngle :=
  let column : WarmRobinSymmetrySystem :=
    (warmRobinXorFourSlotControlSector bits,
      warmRobinXorFourSlotControlPair bits)
  let slot := warmRobinXorFourSlotControlSelector bits
  .twiceArccosRational
    (warmRobinSymmetryXorAmplitude column.1 slot column.2)
    (by
      simpa [warmRobinXorFourSlotCoefficient] using
        warmRobinXorFourSlotCoefficient_abs_le_one slot column)

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotAmplitudeAngle_eval
    (bits : PrimitiveBasis 5) :
    (warmRobinXorFourSlotAmplitudeAngle bits).eval =
      2 * Real.arccos
        (warmRobinXorFourSlotCoefficient
          (warmRobinXorFourSlotControlSelector bits)
          (warmRobinXorFourSlotControlSector bits,
            warmRobinXorFourSlotControlPair bits)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot amplitude ry eq rotation”; the hypotheses and conclusion in the code panel fix its exact scope. Every exact angle denotes the corresponding T2 amplitude rotation.

theorem warmRobinXorFourSlotAmplitudeRy_eq_rotation
    (bits : PrimitiveBasis 5) :
    standardRyMatrix (warmRobinXorFourSlotAmplitudeAngle bits).eval =
      warmRobinXorFourSlotRotation
        (warmRobinXorFourSlotControlSelector bits)
        (warmRobinXorFourSlotControlSector bits,
          warmRobinXorFourSlotControlPair bits) := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotContextIndex
    (context : OtherPrimitiveWires (5 : Fin 6) → Fin 2) :
    Fin 4 × WarmRobinSymmetrySystem :=
  let bit (wire : Fin 5) : Fin 2 :=
    context ⟨warmRobinXorFourSlotControlWires wire,
      warmRobinXorFourSlotControlWires_ne_target wire⟩
  (⟨(bit 3).val + 2 * (bit 4).val, by omega⟩,
    (bit 2, ⟨(bit 0).val + 2 * (bit 1).val, by omega⟩))

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotContextIndex_bijective :
    Function.Bijective warmRobinXorFourSlotContextIndex := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotContextEquiv :
    (OtherPrimitiveWires (5 : Fin 6) → Fin 2) ≃
      Fin 4 × WarmRobinSymmetrySystem :=
  Equiv.ofBijective warmRobinXorFourSlotContextIndex
    warmRobinXorFourSlotContextIndex_bijective

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem warmRobinXorFourSlotContextEquiv_apply
    (context : OtherPrimitiveWires (5 : Fin 6) → Fin 2) :
    warmRobinXorFourSlotContextEquiv context =
      warmRobinXorFourSlotContextIndex context := rfl

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotMiddleBitsEquiv :
    PrimitiveBasis 6 ≃
      ComplexLCU.LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem :=
  (splitPrimitiveWire 5).trans
    (Equiv.prodCongr (Equiv.refl (Fin 2))
      warmRobinXorFourSlotContextEquiv)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem warmRobinXorFourSlotMiddleBitsEquiv_apply
    (bits : PrimitiveBasis 6) :
    warmRobinXorFourSlotMiddleBitsEquiv bits =
      (bits 5,
        (⟨(bits 3).val + 2 * (bits 4).val, by omega⟩,
          (bits 2, ⟨(bits 0).val + 2 * (bits 1).val, by omega⟩))) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSelectBasisAction_middleIndex
    (bits : PrimitiveBasis 6) :
    warmRobinXorFourSlotMiddleBitsEquiv
        (warmRobinXorFourSlotSelectBasisEquiv bits) =
      ComplexLCU.controlledSystemEquiv warmRobinXorFourSlotSystemEquiv
        (warmRobinXorFourSlotMiddleBitsEquiv bits) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot select program eval reindexed”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix-level SELECT refinement under the exact middle-register reindex.

theorem warmRobinXorFourSlotSelectProgram_eval_reindexed :
    evalPrimitiveCircuit warmRobinXorFourSlotSelectCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.selectLift (coefficient := Fin 2)
          warmRobinXorFourSlotSystemEquiv) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot controlled ry eq amplitude lift”; the hypotheses and conclusion in the code panel fix its exact scope. The generic five-control multiplexor is exactly the T2 amplitude lift after the explicit little-endian product-register reindexing.

theorem warmRobinXorFourSlotControlledRy_eq_amplitudeLift :
    controlledRyBlockMatrix warmRobinXorFourSlotControlWires 5
        warmRobinXorFourSlotControlWires_ne_target
        warmRobinXorFourSlotAmplitudeAngle =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.amplitudeLift warmRobinXorFourSlotRotation) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotSelectorLowMatrix :
    _root_.Matrix (Fin 4) (Fin 4) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFourSlotBitsEquiv
    ((1 : _root_.Matrix (Fin 2) (Fin 2) ℂ) ⊗ₖ warmRobinUniformBitPrepare)

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotSelectorHighMatrix :
    _root_.Matrix (Fin 4) (Fin 4) ℂ :=
  _root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFourSlotBitsEquiv
    (warmRobinUniformBitPrepare ⊗ₖ (1 : _root_.Matrix (Fin 2) (Fin 2) ℂ))

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot selector high low eq prepare”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotSelectorHighLow_eq_prepare :
    warmRobinXorFourSlotSelectorHighMatrix *
        warmRobinXorFourSlotSelectorLowMatrix =
      warmRobinFourSlotSelectorPrepare := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotSelectorPrepareCircuit : PrimitiveCircuit 6 :=
  [ .ry 3 (.piRational (1 / 2)), .ry 4 (.piRational (1 / 2)) ]

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem warmRobinFourSlotBitsEquiv_symm_pack
    (low high : Fin 2) :
    warmRobinFourSlotBitsEquiv.symm
        ⟨low.val + 2 * high.val, by omega⟩ = (high, low) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotLowContext_iff
    (row column : PrimitiveBasis 6) :
    (splitPrimitiveWire (3 : Fin 6) row).2 =
        (splitPrimitiveWire (3 : Fin 6) column).2 ↔
      row 5 = column 5 ∧ row 4 = column 4 ∧ row 2 = column 2 ∧
        (⟨(row 0).val + 2 * (row 1).val, by omega⟩ : Fin 4) =
          ⟨(column 0).val + 2 * (column 1).val, by omega⟩ := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotHighContext_iff
    (row column : PrimitiveBasis 6) :
    (splitPrimitiveWire (4 : Fin 6) row).2 =
        (splitPrimitiveWire (4 : Fin 6) column).2 ↔
      row 5 = column 5 ∧ row 3 = column 3 ∧ row 2 = column 2 ∧
        (⟨(row 0).val + 2 * (row 1).val, by omega⟩ : Fin 4) =
          ⟨(column 0).val + 2 * (column 1).val, by omega⟩ := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSelectorLow_eval :
    evalPrimitiveGate (.ry (3 : Fin 6) (.piRational (1 / 2))) =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinSymmetrySystem)
          warmRobinXorFourSlotSelectorLowMatrix) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSelectorHigh_eval :
    evalPrimitiveGate (.ry (4 : Fin 6) (.piRational (1 / 2))) =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinSymmetrySystem)
          warmRobinXorFourSlotSelectorHighMatrix) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSelectorPrepareCircuit_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotSelectorPrepareCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinSymmetrySystem)
          warmRobinFourSlotSelectorPrepare) := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotSelectorUnprepareCircuit : PrimitiveCircuit 6 :=
  warmRobinXorFourSlotSelectorPrepareCircuit.reverse.map PrimitiveGate.dagger

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSelectorUnprepareCircuit_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotSelectorUnprepareCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (star (ComplexLCU.selectorLift (coefficient := Fin 2)
          (system := WarmRobinSymmetrySystem)
          warmRobinFourSlotSelectorPrepare)) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotAmplitudeCircuit : PrimitiveCircuit 6 :=
  compileUniformlyControlledRy 5 warmRobinXorFourSlotControlWires 5
    warmRobinXorFourSlotControlWires_ne_target
    warmRobinXorFourSlotAmplitudeAngle

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotAmplitudeProgram : PrimitiveProgram 6 where
  circuit := warmRobinXorFourSlotAmplitudeCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotAmplitudeProgram_eval :
    evalPrimitiveProgram warmRobinXorFourSlotAmplitudeProgram =
      controlledRyBlockMatrix warmRobinXorFourSlotControlWires 5
        warmRobinXorFourSlotControlWires_ne_target
        warmRobinXorFourSlotAmplitudeAngle := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotAmplitudeCircuit_eval_reindexed :
    evalPrimitiveCircuit warmRobinXorFourSlotAmplitudeCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.amplitudeLift warmRobinXorFourSlotRotation) := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotPrimitiveMiddleCircuit :
    PrimitiveCircuit 6 :=
  warmRobinXorFourSlotSelectorPrepareCircuit ++
    warmRobinXorFourSlotAmplitudeCircuit ++
    warmRobinXorFourSlotSelectCircuit ++
    warmRobinXorFourSlotSelectorUnprepareCircuit

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitiveMiddle_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveMiddleCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        warmRobinXorFourSlotMiddleLogicalUnitary := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotPairCoordinateCircuit : PrimitiveCircuit 6 :=
  [ .cx 2 1 (by decide), .cx 2 0 (by decide) ]

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotPairCoordinateBasisEquiv :
    PrimitiveBasis 6 ≃ PrimitiveBasis 6 :=
  (cxBasisEquiv (2 : Fin 6) (1 : Fin 6) (by decide)).trans
    (cxBasisEquiv (2 : Fin 6) (0 : Fin 6) (by decide))

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPairCoordinateCircuit_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotPairCoordinateCircuit =
      ComplexLCU.equivPermutationMatrix
        warmRobinXorFourSlotPairCoordinateBasisEquiv := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPairCoordinateBasisEquiv_involutive :
    Function.Involutive warmRobinXorFourSlotPairCoordinateBasisEquiv := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSymmetryContext_iff
    (row column : PrimitiveBasis 6) :
    (splitPrimitiveWire (2 : Fin 6) row).2 =
        (splitPrimitiveWire (2 : Fin 6) column).2 ↔
      row 5 = column 5 ∧
        (⟨(row 3).val + 2 * (row 4).val, by omega⟩ : Fin 4) =
          ⟨(column 3).val + 2 * (column 4).val, by omega⟩ ∧
        (⟨(row 0).val + 2 * (row 1).val, by omega⟩ : Fin 4) =
          ⟨(column 0).val + 2 * (column 1).val, by omega⟩ := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotSymmetryPrepareCircuit : PrimitiveCircuit 6 :=
  [ .ry 2 (.piRational (1 / 2)) ]

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSymmetryPrepareCircuit_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotSymmetryPrepareCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (ComplexLCU.systemLift (coefficient := Fin 2) (selector := Fin 4)
          warmRobinSymmetryBasisChange) := by

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotSymmetryUnprepareCircuit : PrimitiveCircuit 6 :=
  warmRobinXorFourSlotSymmetryPrepareCircuit.reverse.map PrimitiveGate.dagger

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotSymmetryUnprepareCircuit_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotSymmetryUnprepareCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        (star (ComplexLCU.systemLift (coefficient := Fin 2) (selector := Fin 4)
          warmRobinSymmetryBasisChange)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot primitive pair circuit”. The middle logical unitary conjugated back from symmetry-sector to pair coordinates, still expressed on the six named primitive wires.

noncomputable def warmRobinXorFourSlotPrimitivePairCircuit :
    PrimitiveCircuit 6 :=
  warmRobinXorFourSlotSymmetryUnprepareCircuit ++
    warmRobinXorFourSlotPrimitiveMiddleCircuit ++
    warmRobinXorFourSlotSymmetryPrepareCircuit

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitivePair_eval :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitivePairCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotMiddleBitsEquiv.symm
        warmRobinXorFourSlotPairLogicalUnitary := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot original bits equiv”. The basis interpretation after the physical pair-coordinate CX stage.

noncomputable def warmRobinXorFourSlotOriginalBitsEquiv :
    PrimitiveBasis 6 ≃
      ComplexLCU.LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem :=
  warmRobinXorFourSlotPairCoordinateBasisEquiv.trans
    warmRobinXorFourSlotMiddleBitsEquiv

/-- The pair-coordinate circuit, the logical pair circuit, and its inverse in
the chronological physical order required by the six-wire implementation. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot primitive circuit”. The pair-coordinate circuit, the logical pair circuit, and its inverse in the chronological physical order required by the six-wire implementation.

noncomputable def warmRobinXorFourSlotPrimitiveCircuit : PrimitiveCircuit 6 :=
  warmRobinXorFourSlotPairCoordinateCircuit ++
    warmRobinXorFourSlotPrimitivePairCircuit ++
    warmRobinXorFourSlotPairCoordinateCircuit

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitive_eval_reindexedPair :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        warmRobinXorFourSlotOriginalBitsEquiv.symm
        warmRobinXorFourSlotPairLogicalUnitary := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot original bits equiv index”; the hypotheses and conclusion in the code panel fix its exact scope. The physical pair-coordinate convention agrees with the original Robin system order and the repository-wide six-wire little-endian convention.

theorem warmRobinXorFourSlotOriginalBitsEquiv_index
    (bits : PrimitiveBasis 6) :
    warmRobinFourSlotIndexEquiv
        (warmRobinXorFourSlotOriginalBitsEquiv bits) =
      primitiveBasisLEEquiv 6 bits := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot primitive eval eq flat unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Exact T3 refinement root: the primitive '{X, RY, RZ, CX}' circuit denotes the XOR four-slot T2 unitary after the explicit little-endian reindexing.

theorem warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        (primitiveBasisLEEquiv 6).symm
        warmRobinXorFourSlotFlatUnitary := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotPrimitiveProgram : PrimitiveProgram 6 where
  circuit := warmRobinXorFourSlotPrimitiveCircuit
  globalPhase := .rational 0

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitiveProgram_eval :
    evalPrimitiveProgram warmRobinXorFourSlotPrimitiveProgram =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        (primitiveBasisLEEquiv 6).symm
        warmRobinXorFourSlotFlatUnitary := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotPrimitiveCleanIndex
    (system : Fin 8) : PrimitiveBasis 6 :=
  (primitiveBasisLEEquiv 6).symm (warmRobinFourSlotCleanIndex system)

/-- The executable primitive circuit has the required exact clean block. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot primitive clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The executable primitive circuit has the required exact clean block.

theorem warmRobinXorFourSlotPrimitive_cleanBlock (row column : Fin 8) :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit
        (warmRobinXorFourSlotPrimitiveCleanIndex row)
        (warmRobinXorFourSlotPrimitiveCleanIndex column) =
      ((RobinEvolution.warmRobinTarget row column /
        RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitive_unitary :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit ∈
      _root_.Matrix.unitaryGroup (PrimitiveBasis 6) ℂ :=
  evalPrimitiveCircuit_unitary _

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitive_noOracleCalls :
    warmRobinXorFourSlotPrimitiveProgram.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

/-- Presentation-only conversion into the repository's legacy circuit list.
The authoritative T3 semantics and resources remain those of PrimitiveCircuit. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot primitive presentation”. Presentation-only conversion into the repository's legacy circuit list.

noncomputable def warmRobinXorFourSlotPrimitivePresentation : Circuit :=
  warmRobinXorFourSlotPrimitiveCircuit.map fun gate =>
    match gate with
    | .x target => .oneQubit "X" target.val
    | .ry target _ => .rotationY target.val "exact-angle"
    | .rz target _ => .rotationZ target.val "exact-angle"
    | .cx control target _ => .cnot control.val target.val

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotPrimitiveResource : Resource :=
  warmRobinXorFourSlotPrimitiveProgram.resource

/-- Resource ownership is definitional: no handwritten gate or depth tuple is
used by the promoted candidate. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot primitive resource faithful”; the hypotheses and conclusion in the code panel fix its exact scope. Resource ownership is definitional: no handwritten gate or depth tuple is used by the promoted candidate.

theorem warmRobinXorFourSlotPrimitive_resource_faithful :
    warmRobinXorFourSlotPrimitiveResource =
      warmRobinXorFourSlotPrimitiveCircuit.resource := rfl

commit-pinned source · Verso Blueprint panel

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

def warmRobinXorFourSlotPrimitiveBlockContainsTarget : Prop :=
  ∀ row column : Fin 8,
    warmRobinXorFourSlotFlatUnitary
        (warmRobinFourSlotCleanIndex row)
        (warmRobinFourSlotCleanIndex column) =
      warmRobinQueryTarget.operator row column /
        warmRobinQueryTarget.normalizer

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotPrimitiveBlockContainsTarget_proof :
    warmRobinXorFourSlotPrimitiveBlockContainsTarget := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot primitive operator candidate”. T3 candidate whose resource row is computed from its exact primitive program.

noncomputable def warmRobinXorFourSlotPrimitiveOperatorCandidate :
    OperatorBlockEncodingCandidate ℂ 3 where
  auxiliaryQubits := 3
  target := warmRobinQueryTarget
  unitary := warmRobinXorFourSlotFlatUnitary
  layout := {
    systemQubits := 3
    signalQubits := 3
    pureAncillas := 0
  }
  circuit := warmRobinXorFourSlotPrimitivePresentation

commit-pinned source · Verso Blueprint panel

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

noncomputable def warmRobinXorFourSlotPrimitiveRefinement :
    PrimitiveRefinement 6 where
  circuit := warmRobinXorFourSlotPrimitiveCircuit
  target := _root_.Matrix.reindexAlgEquiv ℂ ℂ
    (primitiveBasisLEEquiv 6).symm warmRobinXorFourSlotFlatUnitary
  exact := warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary

/-- Exact primitive verified block encoding for the XOR evolved route. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “warm robin xor four slot primitive verified block encoding”. Exact primitive verified block encoding for the XOR evolved route.

noncomputable def warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding :
    VerifiedOperatorBlockEncoding ℂ 3 where
  candidate := warmRobinXorFourSlotPrimitiveOperatorCandidate
  unitaryProof := warmRobinXorFourSlotFlatUnitary_unitary
  blockProof := warmRobinXorFourSlotPrimitiveBlockContainsTarget_proof

/-- Dashboard-compatible names explicitly pointing to the XOR T3 route. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “warm robin four slot t 3 flat unitary”. Dashboard-compatible names explicitly pointing to the XOR T3 route.

noncomputable abbrev warmRobinFourSlotT3FlatUnitary :=
  warmRobinXorFourSlotFlatUnitary

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinFourSlotPrimitive_eval_eq_flatUnitary :
    evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit =
      _root_.Matrix.reindexAlgEquiv ℂ ℂ
        (primitiveBasisLEEquiv 6).symm
        warmRobinFourSlotT3FlatUnitary :=
  warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “warm robin four slot primitive verified block encoding”.

noncomputable abbrev warmRobinFourSlotPrimitiveVerifiedBlockEncoding :=
  warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding

commit-pinned source · Verso Blueprint panel

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

theorem warmRobinXorFourSlotAmplitudeCircuit_counts :
    warmRobinXorFourSlotAmplitudeCircuit.ryCount = 32 ∧
      warmRobinXorFourSlotAmplitudeCircuit.cxCount = 62 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “warm robin xor four slot amplitude program no oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem warmRobinXorFourSlotAmplitudeProgram_noOracleCalls :
    warmRobinXorFourSlotAmplitudeProgram.resource.oracleCalls = 0 :=
  PrimitiveCircuit.resource_oracleCalls_eq_zero _

commit-pinned source · Verso Blueprint panel