Complex exponential and unit-circle helper lemmas (quantum-free)

Generic identities used by the QSP development, factored out so they carry no dependency on the quantum framework (gates, states): phase-factor scalars e^{±iφ}, the special values e^{±iπ/2}, e^{±iπ/4}, the real-square-root identity √(1-x²)² = 1-x², injectivity of t ↦ e^{it} on (0, π), and the SU(2)/unit-circle parameterizations (mul_conj_eq_norm_sq, exists_unit_mul, exists_real_unit, exists_cos_sin, exists_exp_sq_eq).

These are upstream candidates for Mathlib; nothing here mentions Gate/PureState.

theorem QuantumAlg.exp_ofReal_mul_I (θ : ℝ) : Complex.exp (↑θ * Complex.I) = ↑(Real.cos θ) + ↑(Real.sin θ) * Complex.I

exp(iθ) = cos θ + i sin θ for real θ, with real-valued cos/sin.

theorem QuantumAlg.conj_exp_I (φ : ℝ) : (starRingEnd ℂ) (Complex.exp (↑φ * Complex.I)) = Complex.exp (-(↑φ * Complex.I))

theorem QuantumAlg.conj_exp_neg_I (φ : ℝ) : (starRingEnd ℂ) (Complex.exp (-(↑φ * Complex.I))) = Complex.exp (↑φ * Complex.I)

theorem QuantumAlg.exp_I_mul_exp_neg_I (φ : ℝ) : Complex.exp (↑φ * Complex.I) * Complex.exp (-(↑φ * Complex.I)) = 1

theorem QuantumAlg.exp_neg_I_mul_exp_I (φ : ℝ) : Complex.exp (-(↑φ * Complex.I)) * Complex.exp (↑φ * Complex.I) = 1

theorem QuantumAlg.exp_pi_div_two_mul_I : Complex.exp (↑Real.pi / 2 * Complex.I) = Complex.I

theorem QuantumAlg.exp_neg_pi_div_two_mul_I : Complex.exp (-(↑Real.pi / 2 * Complex.I)) = -Complex.I

theorem QuantumAlg.sq_sqrt_one_sub_sq {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : ↑√(1 - x ^ 2) ^ 2 = 1 - ↑x ^ 2

√(1-x²) squares back to 1 - x² over ℂ for x ∈ [-1,1].

theorem QuantumAlg.exists_exp_sq_eq {p q : ℂ} (hq : q ≠ 0) (hpq : p * (starRingEnd ℂ) p = q * (starRingEnd ℂ) q) : ∃ (φ : ℝ), Complex.exp (↑φ * Complex.I) ^ 2 * q = p

A phase factor solving the degree-reduction equation e^{2iφ} q = p, available whenever |p| = |q| ≠ 0 [Lin22, hermfunc.tex:1226].

theorem QuantumAlg.exp_pi_div_four_sq : Complex.exp (↑Real.pi / 4 * Complex.I) * Complex.exp (↑Real.pi / 4 * Complex.I) = Complex.I

theorem QuantumAlg.exp_pi_div_four_mul_neg : Complex.exp (↑Real.pi / 4 * Complex.I) * Complex.exp (-(↑Real.pi / 4 * Complex.I)) = 1

theorem QuantumAlg.exp_pi_div_four_mul_I : Complex.exp (↑Real.pi / 4 * Complex.I) * Complex.I = -Complex.exp (-(↑Real.pi / 4 * Complex.I))

e^{iπ/4} · i = -e^{-iπ/4} (both equal e^{3iπ/4}).

theorem QuantumAlg.exp_neg_pi_div_four_mul_I : Complex.exp (-(↑Real.pi / 4 * Complex.I)) * Complex.I = Complex.exp (↑Real.pi / 4 * Complex.I)

e^{-iπ/4} · i = e^{iπ/4}.

theorem QuantumAlg.ofReal_sin_sq_add_cos_sq (t : ℝ) : ↑(Real.sin t) * ↑(Real.sin t) + ↑(Real.cos t) * ↑(Real.cos t) = 1

theorem QuantumAlg.exp_I_injOn_Ioo : Set.InjOn (fun (t : ℝ) => Complex.exp (↑t * Complex.I)) (Set.Ioo 0 Real.pi)

t ↦ e^{it} is injective on (0, π).

theorem QuantumAlg.mul_conj_eq_norm_sq (z : ℂ) : z * (starRingEnd ℂ) z = ↑‖z‖ ^ 2

z·z* = ‖z‖² in ℂ.

theorem QuantumAlg.exists_unit_mul {p q : ℂ} (hpq : ¬(p = 0 ∧ q = 0)) : ∃ (c : ℂ), c * p * (starRingEnd ℂ) (c * p) + c * q * (starRingEnd ℂ) (c * q) = 1 ∧ (c * p * (c * q)).im = 0

A unit-normalized multiple of a nonzero pair, with real product: the phase e^{-i·arg(pq)/2} makes |cp|² + |cq|² = 1 and c²pq real.

theorem QuantumAlg.exists_real_unit {p q : ℝ} (hpq : ¬(p = 0 ∧ q = 0)) : ∃ (v : ℝ) (w : ℝ), v ^ 2 + w ^ 2 = 1 ∧ ∃ (c : ℝ), v = c * p ∧ w = c * q

A unit-normalized positive multiple of a nonzero real pair.

theorem QuantumAlg.exists_cos_sin {v w : ℝ} (hvw : v ^ 2 + w ^ 2 = 1) : ∃ (θ : ℝ), Real.cos (θ / 2) = v ∧ Real.sin (θ / 2) = w

Any point of the real unit circle is (cos(θ/2), sin(θ/2)) for some angle θ.