This definition gives the library's named construction or computation for “warm robin hadamard 8 index equiv”. Flatten coefficient × selector × system into the seven-qubit basis.
def warmRobinHadamard8IndexEquiv :
LCUIndex (Fin 2) (Fin 8) (Fin 8) ≃ Fin (gridSize 7) :=
(Equiv.prodCongr (Equiv.refl (Fin 2)) finProdFinEquiv).trans
finProdFinEquiv
/-- The clean coefficient/selector branch embedded in the flat seven-qubit basis. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 clean index”. The clean coefficient/selector branch embedded in the flat seven-qubit basis.
def warmRobinHadamard8CleanIndex (system : Fin 8) : Fin (gridSize 7) :=
warmRobinHadamard8IndexEquiv (0, (0, system))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 clean index value”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinHadamard8CleanIndex_value (system : Fin 8) :
(warmRobinHadamard8CleanIndex system).val = system.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 flat unitary”. The product-register logical unitary reindexed as a seven-qubit matrix.
noncomputable def warmRobinHadamard8FlatUnitary :
_root_.Matrix (Fin (gridSize 7)) (Fin (gridSize 7)) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ warmRobinHadamard8IndexEquiv
warmRobinHadamard8LogicalUnitary
/-- Reindexing preserves the exact Mathlib unitary-group certificate. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves the exact Mathlib unitary-group certificate.
theorem warmRobinHadamard8FlatUnitary_unitary :
warmRobinHadamard8FlatUnitary ∈
_root_.Matrix.unitaryGroup (Fin (gridSize 7)) ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Applying the reindexed matrix at reindexed indices recovers the product entry.
@[simp] theorem warmRobinHadamard8FlatUnitary_reindex
(row column : LCUIndex (Fin 2) (Fin 8) (Fin 8)) :
warmRobinHadamard8FlatUnitary
(warmRobinHadamard8IndexEquiv row)
(warmRobinHadamard8IndexEquiv column) =
warmRobinHadamard8LogicalUnitary row column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin uniform bit prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Every row of the one-bit PREPARE has the same clean-column amplitude.
@[simp] theorem warmRobinUniformBitPrepare_cleanColumn (bit : Fin 2) :
warmRobinUniformBitPrepare bit 0 =
((Real.sqrt 2 / 2 : Real) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard bits prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. The three-bit tensor PREPARE has a uniform clean column.
@[simp] theorem warmRobinHadamardBitsPrepare_cleanColumn
(bits : WarmRobinHadamardBits) :
warmRobinHadamardBitsPrepare bits (0, (0, 0)) =
(((Real.sqrt 2 / 2 : Real) : ℂ) *
((Real.sqrt 2 / 2 : Real) : ℂ) *
((Real.sqrt 2 / 2 : Real) : ℂ)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 selector prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. The flattened selector PREPARE still has a uniform clean column.
@[simp] theorem warmRobinHadamard8SelectorPrepare_cleanColumn (slot : Fin 8) :
warmRobinHadamard8SelectorPrepare slot 0 =
(((Real.sqrt 2 / 2 : Real) : ℂ) *
((Real.sqrt 2 / 2 : Real) : ℂ) *
((Real.sqrt 2 / 2 : Real) : ℂ)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 selector prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. Squared magnitude of each selector amplitude is exactly '1/8'.
@[simp] theorem warmRobinHadamard8SelectorPrepare_probability (slot : Fin 8) :
star (warmRobinHadamard8SelectorPrepare slot 0) *
warmRobinHadamard8SelectorPrepare slot 0 = (1 / 8 : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 coefficient complex”; the hypotheses and conclusion in the code panel fix its exact scope. Rational and real-complex views of a slot coefficient agree.
theorem warmRobinHadamard8Coefficient_complex
(slot column : Fin 8) :
(warmRobinHadamard8Coefficient slot column : ℂ) =
(warmRobinEightSlotAmplitude slot column : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable clean-entry expansion specializes to the Robin eight-slot formula.
theorem warmRobinHadamard8LogicalUnitary_cleanEntry
(row column : Fin 8) :
warmRobinHadamard8LogicalUnitary
(0, (0, row)) (0, (0, column)) =
(warmRobinHadamard8CleanFormula row column : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary clean entry eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The product-register clean entry is the normalized fixed Robin target.
theorem warmRobinHadamard8LogicalUnitary_cleanEntry_eq_target
(row column : Fin 8) :
warmRobinHadamard8LogicalUnitary
(0, (0, row)) (0, (0, column)) =
((RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The flat seven-qubit clean block is the normalized fixed Robin operator.
theorem warmRobinHadamard8FlatUnitary_cleanBlock
(row column : Fin 8) :
warmRobinHadamard8FlatUnitary
(warmRobinHadamard8CleanIndex row)
(warmRobinHadamard8CleanIndex 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 complex target”. Complex view of the fixed Robin target used by the operator-first API.
def warmRobinComplexTarget : Matrix 8 8 ℂ := fun row column =>
(RobinEvolution.warmRobinTarget row column : ℂ)
/-- Operator-first target contract for the fixed homogeneous Robin benchmark. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin query target”. Operator-first target contract for the fixed homogeneous Robin benchmark.
def warmRobinQueryTarget : QueryOperatorTarget ℂ 8 8 where
operator := warmRobinComplexTarget
normalizer := (RobinEvolution.warmRobinNormalizer : ℂ)
source := "Guseynov-Huang-Liu 2025, fixed N=8 homogeneous Robin instance"
semanticContract :=
"the coefficient=0 and selector=0 clean block equals A/(56/3) exactly"
freeParameters := []
/-- Four logical stages with the three selector Hadamards made explicit. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 schedule”. Four logical stages with the three selector Hadamards made explicit.
def warmRobinHadamard8T2Schedule : LayeredCircuit :=
[ [ Gate.oneQubit "T2 selector-H-0" 0
, Gate.oneQubit "T2 selector-H-1" 1
, Gate.oneQubit "T2 selector-H-2" 2 ]
, [ Gate.oracleCall "T2 controlled amplitude rotation" ]
, [ Gate.oracleCall "T2 SELECT permutation" ]
, [ Gate.oneQubit "T2 selector-H-0 dagger" 0
, Gate.oneQubit "T2 selector-H-1 dagger" 1
, Gate.oneQubit "T2 selector-H-2 dagger" 2 ]
]
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 circuit”. Logical gate list associated with the fair T2 schedule.
def warmRobinHadamard8T2Circuit : Circuit :=
warmRobinHadamard8T2Schedule.flatten
/-- Resource record under the logical-stage convention, not a T3 primitive count. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 resource”. Resource record under the logical-stage convention, not a T3 primitive count.
def warmRobinHadamard8T2Resource : Resource :=
warmRobinHadamard8T2Schedule.resource
/-- The exact block predicate attached to the operator candidate. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 block contains target”. The exact block predicate attached to the operator candidate.
def warmRobinHadamard8BlockContainsTarget : Prop :=
∀ row column : Fin 8,
warmRobinHadamard8FlatUnitary
(warmRobinHadamard8CleanIndex row)
(warmRobinHadamard8CleanIndex column) =
warmRobinQueryTarget.operator row column /
warmRobinQueryTarget.normalizer
/-- The clean-block predicate follows from the specialized clean-entry theorem. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin hadamard 8 block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope. The clean-block predicate follows from the specialized clean-entry theorem.
theorem warmRobinHadamard8BlockContainsTarget_proof :
warmRobinHadamard8BlockContainsTarget := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 operator candidate”. Fixed 'N=8' Hadamard-8 candidate at the exact logical-unitary tier.
noncomputable def warmRobinHadamard8OperatorCandidate :
OperatorBlockEncodingCandidate ℂ 3 where
auxiliaryQubits := 4
target := warmRobinQueryTarget
unitary := warmRobinHadamard8FlatUnitary
layout := {
systemQubits := 3
signalQubits := 4
pureAncillas := 0
}
circuit := warmRobinHadamard8T2Circuit
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 verified block encoding”. Fully verified T2 block encoding of the fixed Robin matrix.
noncomputable def warmRobinHadamard8VerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinHadamard8OperatorCandidate
unitaryProof := warmRobinHadamard8FlatUnitary_unitary
blockProof := warmRobinHadamard8BlockContainsTarget_proof
/-- Honest boundary: primitive synthesis/refinement is still a separate T3 theorem. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin hadamard 8 t 3 blocked leaf”. Honest boundary: primitive synthesis/refinement is still a separate T3 theorem.
def warmRobinHadamard8T3BlockedLeaf : String :=
"prove that a concrete primitive circuit refines warmRobinHadamard8FlatUnitary and certify its primitive resource counts"
commit-pinned source · Verso Blueprint panel