The boundary contour of the standard fundamental domain

The raw five-segment path family fdBoundary H, parameterized over [0, 5] at a height parameter H: the right vertical from 1/2 + H·i through ρ + 1, the unit-circle arcs from ρ + 1 to i and from i to ρ, the left vertical from ρ through -1/2 + H·i, and the closing top horizontal. For 1 < H — so that the horizontal sits above the arc, whose highest point is i — this is the boundary of the standard fundamental domain truncated at height H; the definitions carry no hypothesis, and the boundary reading is invoked with that bound downstream. The corner values and closedness recorded here are the anchors of the valence-formula contour.

Main declarations

• TauCeti.ModularForm.fdBoundary (with the segments fdBoundarySegment1 … fdBoundarySegment5, built from AffineMap.lineMap and circleMap).
• TauCeti.ModularForm.rho_im: the corner ρ sits on the row Im = √3/2.
• TauCeti.ModularForm.segment1_chord_im: the right vertical's chord spans the height difference √3/2 - H.
• TauCeti.ModularForm.fdBoundary_apply_three: the parameter 3 lands on ρ.
• TauCeti.ModularForm.fdBoundary_closed: the contour is closed.
• TauCeti.ModularForm.continuous_fdBoundary: the contour is (globally) continuous.
• TauCeti.ModularForm.isPiecewiseC1On_fdBoundary: the contour is piecewise C¹ (contDiffOn_fdBoundary certifies fdBoundaryCorners as a breakpoint witness).
• TauCeti.ModularForm.injOn_fdBoundary_arc: the arc is traversed injectively — it covers less than a full turn of the unit circle.
• TauCeti.ModularForm.fdBoundary_four_sub_vertical, …_four_sub_arc: the reflection t ↦ 4 - t identifies the verticals through z ↦ z - 1 and the arc with its own reversal through z ↦ -1/z — the boundary identifications driving the cancellations in the valence-formula contour integral.

References

• AINTLIB LeanModularForms — the valence-formula development this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.rho_im : (↑UpperHalfPlane.ρ).im = √3 / 2

The corner ρ sits on the row Im = √3/2, the height at which the two vertical edges of 𝒟 meet the unit circle.

Not @[simp], tested: Mathlib's UpperHalfPlane.coe_im is already @[simp] and rewrites the left-hand side (↑ρ).im to ρ.im — the ℍ-valued imaginary part — so this statement is not in simp-normal form and simpNF rejects the attribute. The lemma is a rw target for goals that arrive in the complex form, which is how Complex.sub_im and friends leave them.

noncomputable def TauCeti.ModularForm.fdBoundarySegment1 (H : ℝ) : ℝ → ℂ

Segment 1: the right vertical from 1/2 + H·i through ρ + 1, over t ∈ [0, 1].

Equations

• TauCeti.ModularForm.fdBoundarySegment1 H t = (AffineMap.lineMap (1 / 2 + ↑H * Complex.I) (↑UpperHalfPlane.ρ + 1)) t

noncomputable def TauCeti.ModularForm.fdBoundarySegment2 : ℝ → ℂ

Segment 2: the unit-circle arc from ρ + 1 to i (angle π/3 → π/2), over t ∈ [1, 2].

Equations

• TauCeti.ModularForm.fdBoundarySegment2 t = circleMap 0 1 (Real.pi / 3 + (t - 1) * (Real.pi / 2 - Real.pi / 3))

noncomputable def TauCeti.ModularForm.fdBoundarySegment3 : ℝ → ℂ

Segment 3: the unit-circle arc from i to ρ (angle π/2 → 2π/3), over t ∈ [2, 3].

Equations

• TauCeti.ModularForm.fdBoundarySegment3 t = circleMap 0 1 (Real.pi / 2 + (t - 2) * (2 * Real.pi / 3 - Real.pi / 2))

noncomputable def TauCeti.ModularForm.fdBoundarySegment4 (H : ℝ) : ℝ → ℂ

Segment 4: the left vertical from ρ through -1/2 + H·i, over t ∈ [3, 4].

Equations

• TauCeti.ModularForm.fdBoundarySegment4 H t = (AffineMap.lineMap (↑UpperHalfPlane.ρ) (-1 / 2 + ↑H * Complex.I)) (t - 3)

noncomputable def TauCeti.ModularForm.fdBoundarySegment5 (H : ℝ) : ℝ → ℂ

Segment 5: the top horizontal from -1/2 + H·i to 1/2 + H·i, over t ∈ [4, 5].

