Generalized Winding Number at Right Edge Points

Proves generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1/2 for points s on the right vertical edge of the fundamental domain (s.re = 1/2, √3/2 < s.im < H).

theorem rightEdge_t₀_mem_Ioo (H : ℝ) (_hH : heightCutoff ≤ H) (s : ℂ) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : (H - s.im) / (H - √3 / 2) ∈ Set.Ioo 0 1

For a point on the right edge, t₀ = (H - s.im) / (H - √3/2) is the unique parameter in (0, 1) with fdBoundaryH H t₀ = s.

theorem rightEdge_fdBoundary_eq (H : ℝ) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : have t₀ := (H - s.im) / (H - √3 / 2); fdBoundaryH H t₀ = s

fdBoundaryH H passes through s at parameter t₀.

theorem rightEdge_unique_crossing (H : ℝ) (_hH : heightCutoff ≤ H) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_norm : ‖s‖ > 1) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : have t₀ := (H - s.im) / (H - √3 / 2); ∀ t ∈ Set.Icc 0 5, fdBoundaryH H t = s → t = t₀

The right edge parameter t₀ is the UNIQUE crossing point on [0, 5].

theorem rightEdge_dist_from_arc (s z : ℂ) (hz : ‖z‖ = 1) : ‖s‖ - 1 ≤ ‖z - s‖

Points on seg2/seg3 (unit circle) are at distance ≥ ‖s‖ - 1 from s.

theorem rightEdge_dist_from_leftVertical (s : ℂ) (hs_re : s.re = 1 / 2) (z : ℂ) (hz_re : z.re = -1 / 2) : 1 ≤ ‖z - s‖

Points on seg4 (left vertical, re = -1/2) are at distance ≥ 1 from s with re = 1/2.

theorem rightEdge_dist_from_horizontal {H : ℝ} (s : ℂ) (hs_im : s.im < H) (z : ℂ) (hz_im : z.im = H) : H - s.im ≤ ‖z - s‖

Points on seg5 (horizontal at height H) are at distance ≥ H - s.im from s with s.im < H.

theorem rightEdge_min_dist_pos {H : ℝ} (s : ℂ) (hs_norm : ‖s‖ > 1) (hs_im : s.im < H) : 0 < min (min (‖s‖ - 1) 1) (H - s.im)

Minimum distance from s (on right edge) to the non-seg1 parts of the boundary.

theorem ftc_log_neg {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, -f t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (-f b) - Complex.log (-f a)

FTC on a smooth segment: ∫ f'/f = log(−f(b)) − log(−f(a)) when −f stays in slitPlane. Delegates to LogDerivFTC.ftc_log_neg_on_segment.

theorem ftc_log {f : ℝ → ℂ} {a b : ℝ} (hab : a ≤ b) (hf_cont : ContinuousOn f (Set.Icc a b)) (hf_diff : ∀ t ∈ Set.Ioo a b, DifferentiableAt ℝ f t) (hf_deriv_cont : ContinuousOn (deriv f) (Set.Icc a b)) (hf_slit : ∀ t ∈ Set.Icc a b, f t ∈ Complex.slitPlane) : IntervalIntegrable (fun (t : ℝ) => deriv f t / f t) MeasureTheory.volume a b ∧ ∫ (t : ℝ) in a..b, deriv f t / f t = Complex.log (f b) - Complex.log (f a)

FTC for log ∘ f when f stays in slitPlane (no negation). Delegates to LogDerivFTC.ftc_log_on_segment.

theorem log_neg_rI_sub_log_rI {r : ℝ} (hr : 0 < r) : Complex.log (-(↑r * Complex.I)) - Complex.log (↑r * Complex.I) = -(↑Real.pi * Complex.I)

log(-(rI)) - log(rI) = -π*I for r > 0

theorem log_div_of_re_pos {a b : ℂ} (ha : 0 < a.re) (hb : 0 < b.re) : Complex.log (a / b) = Complex.log a - Complex.log b

For elements with positive real part, log(a/b) = log a - log b.

theorem hasDerivAt_arc_rep (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 the arc smooth representative minus s.

theorem re_fdBoundary_H_seg4 (H t : ℝ) (_ht1 : 1 < t) (_ht2 : 2 < t) (ht3 : 3 < t) (ht4 : t ≤ 4) : (fdBoundaryH H t).re = -1 / 2

theorem im_fdBoundary_H_seg5 (H t : ℝ) (_ht1 : 1 < t) (_ht2 : 2 < t) (_ht3 : 3 < t) (ht4 : 4 < t) : (fdBoundaryH H t).im = H

theorem rightEdge_ftc_telescope (H : ℝ) (_hH_sqrt : √3 / 2 < H) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_lt_t₀ : δ < (H - s.im) / (H - √3 / 2)) (hδ_lt_1mt₀ : δ < 1 - (H - s.im) / (H - √3 / 2)) : have h₀ := fun (t : ℝ) => fdBoundarySeg1H H t - s; have t₀ := (H - s.im) / (H - √3 / 2); IntervalIntegrable (fun (t : ℝ) => (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t) MeasureTheory.volume 0 (t₀ - δ) ∧ IntervalIntegrable (fun (t : ℝ) => (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t) MeasureTheory.volume (t₀ + δ) 5 ∧ (∫ (t : ℝ) in 0..t₀ - δ, (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t) + ∫ (t : ℝ) in t₀ + δ..5, (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t = Complex.log (-h₀ (t₀ - δ)) - Complex.log (-h₀ (t₀ + δ))

FTC telescope: the left + right logDeriv integrals of fdBoundaryH H - s (skipping the crossing interval [t₀ - δ, t₀ + δ]) equal log(-(h₀(t₀ - δ))) - log(-(h₀(t₀ + δ))). Here h₀ t = fdBoundarySeg1H H t - s, α = H - √3/2, t₀ = (H - s.im)/α, δ > 0. Also returns integrability of (fdBoundaryH H t - s)⁻¹ * deriv (fdBoundaryH H) t.

theorem gWN_fdBoundary_H_eq_neg_half_of_rightEdge (H : ℝ) (hH_sqrt : √3 / 2 < H) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_norm : ‖s‖ > 1) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1 / 2

SingleCrossingData construction for right edge

Demonstrates how the SingleCrossingData framework can be used to prove the right edge winding number result.

noncomputable def rightEdgeCrossingData (H : ℝ) (hH_sqrt : √3 / 2 < H) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_norm : ‖s‖ > 1) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : SingleCrossingData (fdBoundaryH H) 0 5 s

Construct SingleCrossingData for a right edge point.

Bundles all the geometric ingredients (crossing parameter, cutoff function, far/near bounds, FTC telescope, limit) into a single data structure.

Equations

• One or more equations did not get rendered due to their size.

theorem gWN_fdBoundary_H_eq_neg_half_of_rightEdge' (H : ℝ) (hH_sqrt : √3 / 2 < H) (s : ℂ) (hs_re : s.re = 1 / 2) (hs_norm : ‖s‖ > 1) (hs_im_lower : √3 / 2 < s.im) (hs_im : s.im < H) : generalizedWindingNumber' (fdBoundaryH H) 0 5 s = -1 / 2

Alternative proof of the right edge gWN via the SingleCrossingData framework.

Demonstrates that the main theorem can be derived from the framework by constructing rightEdgeCrossingData and applying gWN_eq_neg_half_of_singleCrossing.