This definition gives the library's named construction or computation for “warm robin pair system to original”. Map a reversal-pair coordinate back to the original 'Fin 8' basis.
def warmRobinPairSystemToOriginal
(index : WarmRobinSymmetrySystem) : Fin 8 :=
if index.1.val = 0 then
warmRobinPairLow index.2
else
warmRobinPairHigh index.2
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair system to original zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairSystemToOriginal_zero (pair : Fin 4) :
warmRobinPairSystemToOriginal (0, pair) = warmRobinPairLow pair := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair system to original one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairSystemToOriginal_one (pair : Fin 4) :
warmRobinPairSystemToOriginal (1, pair) = warmRobinPairHigh pair := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair system to original bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Pair coordinates enumerate the original eight basis states exactly once.
theorem warmRobinPairSystemToOriginal_bijective :
Function.Bijective warmRobinPairSystemToOriginal := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin pair system equiv”. Equivalence between pair coordinates and the original Robin basis.
noncomputable def warmRobinPairSystemEquiv :
WarmRobinSymmetrySystem ≃ Fin 8 :=
Equiv.ofBijective warmRobinPairSystemToOriginal
warmRobinPairSystemToOriginal_bijective
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair system equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairSystemEquiv_apply
(index : WarmRobinSymmetrySystem) :
warmRobinPairSystemEquiv index = warmRobinPairSystemToOriginal index := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair system to original symm”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairSystemToOriginal_symm (system : Fin 8) :
warmRobinPairSystemToOriginal (warmRobinPairSystemEquiv.symm system) = system := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin symmetry basis change”. The symmetry-sector-to-pair basis change: one exact Hadamard-like rotation.
noncomputable def warmRobinSymmetryBasisChange :
_root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem ℂ :=
warmRobinUniformBitPrepare ⊗ₖ
(1 : _root_.Matrix (Fin 4) (Fin 4) ℂ)
/-- The symmetry basis change is unitary. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin symmetry basis change unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The symmetry basis change is unitary.
theorem warmRobinSymmetryBasisChange_unitary :
warmRobinSymmetryBasisChange ∈
_root_.Matrix.unitaryGroup WarmRobinSymmetrySystem ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “star warm robin uniform bit prepare apply”; the hypotheses and conclusion in the code panel fix its exact scope. Every entry of the real two-dimensional basis change is self-conjugate.
@[simp] theorem star_warmRobinUniformBitPrepare_apply
(row column : Fin 2) :
star (warmRobinUniformBitPrepare row column) =
warmRobinUniformBitPrepare row column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin uniform scalar square complex”; the hypotheses and conclusion in the code panel fix its exact scope. The common real selector amplitude has squared magnitude '1/2'.
@[simp] theorem warmRobinUniformScalar_square_complex :
(((Real.sqrt 2 / 2 : Real) : ℂ) *
((Real.sqrt 2 / 2 : Real) : ℂ)) = (1 / 2 : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin symmetry basis change apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the exact symmetry basis change.
@[simp] theorem warmRobinSymmetryBasisChange_apply
(row column : WarmRobinSymmetrySystem) :
warmRobinSymmetryBasisChange row column =
if row.2 = column.2 then
warmRobinUniformBitPrepare row.1 column.1
else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “star warm robin symmetry basis change apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the adjoint symmetry basis change.
@[simp] theorem star_warmRobinSymmetryBasisChange_apply
(row column : WarmRobinSymmetrySystem) :
star warmRobinSymmetryBasisChange row column =
if row.2 = column.2 then
star (warmRobinUniformBitPrepare column.1 row.1)
else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin symmetry basis change mul pair row”; the hypotheses and conclusion in the code panel fix its exact scope. Left multiplication preserves the pair index and sums only over sectors.
theorem warmRobinSymmetryBasisChange_mul_pairRow
{columnType : Type*} [Fintype columnType]
(operator : _root_.Matrix WarmRobinSymmetrySystem columnType ℂ)
(rowSide : Fin 2) (rowPair : Fin 4) (column : columnType) :
(warmRobinSymmetryBasisChange * operator)
(rowSide, rowPair) column =
∑ side : Fin 2,
warmRobinUniformBitPrepare rowSide side *
operator (side, rowPair) column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “mul star warm robin symmetry basis change pair column”; the hypotheses and conclusion in the code panel fix its exact scope. Right multiplication by the adjoint also preserves the pair index.
theorem mul_star_warmRobinSymmetryBasisChange_pairColumn
{rowType : Type*} [Fintype rowType]
(operator : _root_.Matrix rowType WarmRobinSymmetrySystem ℂ)
(row : rowType) (columnSide : Fin 2) (columnPair : Fin 4) :
(operator * star warmRobinSymmetryBasisChange)
row (columnSide, columnPair) =
∑ side : Fin 2,
operator row (side, columnPair) *
star (warmRobinUniformBitPrepare columnSide side) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin integer target pair high low”; the hypotheses and conclusion in the code panel fix its exact scope. Lower-left pair block equals the upper-right pair block by centrosymmetry.
theorem warmRobinIntegerTarget_pair_high_low
(row column : Fin 4) :
warmRobinIntegerTarget (warmRobinPairHigh row) (warmRobinPairLow column) =
warmRobinIntegerTarget (warmRobinPairLow row) (warmRobinPairHigh column) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin integer target pair high high”; the hypotheses and conclusion in the code panel fix its exact scope. The high-high pair block equals the low-low block.
theorem warmRobinIntegerTarget_pair_high_high
(row column : Fin 4) :
warmRobinIntegerTarget (warmRobinPairHigh row) (warmRobinPairHigh column) =
warmRobinIntegerTarget (warmRobinPairLow row) (warmRobinPairLow column) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin pair normalized target rat”. The fixed integer target, reordered by reversal pairs and divided by '224'.
def warmRobinPairNormalizedTargetRat :
_root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem Rat :=
fun row column =>
warmRobinIntegerTargetRat
(warmRobinPairSystemToOriginal row)
(warmRobinPairSystemToOriginal column) / 224
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair normalized target rat zero zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairNormalizedTargetRat_zero_zero
(row column : Fin 4) :
warmRobinPairNormalizedTargetRat (0, row) (0, column) =
(warmRobinIntegerTarget
(warmRobinPairLow row) (warmRobinPairLow column) : Rat) / 224 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair normalized target rat zero one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairNormalizedTargetRat_zero_one
(row column : Fin 4) :
warmRobinPairNormalizedTargetRat (0, row) (1, column) =
(warmRobinIntegerTarget
(warmRobinPairLow row) (warmRobinPairHigh column) : Rat) / 224 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair normalized target rat one zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairNormalizedTargetRat_one_zero
(row column : Fin 4) :
warmRobinPairNormalizedTargetRat (1, row) (0, column) =
(warmRobinIntegerTarget
(warmRobinPairLow row) (warmRobinPairHigh column) : Rat) / 224 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair normalized target rat one one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinPairNormalizedTargetRat_one_one
(row column : Fin 4) :
warmRobinPairNormalizedTargetRat (1, row) (1, column) =
(warmRobinIntegerTarget
(warmRobinPairLow row) (warmRobinPairLow column) : Rat) / 224 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin pair normalized target complex”. Complex view of the pair-ordered normalized Robin target.
def warmRobinPairNormalizedTargetComplex :
_root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem ℂ :=
fun row column => (warmRobinPairNormalizedTargetRat row column : ℂ)
/-- Complex view of the direct-sum sector target. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot sector target complex”. Complex view of the direct-sum sector target.
def warmRobinFourSlotSectorTargetComplex :
_root_.Matrix WarmRobinSymmetrySystem WarmRobinSymmetrySystem ℂ :=
fun row column => (warmRobinFourSlotSectorTarget row column : ℂ)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin symmetry basis change conjugates target”; the hypotheses and conclusion in the code panel fix its exact scope. The exact symmetry transform reconstructs the pair-ordered Robin matrix.
theorem warmRobinSymmetryBasisChange_conjugates_target :
warmRobinSymmetryBasisChange *
(warmRobinFourSlotSectorTargetComplex *
star warmRobinSymmetryBasisChange) =
warmRobinPairNormalizedTargetComplex := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot pair logical unitary”. Conjugate the sector logical unitary back to reversal-pair coordinates.
noncomputable def warmRobinFourSlotPairLogicalUnitary :
_root_.Matrix
(LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem)
(LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ :=
conjugateSystem warmRobinSymmetryBasisChange
warmRobinFourSlotMiddleLogicalUnitary
/-- The pair-basis logical unitary remains exactly unitary. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot pair logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The pair-basis logical unitary remains exactly unitary.
theorem warmRobinFourSlotPairLogicalUnitary_unitary :
warmRobinFourSlotPairLogicalUnitary ∈
_root_.Matrix.unitaryGroup
(LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot pair logical unitary clean system block”; the hypotheses and conclusion in the code panel fix its exact scope. Its clean system block is the pair-ordered normalized Robin target.
theorem warmRobinFourSlotPairLogicalUnitary_cleanSystemBlock :
cleanSystemBlock warmRobinFourSlotPairLogicalUnitary 0 0 =
warmRobinPairNormalizedTargetComplex := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot pair logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Entry form of the pair-basis clean-block certificate.
theorem warmRobinFourSlotPairLogicalUnitary_cleanEntry
(row column : WarmRobinSymmetrySystem) :
warmRobinFourSlotPairLogicalUnitary
(0, (0, row)) (0, (0, column)) =
warmRobinPairNormalizedTargetComplex row column := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot product system equiv”. Reindex only the system component from pair order to original 'Fin 8'.
noncomputable def warmRobinFourSlotProductSystemEquiv :
LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem ≃
LCUIndex (Fin 2) (Fin 4) (Fin 8) :=
Equiv.prodCongr (Equiv.refl (Fin 2))
(Equiv.prodCongr (Equiv.refl (Fin 4)) warmRobinPairSystemEquiv)
/-- Flatten coefficient × selector × original system into six qubits. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot original index equiv”. Flatten coefficient × selector × original system into six qubits.
def warmRobinFourSlotOriginalIndexEquiv :
LCUIndex (Fin 2) (Fin 4) (Fin 8) ≃ Fin (gridSize 6) :=
(Equiv.prodCongr (Equiv.refl (Fin 2)) finProdFinEquiv).trans
finProdFinEquiv
/-- The six primitive wires interpreted as coefficient, selector, and system
registers through the already-certified T2 flattening. Consequently q0--q2
are system, q3--q4 are selector, and q5 is coefficient. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot product bits equiv”. The six primitive wires interpreted as coefficient, selector, and system registers through the already-certified T2 flattening.
def warmRobinFourSlotProductBitsEquiv :
PrimitiveBasis 6 ≃ LCUIndex (Fin 2) (Fin 4) (Fin 8) :=
(primitiveBasisLEEquiv 6).trans warmRobinFourSlotOriginalIndexEquiv.symm
/-- Primitive little-endian indexing is exactly the original T2 index map. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot product bits equiv index”; the hypotheses and conclusion in the code panel fix its exact scope. Primitive little-endian indexing is exactly the original T2 index map.
theorem warmRobinFourSlotProductBitsEquiv_index (bits : PrimitiveBasis 6) :
warmRobinFourSlotOriginalIndexEquiv
(warmRobinFourSlotProductBitsEquiv bits) =
primitiveBasisLEEquiv 6 bits := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot product bits equiv all basis”; the hypotheses and conclusion in the code panel fix its exact scope. Regression over all 64 basis states, stated as the concrete register formula consumed by executable backends.
theorem warmRobinFourSlotProductBitsEquiv_all_basis :
∀ bits : PrimitiveBasis 6,
(warmRobinFourSlotOriginalIndexEquiv
(warmRobinFourSlotProductBitsEquiv bits)).val =
(bits 0).val + 2 * (bits 1).val + 4 * (bits 2).val +
8 * (bits 3).val + 16 * (bits 4).val + 32 * (bits 5).val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot index equiv”. Combined system reindexing and six-qubit flattening.
noncomputable def warmRobinFourSlotIndexEquiv :
LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem ≃
Fin (gridSize 6) :=
warmRobinFourSlotProductSystemEquiv.trans
warmRobinFourSlotOriginalIndexEquiv
/-- Flat clean index for an original Robin system basis state. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot clean index”. Flat clean index for an original Robin system basis state.
noncomputable def warmRobinFourSlotCleanIndex (system : Fin 8) : Fin (gridSize 6) :=
warmRobinFourSlotIndexEquiv
(0, (0, warmRobinPairSystemEquiv.symm system))
/-- Six-qubit matrix in the original system order. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot flat unitary”. Six-qubit matrix in the original system order.
noncomputable def warmRobinFourSlotFlatUnitary :
_root_.Matrix (Fin (gridSize 6)) (Fin (gridSize 6)) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinFourSlotIndexEquiv
warmRobinFourSlotPairLogicalUnitary
/-- Reindexing preserves exact unitarity. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves exact unitarity.
theorem warmRobinFourSlotFlatUnitary_unitary :
warmRobinFourSlotFlatUnitary ∈
_root_.Matrix.unitaryGroup (Fin (gridSize 6)) ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot flat unitary reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Applying the flat matrix at flattened indices recovers the product entry.
@[simp] theorem warmRobinFourSlotFlatUnitary_reindex
(row column :
LCUIndex (Fin 2) (Fin 4) WarmRobinSymmetrySystem) :
warmRobinFourSlotFlatUnitary
(warmRobinFourSlotIndexEquiv row)
(warmRobinFourSlotIndexEquiv column) =
warmRobinFourSlotPairLogicalUnitary row column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin pair normalized target complex symm”; the hypotheses and conclusion in the code panel fix its exact scope. Pair-ordered target at inverse-reindexed indices is the original target.
theorem warmRobinPairNormalizedTargetComplex_symm
(row column : Fin 8) :
warmRobinPairNormalizedTargetComplex
(warmRobinPairSystemEquiv.symm row)
(warmRobinPairSystemEquiv.symm column) =
((warmRobinIntegerTargetRat row column / 224 : Rat) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The flat clean block is exactly the original fixed Robin target.
theorem warmRobinFourSlotFlatUnitary_cleanBlock
(row column : Fin 8) :
warmRobinFourSlotFlatUnitary
(warmRobinFourSlotCleanIndex row)
(warmRobinFourSlotCleanIndex 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 four slot t 2 schedule”. Fair T2 logical-stage schedule for the four-slot construction.
def warmRobinFourSlotT2Schedule : LayeredCircuit :=
[ [ Gate.oneQubit "T2 selector-H-0" 0
, Gate.oneQubit "T2 selector-H-1" 1
, Gate.oneQubit "T2 symmetry-basis-change" 3 ]
, [ Gate.oracleCall "T2 controlled amplitude rotation" ]
, [ Gate.oracleCall "T2 sector-preserving SELECT" ]
, [ Gate.oneQubit "T2 selector-H-0 dagger" 0
, Gate.oneQubit "T2 selector-H-1 dagger" 1
, Gate.oneQubit "T2 symmetry-basis-change dagger" 3 ]
]
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot t 2 circuit”. The corresponding logical gate list.
def warmRobinFourSlotT2Circuit : Circuit :=
warmRobinFourSlotT2Schedule.flatten
/-- Exact resource row under the declared T2 logical-stage convention. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot t 2 resource”. Exact resource row under the declared T2 logical-stage convention.
def warmRobinFourSlotT2Resource : Resource :=
warmRobinFourSlotT2Schedule.resource
/-- The operator-first clean-block predicate for the four-slot route. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot block contains target”. The operator-first clean-block predicate for the four-slot route.
def warmRobinFourSlotBlockContainsTarget : Prop :=
∀ row column : Fin 8,
warmRobinFourSlotFlatUnitary
(warmRobinFourSlotCleanIndex row)
(warmRobinFourSlotCleanIndex column) =
warmRobinQueryTarget.operator row column /
warmRobinQueryTarget.normalizer
/-- The clean-block predicate is discharged by the original-basis theorem. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope. The clean-block predicate is discharged by the original-basis theorem.
theorem warmRobinFourSlotBlockContainsTarget_proof :
warmRobinFourSlotBlockContainsTarget := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot operator candidate”. Four-slot T2 candidate for the fixed 'N=8' Robin target.
noncomputable def warmRobinFourSlotOperatorCandidate :
OperatorBlockEncodingCandidate ℂ 3 where
auxiliaryQubits := 3
target := warmRobinQueryTarget
unitary := warmRobinFourSlotFlatUnitary
layout := {
systemQubits := 3
signalQubits := 3
pureAncillas := 0
}
circuit := warmRobinFourSlotT2Circuit
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot verified block encoding”. Fully verified T2 block encoding for the four-slot symmetry route.
noncomputable def warmRobinFourSlotVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinFourSlotOperatorCandidate
unitaryProof := warmRobinFourSlotFlatUnitary_unitary
blockProof := warmRobinFourSlotBlockContainsTarget_proof
/-- Under one T2 logical-stage convention, four slots strictly improve the
Hadamard-8 route: gate count and depth tie, while the clean layout uses one
fewer auxiliary qubit. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin four slot t 2 cost better than hadamard 8”; the hypotheses and conclusion in the code panel fix its exact scope. Under one T2 logical-stage convention, four slots strictly improve the Hadamard-8 route: gate count and depth tie, while the clean layout uses one fewer auxiliary qubit.
theorem warmRobinFourSlotT2Cost_betterThan_hadamard8 :
warmRobinFourSlotOperatorCandidate.cost.betterThan
warmRobinHadamard8OperatorCandidate.cost := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin four slot t 3 blocked leaf”. Honest boundary: primitive synthesis and refinement remain a T3 obligation.
def warmRobinFourSlotT3BlockedLeaf : String :=
"prove that a concrete primitive circuit refines warmRobinFourSlotFlatUnitary and certify its primitive resource counts"
commit-pinned source · Verso Blueprint panel