This definition gives the library's named construction or computation for “warm robin figure 4 primitive program”.
noncomputable def warmRobinFigure4PrimitiveProgram : PrimitiveProgram 9 :=
PrimitiveProgram.seq warmRobinFigure4SelectorPrepareProgram
(PrimitiveProgram.seq warmRobinFigure4MiddleProgram
warmRobinFigure4SelectorPrepareProgram.dagger)
/-- Both Figure-4 work wires return clean on every selector/system branch.
The coefficient loader may superpose `q6`, but it does not alter this classical
context, so the statement is quantified over both coefficient basis values. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 all workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. Both Figure-4 work wires return clean on every selector/system branch.
theorem warmRobinFigure4AllWorkspaceClean
(slot column : Fin 8) (coefficient : Fin 2) :
let afterIndicator := warmRobinFigure4DTIndicatorBasisEquiv
(warmRobinFigure4TransportInput slot column coefficient 0)
let output := warmRobinFigure4PostLoaderBasisEquiv afterIndicator
output 7 = 0 ∧ output 8 = 0 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 logical middle”.
noncomputable def warmRobinFigure4LogicalMiddle :
_root_.Matrix
(ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinFigure4FullSystem)
(ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinFigure4FullSystem) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFigure4BitsEquiv
(evalPrimitiveProgram warmRobinFigure4MiddleProgram)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 logical middle apply”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4LogicalMiddle_apply
(row column :
ComplexLCU.LCUIndex (Fin 2) (Fin 8) WarmRobinFigure4FullSystem) :
warmRobinFigure4LogicalMiddle row column =
evalPrimitiveProgram warmRobinFigure4MiddleProgram
(warmRobinFigure4BitsEquiv.symm row)
(warmRobinFigure4BitsEquiv.symm column) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 logical middle clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4LogicalMiddle_cleanEntry
(coefficientRow coefficientColumn : Fin 2)
(leftSlot rightSlot row column : Fin 8) :
warmRobinFigure4LogicalMiddle
(coefficientRow, (leftSlot, (row, (0, 0))))
(coefficientColumn, (rightSlot, (column, (0, 0)))) =
if leftSlot = rightSlot ∧
warmRobinSourceDTRow rightSlot column = row then
ComplexLCU.amplitudeRotation
(((warmRobinFigure4SourceCoefficient rightSlot column : Rat) : Real))
coefficientRow coefficientColumn
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 primitive eval eq logical”; the hypotheses and conclusion in the code panel fix its exact scope. Exact physical-program semantics, including all macro compiler phases.
theorem warmRobinFigure4Primitive_eval_eq_logical :
evalPrimitiveProgram warmRobinFigure4PrimitiveProgram =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinFigure4BitsEquiv.symm
(star (ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) *
warmRobinFigure4LogicalMiddle *
ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 logical clean entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4Logical_cleanEntry (row column : Fin 8) :
(star (ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) *
warmRobinFigure4LogicalMiddle *
ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare)
(0, (0, (row, (0, 0))))
(0, (0, (column, (0, 0)))) =
(warmRobinSourceSevenCleanFormula row column : ℂ) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive flat unitary”.
noncomputable def warmRobinFigure4PrimitiveFlatUnitary :
_root_.Matrix (Fin (gridSize 9)) (Fin (gridSize 9)) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv 9)
(evalPrimitiveProgram warmRobinFigure4PrimitiveProgram)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 primitive circuit unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4PrimitiveCircuit_unitary :
warmRobinFigure4PrimitiveFlatUnitary ∈
_root_.Matrix.unitaryGroup (Fin (gridSize 9)) ℂ := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive clean index”.
noncomputable def warmRobinFigure4PrimitiveCleanIndex
(system : Fin 8) : Fin (gridSize 9) :=
primitiveBasisLEEquiv 9
(warmRobinFigure4TransportInput 0 system 0 0)
/-- Required whole-circuit clean entry; this is symbolic, not numerical. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 primitive circuit clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Required whole-circuit clean entry; this is symbolic, not numerical.
theorem warmRobinFigure4PrimitiveCircuit_cleanEntry (row column : Fin 8) :
warmRobinFigure4PrimitiveFlatUnitary
(warmRobinFigure4PrimitiveCleanIndex row)
(warmRobinFigure4PrimitiveCleanIndex column) =
(warmRobinSourceSevenCleanFormula row column : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 primitive circuit clean block”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4PrimitiveCircuit_cleanBlock (row column : Fin 8) :
warmRobinFigure4PrimitiveFlatUnitary
(warmRobinFigure4PrimitiveCleanIndex row)
(warmRobinFigure4PrimitiveCleanIndex 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 figure 4 primitive block contains target”.
def warmRobinFigure4PrimitiveBlockContainsTarget : Prop :=
∀ row column : Fin 8,
warmRobinFigure4PrimitiveFlatUnitary
(warmRobinFigure4PrimitiveCleanIndex row)
(warmRobinFigure4PrimitiveCleanIndex column) =
warmRobinQueryTarget.operator row column /
warmRobinQueryTarget.normalizer
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin figure 4 primitive block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinFigure4PrimitiveBlockContainsTarget_proof :
warmRobinFigure4PrimitiveBlockContainsTarget := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive presentation”.
noncomputable def warmRobinFigure4PrimitivePresentation : Circuit :=
warmRobinFigure4PrimitiveProgram.circuit.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 figure 4 primitive resource”.
noncomputable def warmRobinFigure4PrimitiveResource : Resource :=
warmRobinFigure4PrimitiveProgram.resource
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive operator candidate”.
noncomputable def warmRobinFigure4PrimitiveOperatorCandidate :
OperatorBlockEncodingCandidate ℂ 3 where
auxiliaryQubits := 6
target := warmRobinQueryTarget
unitary := warmRobinFigure4PrimitiveFlatUnitary
layout := {
systemQubits := 3
signalQubits := 4
pureAncillas := 2
}
circuit := warmRobinFigure4PrimitivePresentation
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive refinement”.
noncomputable def warmRobinFigure4PrimitiveRefinement :
PrimitiveProgramRefinement 9 where
program := warmRobinFigure4PrimitiveProgram
target := _root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinFigure4BitsEquiv.symm
(star (ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) *
warmRobinFigure4LogicalMiddle *
ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin figure 4 primitive verified block encoding”. Fixed-N8, f=1, standard-RY-corrected Figure-4 realization.
noncomputable def warmRobinFigure4PrimitiveVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinFigure4PrimitiveOperatorCandidate
unitaryProof := warmRobinFigure4PrimitiveCircuit_unitary
blockProof := warmRobinFigure4PrimitiveBlockContainsTarget_proof
commit-pinned source · Verso Blueprint panel