On-curve capture of the boundary zeros

Every zero of a nonzero level-one modular form on the boundary contour lands in one of the two singular sets: arc points (including the corners) in the arc singular set, vertical points in the vertical singular set — the left vertical through the translation onto the right one — and ceiling points do not occur at all once the height exceeds a bound on the capturing set. The capturing hypothesis is completeness: every fundamental-domain point of nonzero vanishing order belongs to S. The contour lies in the truncated fundamental domain, so each on-curve zero yields a fundamental-domain point of S, and the segment geometry decides which singular set receives it.

Main declarations

• TauCeti.ModularForm.fdBoundary_mem_verticalSingularSet_of_mem_Ioo_zero_one and …_of_mem_Ioo_three_four (the vertical captures).
• TauCeti.ModularForm.fdBoundary_mem_arcSingularSet_of_mem_Icc_one_three (the arc capture).
• TauCeti.ModularForm.comp_ofComplex_fdBoundary_ne_zero_of_forall_im_lt (no ceiling zeros).
• TauCeti.ModularForm.fdBoundary_mem_arcSingularSet_union_verticalSingularSet_of_comp_eq_zero (the full capture).

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/OnCurveCapture.lean) this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.fdBoundary_mem_verticalSingularSet_of_mem_Ioo_zero_one {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} {S : Finset UpperHalfPlane} {H t : ℝ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (hf : ⇑f ≠ 0) (hS : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) (hH : 1 ≤ H) (ht : t ∈ Set.Ioo 0 1) (h0 : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = 0) : fdBoundary H t ∈ ↑(verticalSingularSet S)

A zero on the open right vertical is captured by the vertical singular set.

theorem TauCeti.ModularForm.fdBoundary_mem_arcSingularSet_of_mem_Icc_one_three {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} {S : Finset UpperHalfPlane} {H t : ℝ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (hf : ⇑f ≠ 0) (hS : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) (hH : 1 ≤ H) (ht : t ∈ Set.Icc 1 3) (h0 : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = 0) : fdBoundary H t ∈ ↑(arcSingularSet S)

A zero on the arc, corners included, is captured by the arc singular set.

theorem TauCeti.ModularForm.comp_ofComplex_fdBoundary_ne_zero_of_forall_im_lt {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} {S : Finset UpperHalfPlane} {H t : ℝ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (hf : ⇑f ≠ 0) (hS : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) (hH : 1 ≤ H) (hbound : ∀ p ∈ S, (↑p).im < H) (ht : t ∈ Set.Icc 0 5) (him : (fdBoundary H t).im = H) : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0

The form does not vanish on the contour's ceiling row once the height dominates the capturing set.

theorem TauCeti.ModularForm.fdBoundary_mem_verticalSingularSet_of_mem_Ioo_three_four {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} {S : Finset UpperHalfPlane} {H t : ℝ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (hf : ⇑f ≠ 0) (hS : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) (hH : 1 ≤ H) (ht : t ∈ Set.Ioo 3 4) (h0 : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = 0) : fdBoundary H t ∈ ↑(verticalSingularSet S)

A zero on the open left vertical is captured by the vertical singular set, through the translation onto the right vertical.

theorem TauCeti.ModularForm.fdBoundary_mem_arcSingularSet_union_verticalSingularSet_of_comp_eq_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} {S : Finset UpperHalfPlane} {H t : ℝ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (hf : ⇑f ≠ 0) (hS : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) (hH : 1 ≤ H) (hbound : ∀ p ∈ S, (↑p).im < H) (ht : t ∈ Set.Icc 0 5) (h0 : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = 0) : fdBoundary H t ∈ arcSingularSet S ∪ verticalSingularSet S

Full on-curve capture: every zero of the form on the boundary contour lies in one of the two singular sets, once the height dominates the capturing set.