This definition gives the library's named construction or computation for “warm robin target”. The fixed eight-dimensional homogeneous-Robin benchmark matrix.
def warmRobinTarget : Matrix 8 8 Rat := fun i j =>
match i.val, j.val with
| 0, 0 => -5 / 2
| 0, 1 => 8 / 3
| 0, 2 => -1 / 6
| 1, 0 => 4 / 3
| 1, 1 => -31 / 12
| 1, 2 => 4 / 3
| 1, 3 => -1 / 12
| 2, 0 => -1 / 12
| 2, 1 => 4 / 3
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin normalizer”. Exact normalizer frozen by the warm/cold comparison contract.
def warmRobinNormalizer : Rat := 56 / 3
/-- The clean signal basis index is zero. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin clean signal index”. The clean signal basis index is zero.
def warmRobinCleanSignalIndex : Nat := 0
/-- Signal-first flattening of a signal index and an eight-dimensional system index. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin signal first index”. Signal-first flattening of a signal index and an eight-dimensional system index.
def warmRobinSignalFirstIndex (signal : Nat) (system : Fin 8) : Nat :=
signal * 8 + system.val
/-- Evaluating the symbolic Robin stencil at homogeneous boundary data gives
the fixed rational benchmark entrywise. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin target eq eval robin derivative matrix”; the hypotheses and conclusion in the code panel fix its exact scope. Evaluating the symbolic Robin stencil at homogeneous boundary data gives the fixed rational benchmark entrywise.
theorem warmRobinTarget_eq_eval_robinDerivativeMatrix :
warmRobinTarget = fun i j =>
Coeff.evalWith (fun _ => 0)
(Examples.RobinHeat.robinDerivativeMatrix 3 i j) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin target eq paper eq 9 dimensionless a 1 b 1 zero”; the hypotheses and conclusion in the code panel fix its exact scope. Relation to Guseynov--Huang--Liu Eq.
theorem warmRobinTarget_eq_paperEq9_dimensionless_A1_B1_zero :
warmRobinTarget = fun i j =>
Coeff.evalWith (fun _ => 0)
(Examples.RobinHeat.robinDerivativeMatrix 3 i j) :=
warmRobinTarget_eq_eval_robinDerivativeMatrix
/-! ## Source-ordered warm circuit adapter
These declarations expose the paper-facing ten-block transcript and its fixed
`n = 3` register arithmetic. They do not assign matrices to the transcript
labels or prove oracle cleanup, unitarity, or block correctness.
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin parameters”. Fixed paper-seeded parameters for the eight-dimensional warm instance.
def warmRobinParameters : GHL2025.OneTermRobinParameters :=
Examples.RobinHeat.oneTermParameters 3
/-- The theorem-level register layout specialized to the warm instance. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin source layout”. The theorem-level register layout specialized to the warm instance.
def warmRobinSourceLayout : RegisterLayout :=
GHL2025.oneTermRobinLayout warmRobinParameters
/-- The visible source register partition specialized to the warm instance. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin visible partition”. The visible source register partition specialized to the warm instance.
def warmRobinVisiblePartition : GHL2025.RobinRegisterPartition :=
GHL2025.defaultRobinRegisterPartition warmRobinParameters
/-- The source-ordered ten-label paper transcript for the warm instance.
The register SWAP remains a label here; executable semantics live in
`Robin.SourceBaseline.warmRobinRegisterSwapCircuit`. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin source circuit”. The source-ordered ten-label paper transcript for the warm instance.
def warmRobinSourceCircuit : Circuit :=
[ Gate.oracleCall "H_W^(kappa)"
, Gate.oracleCall "U_indic"
, Gate.oracleCall "O_DT^S"
, Gate.oracleCall "Ry_boundary"
, Gate.oracleCall "O_DT^BS"
, Gate.oracleCall "U_indic^dagger"
, Gate.oracleCall "O_f"
, Gate.oracleCall "SWAP(two n-qubit registers; paper label only)"
, Gate.oracleCall "(O_D^BS)^dagger"
, Gate.oracleCall "(H_W^(kappa))^dagger"
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin source circuit gate list”; the hypotheses and conclusion in the code panel fix its exact scope. The warm adapter preserves the exact source order of all ten blocks.
theorem warmRobinSourceCircuit_gateList :
warmRobinSourceCircuit =
[ Gate.oracleCall "H_W^(kappa)"
, Gate.oracleCall "U_indic"
, Gate.oracleCall "O_DT^S"
, Gate.oracleCall "Ry_boundary"
, Gate.oracleCall "O_DT^BS"
, Gate.oracleCall "U_indic^dagger"
, Gate.oracleCall "O_f"
, Gate.oracleCall "SWAP(two n-qubit registers; paper label only)"
, Gate.oracleCall "(O_D^BS)^dagger"
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin source circuit length”; the hypotheses and conclusion in the code panel fix its exact scope. The source-facing warm transcript contains exactly ten blocks.
theorem warmRobinSourceCircuit_length :
warmRobinSourceCircuit.length = 10 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin parameters spec”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete fields of the fixed warm parameter adapter.
theorem warmRobinParameters_spec :
warmRobinParameters.n = 3 ∧
warmRobinParameters.kappa = 7 ∧
warmRobinParameters.functionPieces = 1 ∧
warmRobinParameters.polynomialDegreeCost = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin source layout spec”; the hypotheses and conclusion in the code panel fix its exact scope. The theorem layout is '(system, signal, pure ancilla) = (3, 9, 6)'.
theorem warmRobinSourceLayout_spec :
warmRobinSourceLayout.systemQubits = 3 ∧
warmRobinSourceLayout.signalQubits = 9 ∧
warmRobinSourceLayout.pureAncillas = 6 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin visible partition spec”; the hypotheses and conclusion in the code panel fix its exact scope. The visible source partition has widths '(5, 1, 3, 0, 3, 1)'.
theorem warmRobinVisiblePartition_spec :
warmRobinVisiblePartition.mfQubits = 5 ∧
warmRobinVisiblePartition.indicatorQubit = 1 ∧
warmRobinVisiblePartition.sparseIndexQubits = 3 ∧
warmRobinVisiblePartition.odPureAncillaQubits = 0 ∧
warmRobinVisiblePartition.systemQubits = 3 ∧
warmRobinVisiblePartition.ancillaQubit = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin total qubits eq”; the hypotheses and conclusion in the code panel fix its exact scope. The visible source register partition occupies thirteen qubits.
theorem warmRobinTotalQubits_eq :
GHL2025.oneTermRobinTotalQubits warmRobinParameters = 13 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin effective signal qubits eq”; the hypotheses and conclusion in the code panel fix its exact scope. The clean projection covers all ten non-system wires.
theorem warmRobinEffectiveSignalQubits_eq :
GHL2025.effectiveRobinSignalQubits warmRobinParameters = 10 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin indicator certificate”; the hypotheses and conclusion in the code panel fix its exact scope. The fixed warm indicator and its dagger form one self-inverse permutation pair.
theorem warmRobinIndicatorCertificate :
(GHL2025.oneTermRobinGate_U_indic_dagger warmRobinParameters).matrix =
(GHL2025.oneTermRobinGate_U_indic warmRobinParameters).matrix ∧
(∀ j : Nat,
GHL2025.indicatorOracleImage warmRobinParameters
(GHL2025.indicatorOracleImage warmRobinParameters j) = j) ∧
(∀ i : Fin (qubitDim
(GHL2025.oneTermRobinTotalQubits warmRobinParameters)),
∃ j : Fin (qubitDim
(GHL2025.oneTermRobinTotalQubits warmRobinParameters)),
GHL2025.indicatorOracleMatrix warmRobinParameters i j = Coeff.rat 1 ∧
commit-pinned source · Verso Blueprint panel