Fundamental Domain Boundary – Basic Definitions

Definitions and continuity for the boundary of the standard fundamental domain for SL₂(ℤ), both at fixed height heightCutoff and at variable height H.

Main Definitions

• heightCutoff — fixed cutoff height (√3/2 + 1)
• fdBoundary — 5-segment boundary at fixed height
• fdBoundaryH — 5-segment boundary at variable height H
• fdPartition — interior partition points
• fdBoundaryFullPartition — full partition including endpoints
• fdBoundaryHPartition — partition for H-parameterized boundary
• seg5QRadiusH — q-expansion radius e^(-2πH)

noncomputable def heightCutoff : ℝ

Height cutoff for the finite-height fundamental domain boundary.

Equations

• heightCutoff = √3 / 2 + 1

theorem one_lt_heightCutoff : 1 < heightCutoff

theorem sqrt3_div2_lt_heightCutoff : √3 / 2 < heightCutoff

noncomputable def fdBoundarySeg1 : ℝ → ℂ

Segment 1: right vertical from (1/2 + H·i) down to ρ+1.

Equations

• fdBoundarySeg1 t = 1 / 2 + (↑heightCutoff - ↑t * (↑heightCutoff - ↑√3 / 2)) * Complex.I

noncomputable def fdBoundarySeg2 : ℝ → ℂ

Segment 2: arc from ρ+1 to i (angle π/3 → π/2).

Equations

• fdBoundarySeg2 t = Complex.exp ((↑Real.pi / 3 + (↑t - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I)

noncomputable def fdBoundarySeg3 : ℝ → ℂ

Segment 3: arc from i to ρ (angle π/2 → 2π/3).

Equations

• fdBoundarySeg3 t = Complex.exp ((↑Real.pi / 2 + (↑t - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I)

noncomputable def fdBoundarySeg4 : ℝ → ℂ

Segment 4: left vertical from ρ up to (-1/2 + H·i).

Equations

• fdBoundarySeg4 t = -1 / 2 + (↑√3 / 2 + (↑t - 3) * (↑heightCutoff - ↑√3 / 2)) * Complex.I

noncomputable def fdBoundarySeg5 : ℝ → ℂ

Segment 5: horizontal from (-1/2 + H·i) to (1/2 + H·i).

Equations

• fdBoundarySeg5 t = ↑t - 9 / 2 + ↑heightCutoff * Complex.I

noncomputable def fdBoundary : ℝ → ℂ

Boundary of the standard fundamental domain at fixed height heightCutoff, parameterized over [0, 5].

Equations

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

noncomputable def fdPartition : Finset ℝ

Interior partition points of fdBoundary.

Equations

• fdPartition = {1, 2, 3, 4}

noncomputable def fdBoundaryFullPartition : Finset ℝ

Full partition including endpoints.

Equations

• fdBoundaryFullPartition = {0, 1, 2, 3, 4, 5}

theorem fdBoundary_at_zero : fdBoundary 0 = 1 / 2 + ↑heightCutoff * Complex.I

theorem fdBoundary_at_one : fdBoundary 1 = ellipticPointRhoPlusOne

theorem fdBoundary_at_two : fdBoundary 2 = ellipticPointI

theorem fdBoundary_at_three : fdBoundary 3 = ellipticPointRho

theorem fdBoundary_at_four : fdBoundary 4 = -1 / 2 + ↑heightCutoff * Complex.I

theorem fdBoundary_at_five : fdBoundary 5 = 1 / 2 + ↑heightCutoff * Complex.I

theorem fdBoundary_closed : fdBoundary 0 = fdBoundary 5

noncomputable def fdBoundarySeg1H (H : ℝ) : ℝ → ℂ

Segment 1 at height H: right vertical from (1/2 + H·i) down to ρ+1.

Equations

• fdBoundarySeg1H H t = 1 / 2 + (↑H - ↑t * (↑H - ↑√3 / 2)) * Complex.I

noncomputable def fdBoundarySeg2H : ℝ → ℂ

Segment 2 at height H (H-independent): arc from ρ+1 to i.

Equations

• fdBoundarySeg2H = fdBoundarySeg2

noncomputable def fdBoundarySeg3H : ℝ → ℂ

Segment 3 at height H (H-independent): arc from i to ρ.

Equations

• fdBoundarySeg3H = fdBoundarySeg3

noncomputable def fdBoundarySeg4H (H : ℝ) : ℝ → ℂ

Segment 4 at height H: left vertical from ρ up to (-1/2 + H·i).

Equations

• fdBoundarySeg4H H t = -1 / 2 + (↑√3 / 2 + (↑t - 3) * (↑H - ↑√3 / 2)) * Complex.I

noncomputable def fdBoundarySeg5H (H : ℝ) : ℝ → ℂ

Segment 5 at height H: horizontal from (-1/2 + H·i) to (1/2 + H·i).

Equations

• fdBoundarySeg5H H t = ↑t - 9 / 2 + ↑H * Complex.I

noncomputable def fdBoundaryH (H : ℝ) : ℝ → ℂ

Boundary of the standard fundamental domain at variable height H, parameterized over [0, 5].

Equations

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

noncomputable def fdBoundaryHPartition : Finset ℝ

Non-differentiable corner points of fdBoundaryH (excluding smooth transitions at t = 2).

Equations

• fdBoundaryHPartition = {1, 3, 4}

noncomputable def seg5QRadiusH (H : ℝ) : ℝ

The q-expansion radius at height H: e^(-2πH).

Equations

• seg5QRadiusH H = Real.exp (-2 * Real.pi * H)

theorem fdBoundary_eq_fdBoundary_H : fdBoundary = fdBoundaryH heightCutoff

theorem fdBoundary_H_at_zero (H : ℝ) : fdBoundaryH H 0 = 1 / 2 + ↑H * Complex.I

theorem fdBoundary_H_at_one (H : ℝ) : fdBoundaryH H 1 = ellipticPointRhoPlusOne

theorem fdBoundary_H_at_two (H : ℝ) : fdBoundaryH H 2 = ellipticPointI

theorem fdBoundary_H_at_three (H : ℝ) : fdBoundaryH H 3 = ellipticPointRho

theorem fdBoundary_H_at_four (H : ℝ) : fdBoundaryH H 4 = -1 / 2 + ↑H * Complex.I

theorem fdBoundary_H_at_five (H : ℝ) : fdBoundaryH H 5 = 1 / 2 + ↑H * Complex.I

theorem fdBoundary_H_closed (H : ℝ) : fdBoundaryH H 0 = fdBoundaryH H 5

theorem fdBoundary_H_continuous (H : ℝ) : Continuous (fdBoundaryH H)