This definition gives the library's named construction or computation for “warm robin paper seven select reversible program”. Physical SELECT in the declared eight-wire order.
def warmRobinPaperSevenSelectReversibleProgram : ReversibleProgram 8 :=
[ .x 3
, .x 4
, .ccx 3 0 7 (by decide) (by decide) (by decide)
, .ccx 7 1 2 (by decide) (by decide) (by decide)
, .ccx 3 0 7 (by decide) (by decide) (by decide)
, .ccx 3 0 1 (by decide) (by decide) (by decide)
, .cx 3 0 (by decide)
, .ccx 4 1 2 (by decide) (by decide) (by decide)
, .cx 4 1 (by decide)
, .cx 5 2 (by decide)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven select basis equiv”.
def warmRobinPaperSevenSelectBasisEquiv :
PrimitiveBasis 8 ≃ PrimitiveBasis 8 :=
evalReversibleProgram warmRobinPaperSevenSelectReversibleProgram
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven system bits”.
def warmRobinPaperSevenSystemBits (bits : PrimitiveBasis 8) : Fin 8 :=
⟨(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val, by omega⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven selector bits”.
def warmRobinPaperSevenSelectorBits (bits : PrimitiveBasis 8) : Fin 8 :=
⟨(bits 3).val + 2 * (bits 4).val + 4 * (bits 5).val, by omega⟩
/-- Clean-workspace action of the source SELECT. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select program clean action”; the hypotheses and conclusion in the code panel fix its exact scope. Clean-workspace action of the source SELECT.
theorem warmRobinPaperSevenSelectProgram_cleanAction
(bits : PrimitiveBasis 8) (workClean : bits 7 = 0) :
let output := warmRobinPaperSevenSelectBasisEquiv bits
warmRobinPaperSevenSystemBits output =
warmRobinSourceDTRow (warmRobinPaperSevenSelectorBits bits)
(warmRobinPaperSevenSystemBits bits) ∧
warmRobinPaperSevenSelectorBits output =
warmRobinPaperSevenSelectorBits bits ∧
output 6 = bits 6 ∧ output 7 = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select program workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectProgram_workspaceClean
(bits : PrimitiveBasis 8) (workClean : bits 7 = 0) :
warmRobinPaperSevenSelectBasisEquiv bits 7 = 0 :=
(warmRobinPaperSevenSelectProgram_cleanAction bits workClean).2.2.2
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven select program”.
noncomputable def warmRobinPaperSevenSelectProgram : PrimitiveProgram 8 :=
compileReversibleProgram warmRobinPaperSevenSelectReversibleProgram
/-- Exact primitive matrix for source SELECT, including its exact compiler
phase. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select program eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact primitive matrix for source SELECT, including its exact compiler phase.
theorem warmRobinPaperSevenSelectProgram_eval :
evalPrimitiveProgram warmRobinPaperSevenSelectProgram =
ComplexLCU.equivPermutationMatrix
warmRobinPaperSevenSelectBasisEquiv := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select program no oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectProgram_noOracleCalls :
warmRobinPaperSevenSelectProgram.resource.oracleCalls = 0 :=
PrimitiveCircuit.resource_oracleCalls_eq_zero _
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “warm robin paper seven full system”.
abbrev WarmRobinPaperSevenFullSystem := Fin 8 × Fin 2
/-- Encode the declared register product into the physical wire order. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven encode bits”. Encode the declared register product into the physical wire order.
def warmRobinPaperSevenEncodeBits
(coefficient : Fin 2) (selector : Fin 8)
(system : WarmRobinPaperSevenFullSystem) : PrimitiveBasis 8
| ⟨0, _⟩ => primitiveBits3LE system.1 0
| ⟨1, _⟩ => primitiveBits3LE system.1 1
| ⟨2, _⟩ => primitiveBits3LE system.1 2
| ⟨3, _⟩ => primitiveBits3LE selector 0
| ⟨4, _⟩ => primitiveBits3LE selector 1
| ⟨5, _⟩ => primitiveBits3LE selector 2
| ⟨6, _⟩ => coefficient
| _ => system.2
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven bits index”.
def warmRobinPaperSevenBitsIndex (bits : PrimitiveBasis 8) :
ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinPaperSevenFullSystem :=
(bits 6, (warmRobinPaperSevenSelectorBits bits,
(warmRobinPaperSevenSystemBits bits, bits 7)))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven bits index bijective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenBitsIndex_bijective :
Function.Bijective warmRobinPaperSevenBitsIndex := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven bits equiv”.
noncomputable def warmRobinPaperSevenBitsEquiv :
PrimitiveBasis 8 ≃
ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinPaperSevenFullSystem :=
Equiv.ofBijective warmRobinPaperSevenBitsIndex
warmRobinPaperSevenBitsIndex_bijective
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven bits equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPaperSevenBitsEquiv_apply
(bits : PrimitiveBasis 8) :
warmRobinPaperSevenBitsEquiv bits = warmRobinPaperSevenBitsIndex bits := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin bit xor”.
def warmRobinBitXor (left right : Fin 2) : Fin 2 :=
⟨(left.val + right.val) % 2, by omega⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin bit and”.
def warmRobinBitAnd (left right : Fin 2) : Fin 2 :=
⟨(left.val * right.val) % 2, Nat.mod_lt _ (by decide)⟩
/-- Explicit full-space action of the reversible adder. On dirty workspace
this records the actual extension instead of claiming tensor identity. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven full system perm”. Explicit full-space action of the reversible adder.
def warmRobinPaperSevenFullSystemPerm
(slot : Fin 8) (system : WarmRobinPaperSevenFullSystem) :
WarmRobinPaperSevenFullSystem :=
let a := primitiveBits3LE system.1
let b := primitiveBits3LE (warmRobinSourceDTOffset slot)
let work1 := warmRobinBitXor system.2 (warmRobinBitAnd (b 0) (a 0))
let a2First := warmRobinBitXor (a 2) (warmRobinBitAnd work1 (a 1))
let a1First := warmRobinBitXor (a 1) (warmRobinBitAnd (b 0) (a 0))
let a0Final := warmRobinBitXor (a 0) (b 0)
let a2Second := warmRobinBitXor a2First (warmRobinBitAnd (b 1) a1First)
let a1Final := warmRobinBitXor a1First (b 1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven full system perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenFullSystemPerm_bijective (slot : Fin 8) :
Function.Bijective (warmRobinPaperSevenFullSystemPerm slot) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven full system equiv”.
noncomputable def warmRobinPaperSevenFullSystemEquiv (slot : Fin 8) :
WarmRobinPaperSevenFullSystem ≃ WarmRobinPaperSevenFullSystem :=
Equiv.ofBijective (warmRobinPaperSevenFullSystemPerm slot)
(warmRobinPaperSevenFullSystemPerm_bijective slot)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven full system equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPaperSevenFullSystemEquiv_apply
(slot : Fin 8) (system : WarmRobinPaperSevenFullSystem) :
warmRobinPaperSevenFullSystemEquiv slot system =
warmRobinPaperSevenFullSystemPerm slot system := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven full system equiv clean”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenFullSystemEquiv_clean
(slot column : Fin 8) :
warmRobinPaperSevenFullSystemEquiv slot (column, 0) =
(warmRobinSourceDTRow slot column, 0) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select basis action index”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectBasisAction_index
(bits : PrimitiveBasis 8) :
warmRobinPaperSevenBitsEquiv
(warmRobinPaperSevenSelectBasisEquiv bits) =
ComplexLCU.controlledSystemEquiv
warmRobinPaperSevenFullSystemEquiv
(warmRobinPaperSevenBitsEquiv bits) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven select program eval reindexed”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenSelectProgram_eval_reindexed :
evalPrimitiveProgram warmRobinPaperSevenSelectProgram =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
(ComplexLCU.selectLift (coefficient := Fin 2)
warmRobinPaperSevenFullSystemEquiv) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven workspace rotation”.
noncomputable def warmRobinPaperSevenWorkspaceRotation
(slot : Fin 8) (system : WarmRobinPaperSevenFullSystem) :
_root_.Matrix (Fin 2) (Fin 2) ℂ :=
warmRobinPaperSevenRotation slot system.1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven workspace rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenWorkspaceRotation_unitary
(slot : Fin 8) (system : WarmRobinPaperSevenFullSystem) :
warmRobinPaperSevenWorkspaceRotation slot system ∈
_root_.Matrix.unitaryGroup (Fin 2) ℂ :=
warmRobinPaperSevenRotation_unitary _ _
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin paper seven workspace logical unitary”.
noncomputable def warmRobinPaperSevenWorkspaceLogicalUnitary :
_root_.Matrix
(ComplexLCU.LCUIndex (Fin 2) (Fin 8)
WarmRobinPaperSevenFullSystem)
(ComplexLCU.LCUIndex (Fin 2) (Fin 8)
WarmRobinPaperSevenFullSystem) ℂ :=
ComplexLCU.prepareAmplitudeSelectUnprepare
warmRobinPaperSevenSelectorPrepare
warmRobinPaperSevenWorkspaceRotation
warmRobinPaperSevenFullSystemEquiv
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven workspace logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenWorkspaceLogicalUnitary_unitary :
warmRobinPaperSevenWorkspaceLogicalUnitary ∈
_root_.Matrix.unitaryGroup
(ComplexLCU.LCUIndex (Fin 2) (Fin 8)
WarmRobinPaperSevenFullSystem) ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin paper seven workspace logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinPaperSevenWorkspaceLogicalUnitary_cleanEntry
(row column : Fin 8) :
warmRobinPaperSevenWorkspaceLogicalUnitary
(0, (0, (row, 0))) (0, (0, (column, 0))) =
(warmRobinSourceSevenCleanFormula row column : ℂ) := by
commit-pinned source · Verso Blueprint panel