Equations

• TauCeti.ModularForm.fdBoundarySegment5 H t = (AffineMap.lineMap (-1 / 2 + ↑H * Complex.I) (1 / 2 + ↑H * Complex.I)) (t - 4)

The five characteristic evaluation lemmas: the segment definitions are sealed by the module system, and these equations are the supported cross-module rewrites. They are deliberately not @[simp]: the endpoint values fdBoundary_segment*_apply_* below are the simp normal forms, and a general unfolding rule would reduce their left-hand sides past them (the arc endpoints do not simp-evaluate from circleMap).

theorem TauCeti.ModularForm.fdBoundarySegment1_apply (H t : ℝ) : fdBoundarySegment1 H t = (AffineMap.lineMap (1 / 2 + ↑H * Complex.I) (↑UpperHalfPlane.ρ + 1)) t

Segment 1 evaluated: the line from 1/2 + H·i to ρ + 1.

theorem TauCeti.ModularForm.fdBoundarySegment2_apply (t : ℝ) : fdBoundarySegment2 t = circleMap 0 1 (Real.pi / 3 + (t - 1) * (Real.pi / 2 - Real.pi / 3))

Segment 2 evaluated: the unit-circle arc at angle π/3 + (t - 1)·(π/2 - π/3).

theorem TauCeti.ModularForm.fdBoundarySegment3_apply (t : ℝ) : fdBoundarySegment3 t = circleMap 0 1 (Real.pi / 2 + (t - 2) * (2 * Real.pi / 3 - Real.pi / 2))

Segment 3 evaluated: the unit-circle arc at angle π/2 + (t - 2)·(2π/3 - π/2).

theorem TauCeti.ModularForm.fdBoundarySegment4_apply (H t : ℝ) : fdBoundarySegment4 H t = (AffineMap.lineMap (↑UpperHalfPlane.ρ) (-1 / 2 + ↑H * Complex.I)) (t - 3)

Segment 4 evaluated: the line from ρ to -1/2 + H·i at parameter t - 3.

theorem TauCeti.ModularForm.fdBoundarySegment5_apply (H t : ℝ) : fdBoundarySegment5 H t = (AffineMap.lineMap (-1 / 2 + ↑H * Complex.I) (1 / 2 + ↑H * Complex.I)) (t - 4)

Segment 5 evaluated: the line from -1/2 + H·i to 1/2 + H·i at parameter t - 4.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment1_apply_zero (H : ℝ) : fdBoundarySegment1 H 0 = 1 / 2 + ↑H * Complex.I

Segment 1 starts at the top right corner 1/2 + H·i.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment1_apply_one (H : ℝ) : fdBoundarySegment1 H 1 = ↑UpperHalfPlane.ρ + 1

Segment 1 ends at the corner ρ + 1.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment2_apply_one : fdBoundarySegment2 1 = ↑UpperHalfPlane.ρ + 1

Segment 2 starts at the corner ρ + 1.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment2_apply_two : fdBoundarySegment2 2 = Complex.I

Segment 2 ends at i.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment3_apply_two : fdBoundarySegment3 2 = Complex.I

Segment 3 starts at i.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment3_apply_three : fdBoundarySegment3 3 = ↑UpperHalfPlane.ρ

Segment 3 ends at the elliptic corner ρ.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment4_apply_three (H : ℝ) : fdBoundarySegment4 H 3 = ↑UpperHalfPlane.ρ

Segment 4 starts at the elliptic corner ρ.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment4_apply_four (H : ℝ) : fdBoundarySegment4 H 4 = -1 / 2 + ↑H * Complex.I

Segment 4 ends at the top left corner -1/2 + H·i.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment5_apply_four (H : ℝ) : fdBoundarySegment5 H 4 = -1 / 2 + ↑H * Complex.I

Segment 5 starts at the top left corner -1/2 + H·i.

@[simp]

theorem TauCeti.ModularForm.fdBoundarySegment5_apply_five (H : ℝ) : fdBoundarySegment5 H 5 = 1 / 2 + ↑H * Complex.I

Segment 5 ends at the top right corner 1/2 + H·i.

noncomputable def TauCeti.ModularForm.fdBoundary (H : ℝ) : ℝ → ℂ

The raw five-segment path at height parameter H, parameterized over [0, 5] and closed for every H. For 1 < H it is the boundary of the standard fundamental domain truncated at height H.

Equations

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

noncomputable def TauCeti.ModularForm.fdBoundaryBreakpoints : Finset ℝ

