This definition gives the library's named construction or computation for “warm robin paper seven selector high matrix”.
noncomputable def warmRobinPaperSevenSelectorHighMatrix :
_root_.Matrix (Fin 8) (Fin 8) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 3)
(evalPrimitiveGate (.ry (2 : Fin 3) warmRobinUniformSevenHighAngle))
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven selector middle matrix”.
noncomputable def warmRobinPaperSevenSelectorMiddleMatrix :
_root_.Matrix (Fin 8) (Fin 8) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 3)
(controlledRyBlockMatrix warmRobinUniformSevenMiddleWires 1
warmRobinUniformSevenMiddleWires_ne_target
warmRobinUniformSevenMiddleAngles)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven selector low matrix”.
noncomputable def warmRobinPaperSevenSelectorLowMatrix :
_root_.Matrix (Fin 8) (Fin 8) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 3)
(controlledRyBlockMatrix warmRobinUniformSevenLowWires 0
warmRobinUniformSevenLowWires_ne_target warmRobinUniformSevenLowAngles)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven selector stages eq prepare”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectorStages_eq_prepare :
warmRobinPaperSevenSelectorLowMatrix *
(warmRobinPaperSevenSelectorMiddleMatrix *
warmRobinPaperSevenSelectorHighMatrix) =
warmRobinPaperSevenSelectorPrepare := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven middle physical wires”.
def warmRobinPaperSevenMiddlePhysicalWires : Fin 1 → Fin 8 := fun _ => 5
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven middle physical wires ne target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenMiddlePhysicalWires_ne_target
(wire : Fin 1) :
warmRobinPaperSevenMiddlePhysicalWires wire ≠ (4 : Fin 8) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven low physical wires”.
def warmRobinPaperSevenLowPhysicalWires : Fin 2 → Fin 8
| 0 => 4
| _ => 5
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven low physical wires ne target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenLowPhysicalWires_ne_target
(wire : Fin 2) :
warmRobinPaperSevenLowPhysicalWires wire ≠ (3 : Fin 8) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven selector bits decode”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPaperSevenSelectorBits_decode
(bits : PrimitiveBasis 8) (wire : Fin 3) :
primitiveBits3LE (warmRobinPaperSevenSelectorBits bits) wire =
bits ⟨wire.val + 3, by omega⟩ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven high context iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenHighContext_iff
(row column : PrimitiveBasis 8) :
(splitPrimitiveWire (5 : Fin 8) row).2 =
(splitPrimitiveWire (5 : Fin 8) column).2 ↔
row 6 = column 6 ∧
(splitPrimitiveWire (2 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits row))).2 =
(splitPrimitiveWire (2 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits column))).2 ∧
(warmRobinPaperSevenSystemBits row, row 7) =
(warmRobinPaperSevenSystemBits column, column 7) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven high physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenHighPhysical_eval :
evalPrimitiveGate (.ry (5 : Fin 8) warmRobinUniformSevenHighAngle) =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinPaperSevenFullSystem)
warmRobinPaperSevenSelectorHighMatrix) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven middle context iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenMiddleContext_iff
(row column : PrimitiveBasis 8) :
(splitPrimitiveWire (4 : Fin 8) row).2 =
(splitPrimitiveWire (4 : Fin 8) column).2 ↔
row 6 = column 6 ∧
(splitPrimitiveWire (1 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits row))).2 =
(splitPrimitiveWire (1 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits column))).2 ∧
(warmRobinPaperSevenSystemBits row, row 7) =
(warmRobinPaperSevenSystemBits column, column 7) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven middle physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenMiddlePhysical_eval :
controlledRyBlockMatrix warmRobinPaperSevenMiddlePhysicalWires 4
warmRobinPaperSevenMiddlePhysicalWires_ne_target
warmRobinUniformSevenMiddleAngles =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinPaperSevenFullSystem)
warmRobinPaperSevenSelectorMiddleMatrix) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven low context iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenLowContext_iff
(row column : PrimitiveBasis 8) :
(splitPrimitiveWire (3 : Fin 8) row).2 =
(splitPrimitiveWire (3 : Fin 8) column).2 ↔
row 6 = column 6 ∧
(splitPrimitiveWire (0 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits row))).2 =
(splitPrimitiveWire (0 : Fin 3)
(primitiveBits3LE (warmRobinPaperSevenSelectorBits column))).2 ∧
(warmRobinPaperSevenSystemBits row, row 7) =
(warmRobinPaperSevenSystemBits column, column 7) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven low physical eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenLowPhysical_eval :
controlledRyBlockMatrix warmRobinPaperSevenLowPhysicalWires 3
warmRobinPaperSevenLowPhysicalWires_ne_target
warmRobinUniformSevenLowAngles =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinPaperSevenFullSystem)
warmRobinPaperSevenSelectorLowMatrix) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven selector prepare circuit”.
noncomputable def warmRobinPaperSevenSelectorPrepareCircuit :
PrimitiveCircuit 8 :=
[.ry 5 warmRobinUniformSevenHighAngle] ++
compileUniformlyControlledRy 1 warmRobinPaperSevenMiddlePhysicalWires 4
warmRobinPaperSevenMiddlePhysicalWires_ne_target
warmRobinUniformSevenMiddleAngles ++
compileUniformlyControlledRy 2 warmRobinPaperSevenLowPhysicalWires 3
warmRobinPaperSevenLowPhysicalWires_ne_target
warmRobinUniformSevenLowAngles
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven selector prepare circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectorPrepareCircuit_eval :
evalPrimitiveCircuit warmRobinPaperSevenSelectorPrepareCircuit =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinPaperSevenFullSystem)
warmRobinPaperSevenSelectorPrepare) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven selector unprepare circuit”.
noncomputable def warmRobinPaperSevenSelectorUnprepareCircuit : PrimitiveCircuit 8 :=
warmRobinPaperSevenSelectorPrepareCircuit.reverse.map PrimitiveGate.dagger
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven selector unprepare circuit eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectorUnprepareCircuit_eval :
evalPrimitiveCircuit warmRobinPaperSevenSelectorUnprepareCircuit =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(star (ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinPaperSevenFullSystem)
warmRobinPaperSevenSelectorPrepare)) := by
commit-pinned source · Verso Blueprint panel