Lean checks the proposition indexed as “warm robin figure 4 indicator basis equiv clean”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinFigure4IndicatorBasisEquiv_clean
(slot column : Fin 8) (coefficient : Fin 2) :
warmRobinFigure4DTIndicatorBasisEquiv
(warmRobinFigure4TransportInput slot column coefficient 0) =
warmRobinFigure4TransportInput slot column coefficient
(warmRobinFigure4IndicatorValue column) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 bulk assignment transport input”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinFigure4BulkAssignment_transportInput
(slot column : Fin 8) (coefficient indicator : Fin 2) :
primitiveControlAssignment warmRobinFigure4BulkControlWires 6
warmRobinFigure4BulkControlWires_ne_target
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput slot column coefficient indicator)).2 =
warmRobinFigure4BulkControlInput slot indicator := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 boundary assignment transport input”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinFigure4BoundaryAssignment_transportInput
(slot column : Fin 8) (coefficient indicator : Fin 2) :
primitiveControlAssignment warmRobinFigure4BoundaryControlWires 6
warmRobinFigure4BoundaryControlWires_ne_target
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput slot column coefficient indicator)).2 =
warmRobinFigure4BoundaryControlInput slot column indicator := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 derivative loader physical clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The physical loader's clean coefficient entry is the exact source coefficient.
theorem warmRobinFigure4DerivativeLoader_physicalCleanEntry
(slot column : Fin 8) :
let input := warmRobinFigure4TransportInput slot column 0
(warmRobinFigure4IndicatorValue column)
evalPrimitiveProgram warmRobinFigure4DerivativeLoaderProgram input input =
((warmRobinFigure4SourceCoefficient slot column : Rat) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 transport input split coefficient fst”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinFigure4TransportInput_splitCoefficient_fst
(slot column : Fin 8) (coefficient indicator : Fin 2) :
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput slot column coefficient indicator)).1 =
coefficient := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 transport input split coefficient context”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4TransportInput_splitCoefficient_context
(slot column : Fin 8) (left right indicator : Fin 2) :
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput slot column left indicator)).2 =
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput slot column right indicator)).2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 transport input split coefficient context iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4TransportInput_splitCoefficient_context_iff
(leftSlot rightSlot leftColumn rightColumn : Fin 8)
(leftCoefficient rightCoefficient leftIndicator rightIndicator : Fin 2) :
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput leftSlot leftColumn
leftCoefficient leftIndicator)).2 =
(splitPrimitiveWire (6 : Fin 9)
(warmRobinFigure4TransportInput rightSlot rightColumn
rightCoefficient rightIndicator)).2 ↔
leftSlot = rightSlot ∧ leftColumn = rightColumn ∧
leftIndicator = rightIndicator := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 derivative loader entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4DerivativeLoader_entry
(coefficientRow coefficientColumn : Fin 2)
(leftSlot rightSlot leftColumn rightColumn : Fin 8) :
evalPrimitiveProgram warmRobinFigure4DerivativeLoaderProgram
(warmRobinFigure4TransportInput leftSlot leftColumn coefficientRow
(warmRobinFigure4IndicatorValue leftColumn))
(warmRobinFigure4TransportInput rightSlot rightColumn coefficientColumn
(warmRobinFigure4IndicatorValue rightColumn)) =
if leftSlot = rightSlot ∧ leftColumn = rightColumn then
ComplexLCU.amplitudeRotation
(((warmRobinFigure4SourceCoefficient rightSlot rightColumn : Rat) : Real))
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 full register swap primitive program”.
noncomputable def warmRobinFigure4FullRegisterSwapPrimitiveProgram :
PrimitiveProgram 9 :=
compileReversibleProgram warmRobinFigure4RegisterSwapReversibleProgram
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 register swap program eval full”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4RegisterSwapProgram_eval_full :
evalPrimitiveProgram warmRobinFigure4FullRegisterSwapPrimitiveProgram =
ComplexLCU.equivPermutationMatrix
warmRobinFigure4RegisterSwapFullBasisEquiv :=
compileReversibleProgram_eval _
/-- The homogeneous `f=1` stage is constant-folded to the exact identity. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 homogeneous program”. The homogeneous 'f=1' stage is constant-folded to the exact identity.
def warmRobinFigure4HomogeneousProgram : PrimitiveProgram 9 :=
PrimitiveProgram.identity 9
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 homogeneous program eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4HomogeneousProgram_eval :
evalPrimitiveProgram warmRobinFigure4HomogeneousProgram = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 post loader program”.
noncomputable def warmRobinFigure4PostLoaderProgram : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4DTSparseAccessProgram
(PrimitiveProgram.seq warmRobinFigure4DTIndicatorProgram.dagger
(PrimitiveProgram.seq warmRobinFigure4HomogeneousProgram
(PrimitiveProgram.seq warmRobinFigure4FullRegisterSwapPrimitiveProgram
warmRobinFigure4DSparseAccessProgram.dagger)))
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 post loader basis equiv”.
def warmRobinFigure4PostLoaderBasisEquiv :
PrimitiveBasis 9 ≃ PrimitiveBasis 9 :=
warmRobinFigure4DTSparseAccessBasisEquiv.trans
(warmRobinFigure4DTIndicatorBasisEquiv.symm.trans
(warmRobinFigure4RegisterSwapFullBasisEquiv.trans
warmRobinFigure4DSparseAccessBasisEquiv.symm))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 post loader program eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4PostLoaderProgram_eval :
evalPrimitiveProgram warmRobinFigure4PostLoaderProgram =
ComplexLCU.equivPermutationMatrix
warmRobinFigure4PostLoaderBasisEquiv := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 post loader clean action”; the hypotheses and conclusion in the code panel fix its exact scope. The post-loader basis permutation restores both work wires and the physical selector, while transporting the selected source row into the system register.
theorem warmRobinFigure4PostLoader_cleanAction
(slot column : Fin 8) (coefficient : Fin 2) :
warmRobinFigure4PostLoaderBasisEquiv
(warmRobinFigure4TransportInput slot column coefficient
(warmRobinFigure4IndicatorValue column)) =
warmRobinFigure4TransportInput slot
(warmRobinSourceDTRow slot column) coefficient 0 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 source dt column”.
def warmRobinFigure4SourceDTColumn (slot row : Fin 8) : Fin 8 :=
⟨(row.val + 8 - (warmRobinSourceDTOffset slot).val) % 8,
Nat.mod_lt _ (by decide)⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 source dt column inverse”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4SourceDTColumn_inverse
(slot row : Fin 8) :
warmRobinSourceDTRow slot (warmRobinFigure4SourceDTColumn slot row) = row := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 source dt column eq iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4SourceDTColumn_eq_iff
(slot row column : Fin 8) :
warmRobinFigure4SourceDTColumn slot row = column ↔
warmRobinSourceDTRow slot column = row := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 post loader inverse clean action”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4PostLoader_inverseCleanAction
(slot row : Fin 8) (coefficient : Fin 2) :
warmRobinFigure4PostLoaderBasisEquiv.symm
(warmRobinFigure4TransportInput slot row coefficient 0) =
warmRobinFigure4TransportInput slot
(warmRobinFigure4SourceDTColumn slot row) coefficient
(warmRobinFigure4IndicatorValue
(warmRobinFigure4SourceDTColumn slot row)) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 middle program”.
noncomputable def warmRobinFigure4MiddleProgram : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4DTIndicatorProgram
(PrimitiveProgram.seq warmRobinFigure4DerivativeLoaderProgram
warmRobinFigure4PostLoaderProgram)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 middle program eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4MiddleProgram_eval :
evalPrimitiveProgram warmRobinFigure4MiddleProgram =
ComplexLCU.equivPermutationMatrix warmRobinFigure4PostLoaderBasisEquiv *
evalPrimitiveProgram warmRobinFigure4DerivativeLoaderProgram *
ComplexLCU.equivPermutationMatrix
warmRobinFigure4DTIndicatorBasisEquiv := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 middle program clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4MiddleProgram_cleanEntry
(coefficientRow coefficientColumn : Fin 2)
(leftSlot rightSlot row column : Fin 8) :
evalPrimitiveProgram warmRobinFigure4MiddleProgram
(warmRobinFigure4TransportInput leftSlot row coefficientRow 0)
(warmRobinFigure4TransportInput rightSlot column coefficientColumn 0) =
if leftSlot = rightSlot ∧
warmRobinSourceDTRow rightSlot column = row then
ComplexLCU.amplitudeRotation
(((warmRobinFigure4SourceCoefficient rightSlot column : Rat) : Real))
coefficientRow coefficientColumn
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through indicator”. The post-loader basis permutation restores both work wires and the physical selector, while transporting the selected source row into the system register.
noncomputable def warmRobinFigure4ThroughIndicator : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4SelectorPrepareProgram
warmRobinFigure4DTIndicatorProgram
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after indicator”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_indicator :
evalPrimitiveProgram warmRobinFigure4ThroughIndicator =
evalPrimitiveProgram warmRobinFigure4DTIndicatorProgram *
evalPrimitiveProgram warmRobinFigure4SelectorPrepareProgram := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through derivative”.
noncomputable def warmRobinFigure4ThroughDerivative : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4ThroughIndicator
warmRobinFigure4DerivativeLoaderProgram
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after derivative loader”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_derivative_loader :
evalPrimitiveProgram warmRobinFigure4ThroughDerivative =
evalPrimitiveProgram warmRobinFigure4DerivativeLoaderProgram *
evalPrimitiveProgram warmRobinFigure4ThroughIndicator := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through dt access”.
noncomputable def warmRobinFigure4ThroughDTAccess : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4ThroughDerivative
warmRobinFigure4DTSparseAccessProgram
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after dt sparse access”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_DT_sparse_access :
evalPrimitiveProgram warmRobinFigure4ThroughDTAccess =
evalPrimitiveProgram warmRobinFigure4DTSparseAccessProgram *
evalPrimitiveProgram warmRobinFigure4ThroughDerivative := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through indicator cleanup”.
noncomputable def warmRobinFigure4ThroughIndicatorCleanup : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4ThroughDTAccess
warmRobinFigure4DTIndicatorProgram.dagger
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after indicator cleanup”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_indicator_cleanup :
evalPrimitiveProgram warmRobinFigure4ThroughIndicatorCleanup =
evalPrimitiveProgram warmRobinFigure4DTIndicatorProgram.dagger *
evalPrimitiveProgram warmRobinFigure4ThroughDTAccess := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through swap”.
noncomputable def warmRobinFigure4ThroughSwap : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4ThroughIndicatorCleanup
warmRobinFigure4FullRegisterSwapPrimitiveProgram
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after swap”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_swap :
evalPrimitiveProgram warmRobinFigure4ThroughSwap =
evalPrimitiveProgram warmRobinFigure4FullRegisterSwapPrimitiveProgram *
evalPrimitiveProgram warmRobinFigure4ThroughIndicatorCleanup := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 through transported cleanup”.
noncomputable def warmRobinFigure4ThroughTransportedCleanup : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4ThroughSwap
warmRobinFigure4DSparseAccessProgram.dagger
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 after transported cleanup”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4_after_transported_cleanup :
evalPrimitiveProgram warmRobinFigure4ThroughTransportedCleanup =
evalPrimitiveProgram warmRobinFigure4DSparseAccessProgram.dagger *
evalPrimitiveProgram warmRobinFigure4ThroughSwap := by
commit-pinned source · Verso Blueprint panel