The four interior subdivision parameters of the five-segment parameterization; the junction at 2 is smooth, so only fdBoundaryCorners are genuine corners.

Equations

• TauCeti.ModularForm.fdBoundaryBreakpoints = {1, 2, 3, 4}

@[simp]

theorem TauCeti.ModularForm.mem_fdBoundaryBreakpoints {t : ℝ} : t ∈ fdBoundaryBreakpoints ↔ t = 1 ∨ t = 2 ∨ t = 3 ∨ t = 4

Membership in the four subdivision parameters.

The simp normal form: the five branch selectors together with the segment-endpoint values form the simp set, so fdBoundary H t at a corner numeral reduces in two steps — branch selection, then the endpoint value (fdBoundary H 1 to fdBoundarySegment1 H 1 to ↑ρ + 1). The fdBoundary_apply_* corner lemmas below restate the composites for rw ergonomics; they are deliberately not @[simp], since the two-step chain already reduces their left-hand sides (simp-normal-form confluence).

@[simp]

theorem TauCeti.ModularForm.fdBoundary_of_le_one {H t : ℝ} (ht : t ≤ 1) : fdBoundary H t = fdBoundarySegment1 H t

On t ≤ 1 the path follows segment 1.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_of_le_two {H t : ℝ} (h1 : 1 < t) (h2 : t ≤ 2) : fdBoundary H t = fdBoundarySegment2 t

On 1 < t ≤ 2 the path follows segment 2.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_of_le_three {H t : ℝ} (h2 : 2 < t) (h3 : t ≤ 3) : fdBoundary H t = fdBoundarySegment3 t

On 2 < t ≤ 3 the path follows segment 3.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_of_le_four {H t : ℝ} (h3 : 3 < t) (h4 : t ≤ 4) : fdBoundary H t = fdBoundarySegment4 H t

On 3 < t ≤ 4 the path follows segment 4.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_of_gt_four {H t : ℝ} (h4 : 4 < t) : fdBoundary H t = fdBoundarySegment5 H t

On 4 < t the path follows segment 5.

theorem TauCeti.ModularForm.fdBoundary_apply_zero (H : ℝ) : fdBoundary H 0 = 1 / 2 + ↑H * Complex.I

The path starts at the top right corner 1/2 + H·i.

theorem TauCeti.ModularForm.fdBoundary_apply_one (H : ℝ) : fdBoundary H 1 = ↑UpperHalfPlane.ρ + 1

The parameter 1 lands on the corner ρ + 1.

theorem TauCeti.ModularForm.fdBoundary_apply_two (H : ℝ) : fdBoundary H 2 = Complex.I

The parameter 2 lands on i.

theorem TauCeti.ModularForm.fdBoundary_apply_three (H : ℝ) : fdBoundary H 3 = ↑UpperHalfPlane.ρ

The parameter 3 lands on the elliptic corner ρ.

theorem TauCeti.ModularForm.fdBoundary_apply_four (H : ℝ) : fdBoundary H 4 = -1 / 2 + ↑H * Complex.I

The parameter 4 lands on the top left corner -1/2 + H·i.

theorem TauCeti.ModularForm.fdBoundary_apply_five (H : ℝ) : fdBoundary H 5 = 1 / 2 + ↑H * Complex.I

The path ends where it starts, at 1/2 + H·i.

theorem TauCeti.ModularForm.fdBoundary_closed (H : ℝ) : fdBoundary H 5 = fdBoundary H 0

The boundary contour is closed.

theorem TauCeti.ModularForm.contDiff_fdBoundarySegment1 {n : WithTop ℕ∞} (H : ℝ) : ContDiff ℝ n (fdBoundarySegment1 H)

Segment 1 is smooth.

theorem TauCeti.ModularForm.contDiff_fdBoundarySegment2 {n : WithTop ℕ∞} : ContDiff ℝ n fdBoundarySegment2

Segment 2 is smooth.

theorem TauCeti.ModularForm.contDiff_fdBoundarySegment3 {n : WithTop ℕ∞} : ContDiff ℝ n fdBoundarySegment3

Segment 3 is smooth.

theorem TauCeti.ModularForm.contDiff_fdBoundarySegment4 {n : WithTop ℕ∞} (H : ℝ) : ContDiff ℝ n (fdBoundarySegment4 H)

Segment 4 is smooth.

theorem TauCeti.ModularForm.contDiff_fdBoundarySegment5 {n : WithTop ℕ∞} (H : ℝ) : ContDiff ℝ n (fdBoundarySegment5 H)

