Fundamental Domain Boundary – Bounds

Segment selectors, trigonometric helpers, and geometric bounds for the fundamental domain boundary.

Main Results

• fdBoundary_H_im_pos — positive imaginary part
• fdBoundary_H_im_ge_sqrt3_div_2 — imaginary part ≥ √3/2
• fdBoundary_H_re_abs_le_half — |real part| ≤ 1/2
• fdBoundary_continuous — continuity of fixed-height boundary

theorem fdBoundary_H_eq_seg1_H {H t : ℝ} (ht : t ≤ 1) : fdBoundaryH H t = fdBoundarySeg1H H t

theorem fdBoundary_H_eq_seg2_H {t : ℝ} (H : ℝ) (ht1 : 1 < t) (ht2 : t ≤ 2) : fdBoundaryH H t = fdBoundarySeg2H t

theorem fdBoundary_H_eq_seg3_H {t : ℝ} (H : ℝ) (ht2 : 2 < t) (ht3 : t ≤ 3) : fdBoundaryH H t = fdBoundarySeg3H t

theorem fdBoundary_H_eq_seg4_H {H t : ℝ} (ht3 : 3 < t) (ht4 : t ≤ 4) : fdBoundaryH H t = fdBoundarySeg4H H t

theorem fdBoundary_H_eq_seg5_H {H t : ℝ} (ht4 : 4 < t) : fdBoundaryH H t = fdBoundarySeg5H H t

theorem fdBoundary_H_im_pos (H : ℝ) (hH : √3 / 2 < H) (t : ℝ) : t ∈ Set.Icc 0 5 → 0 < (fdBoundaryH H t).im

theorem fdBoundary_H_im_ge_sqrt3_div_2 (H : ℝ) (hH : √3 / 2 ≤ H) (t : ℝ) : t ∈ Set.Icc 0 5 → √3 / 2 ≤ (fdBoundaryH H t).im

theorem fdBoundary_H_re_abs_le_half (H t : ℝ) : t ∈ Set.Icc 0 5 → |(fdBoundaryH H t).re| ≤ 1 / 2

theorem fdBoundary_eq_seg1 {t : ℝ} (ht : t ≤ 1) : fdBoundary t = fdBoundarySeg1 t

theorem fdBoundary_eq_seg2 {t : ℝ} (ht1 : 1 < t) (ht2 : t ≤ 2) : fdBoundary t = fdBoundarySeg2 t

theorem fdBoundary_eq_seg3 {t : ℝ} (ht2 : 2 < t) (ht3 : t ≤ 3) : fdBoundary t = fdBoundarySeg3 t

theorem fdBoundary_eq_seg4 {t : ℝ} (ht3 : 3 < t) (ht4 : t ≤ 4) : fdBoundary t = fdBoundarySeg4 t

theorem fdBoundary_eq_seg5 {t : ℝ} (ht4 : 4 < t) : fdBoundary t = fdBoundarySeg5 t

theorem fdBoundary_continuous : Continuous fdBoundary

theorem fdBoundary_im_pos (t : ℝ) : t ∈ Set.Icc 0 5 → 0 < (fdBoundary t).im

theorem fdBoundary_H_im_le_H {H : ℝ} (hH : 1 ≤ H) (t : ℝ) : t ∈ Set.Icc 0 5 → (fdBoundaryH H t).im ≤ H

theorem fdBoundary_im_le_heightCutoff (t : ℝ) : t ∈ Set.Icc 0 5 → (fdBoundary t).im ≤ heightCutoff

theorem fdBoundary_re_abs_le_half (t : ℝ) : t ∈ Set.Icc 0 5 → |(fdBoundary t).re| ≤ 1 / 2

theorem fdBoundary_im_ge_sqrt3_div_2 (t : ℝ) : t ∈ Set.Icc 0 5 → √3 / 2 ≤ (fdBoundary t).im

theorem fdBoundary_passes_through_i : ∃ t ∈ Set.Icc 0 5, fdBoundary t = ellipticPointI

theorem fdBoundary_passes_through_rho : ∃ t ∈ Set.Icc 0 5, fdBoundary t = ellipticPointRho

theorem fdBoundary_passes_through_rho_plus_one : ∃ t ∈ Set.Icc 0 5, fdBoundary t = ellipticPointRhoPlusOne