On-Curve Capture Lemmas

If f vanishes at a point on the boundary curve fdBoundaryH H, then that point is captured by one of the singular sets sArcOfS S or sVertOfS S.

Main Results

• oncurve_arc_capture — arc points (‖·‖ = 1) land in sArcOfS S
• oncurve_vert_capture — seg1 points (t ∈ (0,1)) land in sVertOfS S
• height_contradiction — seg5 / endpoint points (im = H) contradict the height bound
• oncurve_seg4_capture — seg4 points (t ∈ (3,4)) land in sVertOfS S via T-periodicity
• oncurve_full_capture — full assembly for all t ∈ [0,5]

theorem oncurve_arc_capture {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H : ℝ} (hH : √3 / 2 < H) {t : ℝ} (ht : t ∈ Set.Icc 0 5) (h_norm : ‖fdBoundaryH H t‖ = 1) (h_zero : modularFormCompOfComplex f (fdBoundaryH H t) = 0) : fdBoundaryH H t ∈ ↑(sArcOfS S)

Arc points with ‖·‖ = 1 are captured by sArcOfS S.

theorem oncurve_vert_capture {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H' : ℝ} (hH' : √3 / 2 < H') {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (h_zero : modularFormCompOfComplex f (fdBoundaryH H' t) = 0) : fdBoundaryH H' t ∈ ↑(sVertOfS S)

Seg1 points with t ∈ (0,1) are captured by sVertOfS S.

theorem height_contradiction {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H : ℝ} (hH_ge1 : 1 ≤ H) (hH_bound : ∀ s ∈ S, (↑s).im < H) {z : ℂ} (h_im : z.im = H) (h_re : |z.re| ≤ 1 / 2) (h_zero : modularFormCompOfComplex f z = 0) : False

A zero at height H with |re| ≤ 1/2 contradicts the height bound.

theorem seg4_eq_seg1_minus_one_H (H s : ℝ) (_hs : s ∈ Set.Icc 0 1) : fdBoundarySeg4H H (4 - s) = fdBoundarySeg1H H s - 1

theorem oncurve_seg4_capture {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H : ℝ} (hH : √3 / 2 < H) {t : ℝ} (ht : t ∈ Set.Ioo 3 4) (h_zero : modularFormCompOfComplex f (fdBoundaryH H t) = 0) : fdBoundaryH H t ∈ ↑(sVertOfS S)

Seg4 points with t ∈ (3,4) are captured by sVertOfS S via T-periodicity.

theorem oncurve_full_capture {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (_hS : ∀ p ∈ S, p ∈ ModularGroup.fd) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H : ℝ} (hH_ge1 : 1 ≤ H) (hH_sqrt3 : √3 / 2 < H) (hH_bound : ∀ s ∈ S, (↑s).im < H) (t : ℝ) : t ∈ Set.Icc 0 5 → modularFormCompOfComplex f (fdBoundaryH H t) = 0 → fdBoundaryH H t ∈ ↑(sArcOfS S ∪ sVertOfS S)

Full on-curve capture: any zero of f on fdBoundaryH H is in the singular set.