Segment 5 is smooth.

theorem TauCeti.ModularForm.eqOn_fdBoundarySegment1 (H : ℝ) : Set.EqOn (fdBoundary H) (fdBoundarySegment1 H) (Set.Icc 0 1)

On [0, 1] the path agrees with segment 1.

theorem TauCeti.ModularForm.eqOn_fdBoundarySegment2 (H : ℝ) : Set.EqOn (fdBoundary H) fdBoundarySegment2 (Set.Icc 1 2)

On [1, 2] the path agrees with segment 2.

theorem TauCeti.ModularForm.eqOn_fdBoundarySegment3 (H : ℝ) : Set.EqOn (fdBoundary H) fdBoundarySegment3 (Set.Icc 2 3)

On [2, 3] the path agrees with segment 3.

theorem TauCeti.ModularForm.eqOn_fdBoundarySegment4 (H : ℝ) : Set.EqOn (fdBoundary H) (fdBoundarySegment4 H) (Set.Icc 3 4)

On [3, 4] the path agrees with segment 4.

theorem TauCeti.ModularForm.eqOn_fdBoundarySegment5 (H : ℝ) : Set.EqOn (fdBoundary H) (fdBoundarySegment5 H) (Set.Icc 4 5)

On [4, 5] the path agrees with segment 5.

theorem TauCeti.ModularForm.eqOn_fdBoundary_arc (H : ℝ) : Set.EqOn (fdBoundary H) (fun (s : ℝ) => circleMap 0 1 ((s + 1) * (Real.pi / 6))) (Set.Icc 1 3)

On [1, 3] the path agrees with the unified unit-circle arc of angle (t + 1)·π/6: the two arc segments continue one smooth circle parameterization.

theorem TauCeti.ModularForm.injOn_fdBoundary_arc (H : ℝ) : Set.InjOn (fdBoundary H) (Set.Icc 1 3)

The arc is traversed injectively. On [1, 3] the boundary runs through the angles [π/3, 2π/3] of the unit circle — less than one full turn — so circleMap is injective there and distinct parameters give distinct points.

noncomputable def TauCeti.ModularForm.fdBoundaryCorners : Finset ℝ

The genuinely nonsmooth junctions of the boundary contour: the two arcs continue one smooth circle parameterization through t = 2, so only 1, 3, and 4 are corners.

Equations

• TauCeti.ModularForm.fdBoundaryCorners = {1, 3, 4}

@[simp]

theorem TauCeti.ModularForm.mem_fdBoundaryCorners {t : ℝ} : t ∈ fdBoundaryCorners ↔ t = 1 ∨ t = 3 ∨ t = 4

Membership in the corner parameters.

theorem TauCeti.ModularForm.continuous_fdBoundary (H : ℝ) : Continuous (fdBoundary H)

The boundary path is continuous: consecutive segments agree at the junctions.

theorem TauCeti.ModularForm.continuousOn_fdBoundary (H : ℝ) : ContinuousOn (fdBoundary H) (Set.Icc 0 5)

The boundary path is continuous on the parameter interval [0, 5].

theorem TauCeti.ModularForm.subset_piece_of_disjoint_corners {c d : ℝ} (hcd : Set.Icc c d ⊆ Set.Icc 0 5) (hdis : Disjoint (↑fdBoundaryCorners) (Set.Ioo c d)) : Set.Icc c d ⊆ Set.Icc 0 1 ∨ Set.Icc c d ⊆ Set.Icc 1 3 ∨ Set.Icc c d ⊆ Set.Icc 3 4 ∨ Set.Icc c d ⊆ Set.Icc 4 5

A corner-free closed subinterval of [0, 5] lies inside one smooth piece — the classification certificate shared by the smoothness and immersion witnesses.

theorem TauCeti.ModularForm.contDiffOn_fdBoundary {n : WithTop ℕ∞} (H : ℝ) {c d : ℝ} (hcd : Set.Icc c d ⊆ Set.Icc 0 5) (hdis : Disjoint (↑fdBoundaryCorners) (Set.Ioo c d)) : ContDiffOn ℝ n (fdBoundary H) (Set.Icc c d)

On every closed subinterval of [0, 5] whose interior avoids the three genuine corners, the contour is smooth at every order — the certificate that fdBoundaryCorners is a valid breakpoint witness for isPiecewiseC1On_fdBoundary. The two arcs continue one smooth circle map through t = 2, so no hypothesis excludes it.

