This definition gives the library's named construction or computation for “warm robin printed boundary angle”. Literal angle printed in the source-side formula.
noncomputable def warmRobinPrintedBoundaryAngle (ratio : Real) : Real :=
Real.arccos ratio
/-- Angle required by the standard `Ry(theta)` half-angle convention. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin standard ry boundary angle”. Angle required by the standard 'Ry(theta)' half-angle convention.
noncomputable def warmRobinStandardRyBoundaryAngle (ratio : Real) : Real :=
2 * Real.arccos ratio
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin standard ry boundary angle eq twice printed”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinStandardRyBoundaryAngle_eq_twice_printed (ratio : Real) :
warmRobinStandardRyBoundaryAngle ratio =
2 * warmRobinPrintedBoundaryAngle ratio := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin register swap pairs”. The actual logical wire pairs for swapping two three-qubit registers.
def warmRobinRegisterSwapPairs : List (Nat × Nat) :=
[(0, 3), (1, 4), (2, 5)]
/-- Executable transcript fragment: three real SWAPs, never `swap 0 0`. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin register swap circuit”. Executable transcript fragment: three real SWAPs, never 'swap 0 0'.
def warmRobinRegisterSwapCircuit : Circuit :=
[Gate.swap 0 3, Gate.swap 1 4, Gate.swap 2 5]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin register swap circuit gate list”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinRegisterSwapCircuit_gateList :
warmRobinRegisterSwapCircuit =
[Gate.swap 0 3, Gate.swap 1 4, Gate.swap 2 5] := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin register swap circuit length”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinRegisterSwapCircuit_length :
warmRobinRegisterSwapCircuit.length = 3 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin register swap wire”. Fixed wire-index action induced by the register swap.
def warmRobinRegisterSwapWire (wire : Fin 6) : Fin 6 :=
if h : wire.val < 3 then
⟨wire.val + 3, by omega⟩
else
⟨wire.val - 3, by fin_cases wire <;> decide⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin register swap wire involution”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinRegisterSwapWire_involution (wire : Fin 6) :
warmRobinRegisterSwapWire (warmRobinRegisterSwapWire wire) = wire := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin register swap wire bijective”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinRegisterSwapWire_bijective :
Function.Bijective warmRobinRegisterSwapWire := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin generic source open contracts”. Obligations outside the fixed benchmark: arbitrary size and literal-source routes.
def warmRobinGenericSourceOpenContracts : List String :=
[ "arbitrary-n sparse access and uniform resource theorem"
, "general piecewise f coefficient oracle"
, "paper-literal arccos convention reconciliation"
, "complete one-dimensional and multidimensional Hamiltonian composition"
]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin generic source open contracts nonempty”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinGenericSourceOpenContracts_nonempty :
warmRobinGenericSourceOpenContracts ≠ [] := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “warm robin fixed n 8 source open contracts”. The fixed-N8, f=1, standard-RY-corrected source route is closed.
def warmRobinFixedN8SourceOpenContracts : List String := []
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin fixed n 8 source open contracts eq nil”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem warmRobinFixedN8SourceOpenContracts_eq_nil :
warmRobinFixedN8SourceOpenContracts = [] := rfl
/-- Historical compatibility alias for the generic, arbitrary-n and
paper-literal obligations. It does not describe the certified fixed-N8 route. -/
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “warm robin source open contracts”. Historical compatibility alias for the generic, arbitrary-n and paper-literal obligations.
abbrev warmRobinSourceOpenContracts : List String :=
warmRobinGenericSourceOpenContracts
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “warm robin source open contracts nonempty”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem warmRobinSourceOpenContracts_nonempty :
warmRobinSourceOpenContracts ≠ [] :=
warmRobinGenericSourceOpenContracts_nonempty
commit-pinned source · Verso Blueprint panel