Lean checks the proposition indexed as “standard ry centered difference”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem standardRy_centered_difference (u v : ℝ) :
standardRyMatrix (u + v) - standardRyMatrix (u - v) =
((2 * Real.sin (v / 2) : ℝ) : ℂ) • standardRyMatrix (u + Real.pi) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “standard ry difference factor”; the hypotheses and conclusion in the code panel fix its exact scope. The scalar sign is retained; this is equality, not equality up to phase.
theorem standardRy_difference_factor (a b : ℝ) :
standardRyMatrix a - standardRyMatrix b =
((2 * Real.sin ((a - b) / 4) : ℝ) : ℂ) •
standardRyMatrix ((a + b) / 2 + Real.pi) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift sub”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem lift_sub {qubits : ℕ} (target : Fin qubits)
(A B : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
liftPrimitiveOneQubit target (A - B) =
liftPrimitiveOneQubit target A - liftPrimitiveOneQubit target B := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift smul”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem lift_smul {qubits : ℕ} (target : Fin qubits) (c : ℂ)
(A : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
liftPrimitiveOneQubit target (c • A) = c • liftPrimitiveOneQubit target A := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lifted ry difference factor”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem liftedRy_difference_factor {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
liftPrimitiveOneQubit target (standardRyMatrix a) -
liftPrimitiveOneQubit target (standardRyMatrix b) =
((2 * Real.sin ((a - b) / 4) : ℝ) : ℂ) •
liftPrimitiveOneQubit target (standardRyMatrix ((a + b) / 2 + Real.pi)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lifted ry distance”; the hypotheses and conclusion in the code panel fix its exact scope. Exact L2 norm for every physical target and every number of spectators.
theorem liftedRy_distance {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
‖liftPrimitiveOneQubit target (standardRyMatrix a) -
liftPrimitiveOneQubit target (standardRyMatrix b)‖ =
2 * |Real.sin ((a - b) / 4)| := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lifted ry distance le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem liftedRy_distance_le {qubits : ℕ} (target : Fin qubits) (a b : ℝ) :
‖liftPrimitiveOneQubit target (standardRyMatrix a) -
liftPrimitiveOneQubit target (standardRyMatrix b)‖ ≤ |a - b| / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval ry distance”; the hypotheses and conclusion in the code panel fix its exact scope. This names the existing actual RY gate, not an abstract error assumption.
theorem eval_ry_distance {qubits : ℕ} (target : Fin qubits) (a b : ExactAngle) :
‖evalPrimitiveGate (.ry target a) - evalPrimitiveGate (.ry target b)‖ =
2 * |Real.sin ((a.eval - b.eval) / 4)| :=
liftedRy_distance target a.eval b.eval
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval ry distance le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eval_ry_distance_le {qubits : ℕ} (target : Fin qubits) (a b : ExactAngle) :
‖evalPrimitiveGate (.ry target a) - evalPrimitiveGate (.ry target b)‖ ≤
|a.eval - b.eval| / 2 := liftedRy_distance_le target a.eval b.eval
/-- Explicit Euclidean continuous-linear-map form removes all norm-scope ambiguity. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval ry clm distance le”; the hypotheses and conclusion in the code panel fix its exact scope. Explicit Euclidean continuous-linear-map form removes all norm-scope ambiguity.
theorem eval_ry_clm_distance_le {qubits : ℕ} (target : Fin qubits) (a b : ExactAngle) :
‖_root_.Matrix.toEuclideanCLM (𝕜 := ℂ) (n := PrimitiveBasis qubits)
(evalPrimitiveGate (.ry target a) - evalPrimitiveGate (.ry target b))‖ ≤
|a.eval - b.eval| / 2 := by
commit-pinned source · Verso Blueprint panel