theorem TauCeti.ModularForm.im_fdBoundary_of_le_four {t H : ℝ} (h3 : 3 < t) (h4 : t ≤ 4) : (fdBoundary H t).im = √3 / 2 + (t - 3) * (H - √3 / 2)

The left vertical ascends affinely from the corner row to the ceiling.

theorem TauCeti.ModularForm.re_fdBoundarySegment1 (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (fdBoundary H t).re = 1 / 2

The right vertical has constant real part 1/2.

theorem TauCeti.ModularForm.im_fdBoundary_arc_le (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 1 3) : (fdBoundary H t).im ≤ 1

The arc stays at height at most 1.

theorem TauCeti.ModularForm.im_fdBoundary_arc_pos (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 1 3) : 0 < (fdBoundary H t).im

The arc stays in the open upper half-plane.

theorem TauCeti.ModularForm.re_fdBoundarySegment4 (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 3 4) : (fdBoundary H t).re = -(1 / 2)

The left vertical has constant real part -1/2.

theorem TauCeti.ModularForm.im_fdBoundarySegment5 (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 4 5) : (fdBoundary H t).im = H

The truncation ceiling has constant height H.

theorem TauCeti.ModularForm.isPiecewiseC1On_fdBoundary (H : ℝ) : Contour.IsPiecewiseC1On (fdBoundary H) 0 5

The fundamental-domain boundary contour is piecewise C¹ on [0, 5]; contDiffOn_fdBoundary certifies the three genuine corners as a breakpoint witness.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_four_sub_vertical (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : fdBoundary H (4 - t) = fdBoundary H t - 1

The reflection t ↦ 4 - t of the parameter interval carries the right vertical onto the left vertical through the translation z ↦ z - 1: the two verticals of the fundamental-domain boundary are identified by T⁻¹.

@[simp]

theorem TauCeti.ModularForm.fdBoundary_four_sub_arc (H : ℝ) {t : ℝ} (ht : t ∈ Set.Icc 1 3) : fdBoundary H (4 - t) = -1 / fdBoundary H t

The reflection t ↦ 4 - t of the parameter interval carries the unit-circle arc onto itself, reversed, through the inversion z ↦ -1/z: the two halves of the arc of the fundamental-domain boundary are identified by S.

Coordinates of the segments

The real part, imaginary part and norm of the contour, segment by segment: elementary computations from the segment formulas, needed wherever a point of the boundary has to be located. They say nothing about winding, and are used by the principal-value and capture arguments as much as by the winding ones.

theorem TauCeti.ModularForm.re_fdBoundary_of_le_one {H t : ℝ} (h1 : t ≤ 1) : (fdBoundary H t).re = 1 / 2

The right vertical has constant real part 1/2.

theorem TauCeti.ModularForm.segment1_chord_im {H : ℝ} : (↑UpperHalfPlane.ρ + 1 - (1 / 2 + ↑H * Complex.I)).im = √3 / 2 - H

The segment-1 chord spans the height difference: the right vertical runs from the ceiling H to the corner row √3/2, so its chord has imaginary part √3/2 - H.

Not @[simp], for the same reason as rho_im: UpperHalfPlane.coe_im normalises (↑ρ).im away before this could fire, so the left-hand side is not in simp-normal form.

theorem TauCeti.ModularForm.im_fdBoundary_of_le_one {H t : ℝ} (h1 : t ≤ 1) : (fdBoundary H t).im = H + t * (√3 / 2 - H)

The right vertical runs affinely in height from the ceiling H to the corner row √3/2, descending when the ceiling is above that row and ascending when it is below.

theorem TauCeti.ModularForm.re_fdBoundary_of_le_four {H t : ℝ} (h3 : 3 < t) (h4 : t ≤ 4) : (fdBoundary H t).re = -(1 / 2)

The left vertical has constant real part -1/2.

theorem TauCeti.ModularForm.re_fdBoundary_of_gt_four {H t : ℝ} (h4 : 4 < t) : (fdBoundary H t).re = -(1 / 2) + (t - 4)

The truncation ceiling runs affinely from the left corner to the right.

theorem TauCeti.ModularForm.im_fdBoundary_of_gt_four {H t : ℝ} (h4 : 4 < t) : (fdBoundary H t).im = H

The truncation ceiling has constant height H.

@[simp]

theorem TauCeti.ModularForm.norm_fdBoundary_arc {H t : ℝ} (h1 : 1 ≤ t) (h3 : t ≤ 3) : ‖fdBoundary H t‖ = 1

The arc lies on the unit circle.