Shared Infrastructure for Winding Weight Computations

Common helpers used across the ρ, ρ+1, and i winding weight proofs: trigonometric identities, old-style segment selectors, the unified arc formula, and FTC lemmas for log-derivative integrals.

theorem fdBoundary_H_at_one_eq_rho_plus_one (H : ℝ) : fdBoundaryH H 1 = ellipticPointRhoPlusOne

theorem fdBoundary_H_at_two_eq_I (H : ℝ) : fdBoundaryH H 2 = Complex.I

theorem fdBoundary_H_at_three_eq_rho (H : ℝ) : fdBoundaryH H 3 = ellipticPointRho

theorem fdBoundary_H_seg0 (H : ℝ) {t : ℝ} (ht : t ≤ 1) : fdBoundaryH H t = 1 / 2 + (↑H - ↑t * (↑H - ↑√3 / 2)) * Complex.I

theorem fdBoundary_H_seg1 (H : ℝ) {t : ℝ} (ht1 : ¬t ≤ 1) (ht2 : t ≤ 2) : fdBoundaryH H t = Complex.exp ((↑Real.pi / 3 + (↑t - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I)

theorem fdBoundary_H_seg2 (H : ℝ) {t : ℝ} (ht1 : ¬t ≤ 1) (ht2 : ¬t ≤ 2) (ht3 : t ≤ 3) : fdBoundaryH H t = Complex.exp ((↑Real.pi / 2 + (↑t - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I)

theorem fdBoundary_H_seg3 (H : ℝ) {t : ℝ} (ht1 : ¬t ≤ 1) (ht2 : ¬t ≤ 2) (ht3 : ¬t ≤ 3) (ht4 : t ≤ 4) : fdBoundaryH H t = -1 / 2 + (↑√3 / 2 + (↑t - 3) * (↑H - ↑√3 / 2)) * Complex.I

theorem fdBoundary_H_seg4 (H : ℝ) {t : ℝ} (ht1 : ¬t ≤ 1) (ht2 : ¬t ≤ 2) (ht3 : ¬t ≤ 3) (ht4 : ¬t ≤ 4) : fdBoundaryH H t = ↑t - 9 / 2 + ↑H * Complex.I

theorem fdBoundary_H_eq_arc {H t : ℝ} (ht1 : 1 < t) (ht3 : t < 3) : fdBoundaryH H t = Complex.exp (↑(Real.pi * (1 + t) / 6) * Complex.I)

theorem ftc_log_piece {g h : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hh_cont : ContinuousOn h (Set.Icc a b)) (hh_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ h t) (hh_deriv_cont : ContinuousOn (deriv h) (Set.Icc a b)) (hh_slit : ∀ t ∈ Set.Icc a b, h t ∈ Complex.slitPlane) (heq : ∀ t ∈ Set.Ioo a b, g t = h t ∧ deriv g t = deriv h t) (heq_a : g a = h a) (heq_b : g b = h b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

theorem continuousOn_arg_im_nonneg : ContinuousOn Complex.arg {z : ℂ | 0 ≤ z.im ∧ z ≠ 0}

theorem continuousOn_clog_im_nonneg : ContinuousOn Complex.log {z : ℂ | 0 ≤ z.im ∧ z ≠ 0}

theorem ftc_log_piece_upper {g h : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hh_cont : ContinuousOn h (Set.Icc a b)) (hh_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ h t) (hh_deriv_cont : ContinuousOn (deriv h) (Set.Icc a b)) (hh_im_nn : ∀ t ∈ Set.Icc a b, 0 ≤ (h t).im) (hh_ne : ∀ t ∈ Set.Icc a b, h t ≠ 0) (hh_slit_interior : ∀ t ∈ Set.Ioo a b, h t ∈ Complex.slitPlane) (heq : ∀ t ∈ Set.Ioo a b, g t = h t ∧ deriv g t = deriv h t) (heq_a : g a = h a) (heq_b : g b = h b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

theorem ftc_log_piece_lower {g h : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hh_cont : ContinuousOn h (Set.Icc a b)) (hh_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ h t) (hh_deriv_cont : ContinuousOn (deriv h) (Set.Icc a b)) (hh_im_np : ∀ t ∈ Set.Icc a b, (h t).im ≤ 0) (hh_ne : ∀ t ∈ Set.Icc a b, h t ≠ 0) (hh_im_neg_interior : ∀ t ∈ Set.Ioo a b, (h t).im < 0) (heq : ∀ t ∈ Set.Ioo a b, g t = h t ∧ deriv g t = deriv h t) (heq_a : g a = h a) (heq_b : g b = h b) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (-g b) - Complex.log (-g a)

theorem ftc_piece_of_hasDerivAt {g h : ℝ → ℂ} {a b : ℝ} {d : ℝ → ℂ} (hab : a ≤ b) (hd : ∀ (t : ℝ), HasDerivAt h (d t) t) (hd_cont : Continuous d) (hg_eq : ∀ (t : ℝ), a ≤ t → t ≤ b → g t = h t) (hg_eq_nhds : ∀ t ∈ Set.Ioo a b, g =ᶠ[nhds t] h) (hh_slit : ∀ t ∈ Set.Icc a b, h t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

FTC piece helper: given HasDerivAt h d t for all t, g = h on [a,b], and h t ∈ slitPlane, get integrability + ∫ g'/g = log(g(b)) - log(g(a)).

theorem ftc_piece_upper_of_hasDerivAt {g h : ℝ → ℂ} {a b : ℝ} {d : ℝ → ℂ} (hab : a ≤ b) (hd : ∀ (t : ℝ), HasDerivAt h (d t) t) (hd_cont : Continuous d) (hg_eq : ∀ (t : ℝ), a ≤ t → t ≤ b → g t = h t) (hg_eq_nhds : ∀ t ∈ Set.Ioo a b, g =ᶠ[nhds t] h) (hh_im_nn : ∀ t ∈ Set.Icc a b, 0 ≤ (h t).im) (hh_ne : ∀ t ∈ Set.Icc a b, h t ≠ 0) (hh_slit_int : ∀ t ∈ Set.Ioo a b, h t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv g t / g t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv g t / g t = Complex.log (g b) - Complex.log (g a)

FTC piece variant for upper half-plane (im ≥ 0).

theorem hasDerivAt_arc (s : ℂ) (t : ℝ) : HasDerivAt (fun (t : ℝ) => Complex.exp (↑(Real.pi * (1 + t) / 6) * Complex.I) - s) (↑(Real.pi / 6) * Complex.I * Complex.exp (↑(Real.pi * (1 + t) / 6) * Complex.I)) t

HasDerivAt for arc parameterization exp(i*pi*(1+t)/6) - s.

theorem continuous_arc_deriv : ∀ (x : ℂ), Continuous fun (t : ℝ) => ↑(Real.pi / 6) * Complex.I * Complex.exp (↑(Real.pi * (1 + t) / 6) * Complex.I)

Continuity of the arc derivative.

theorem eventuallyEq_of_Ioo_subset {g h : ℝ → ℂ} {a b : ℝ} (hg_eq : ∀ (t : ℝ), a < t → t < b → g t = h t) (t : ℝ) (ht : t ∈ Set.Ioo a b) : g =ᶠ[nhds t] h

nhds equality from Ioo agreement.

theorem eventuallyEq_of_Iio {g h : ℝ → ℂ} {b : ℝ} (hg_eq : ∀ t < b, g t = h t) (t : ℝ) (ht : t < b) : g =ᶠ[nhds t] h

nhds equality from Iio agreement.

theorem eventuallyEq_of_Ioi {g h : ℝ → ℂ} {a : ℝ} (hg_eq : ∀ (t : ℝ), a < t → g t = h t) (t : ℝ) (ht : a < t) : g =ᶠ[nhds t] h

nhds equality from Ioi agreement.

theorem sin_pi_12_lt_half : Real.sin (Real.pi / 12) < 1 / 2

sin(π/12) < 1/2, used to bound ε from 2·sin(π/12) bounds.

theorem sin_pi_12_pos : 0 < Real.sin (Real.pi / 12)

sin(π/12) > 0.

theorem arcsin_eps_div_two_lt_pi_12 {ε : ℝ} (hε_pos : 0 < ε) (hε_lt_2sin : ε < 2 * Real.sin (Real.pi / 12)) : Real.arcsin (ε / 2) < Real.pi / 12

arcsin(ε/2) < π/12 whenever 0 < ε < 2·sin(π/12).