The boundary contour lies in the truncated fundamental domain

The valence-formula contour fdBoundary H traces the boundary of the truncated fundamental domain, so every point of it lies in that domain's closure. This file records that containment and the four coordinate estimates it rests on — a height bound above and below, a bound on the real part, and the lower bound on the modulus.

These are statements about the contour's geometry alone. They are separated from the winding theory that first needed them so that consumers wanting only the containment — the excised integrability criterion, for instance — need not import winding numbers.

Main results

• TauCeti.ModularForm.fdBoundary_mem_coe_truncatedFundamentalDomain: the contour lies in the closed truncated fundamental domain.
• TauCeti.ModularForm.sqrt_three_div_two_lt_one: the corner height lies below the apex.
• TauCeti.ModularForm.sqrt_three_div_two_le_im_fdBoundary, …im_fdBoundary_le, …abs_re_fdBoundary_le_half, …one_le_norm_fdBoundary: the four coordinate estimates.

References

The contour geometry follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean), ported onto the current Mathlib pin; these declarations were first written in Tau Ceti's Winding/Basic.lean and are collected here so that consumers needing only the containment do not import winding theory.

theorem TauCeti.ModularForm.sqrt_three_div_two_lt_one : √3 / 2 < 1

The corner height √3/2 lies strictly below 1, the height of the arc's apex.

theorem TauCeti.ModularForm.sqrt_three_div_two_le_im_fdBoundary {H t : ℝ} (hH : √3 / 2 ≤ H) (ht : t ∈ Set.Icc 0 5) : √3 / 2 ≤ (fdBoundary H t).im

Every point of the boundary contour has imaginary part at least √3/2, provided the height parameter clears the corner row.

theorem TauCeti.ModularForm.abs_re_fdBoundary_le_half {H t : ℝ} (ht : t ≤ 5) : |(fdBoundary H t).re| ≤ 1 / 2

The contour's real part stays within the fundamental strip.

theorem TauCeti.ModularForm.im_fdBoundary_le {H t : ℝ} (hH : 1 ≤ H) (ht : t ∈ Set.Icc 0 5) : (fdBoundary H t).im ≤ H

The contour stays at or below its height parameter.

theorem TauCeti.ModularForm.one_le_norm_fdBoundary {H t : ℝ} (hH : 1 ≤ H) (ht : t ∈ Set.Icc 0 5) : 1 ≤ ‖fdBoundary H t‖

The boundary contour stays outside the open unit disc: the verticals and the ceiling clear it by height and offset, and the arc lies on the unit circle.

theorem TauCeti.ModularForm.fdBoundary_mem_coe_truncatedFundamentalDomain {H : ℝ} (hH : 1 ≤ H) {t : ℝ} (ht : t ∈ Set.Icc 0 5) : fdBoundary H t ∈ UpperHalfPlane.coe '' ModularGroup.truncatedFundamentalDomain H

The boundary contour lies in the closed truncated fundamental domain.