The ceiling contour integral is a q-circle integral

The change of variables for the cusp term of the valence contour: along the truncation ceiling the contour derivative is 1, the q-parameter maps the ceiling onto the q-circle of radius e^{-2πH}, and the logarithmic derivative of a width-1 periodic function factors through its cusp function — so the ceiling contour integral of the logarithmic derivative equals the q-circle integral of the cusp function's logarithmic derivative.

The same bridge serves the excised valence contour unchanged, because the excision never fires on the ceiling: the excision centres of the corner computations lie on the unit circle, so their heights are at most 1, while the ceiling runs at height H. Once each centre clears ε below the ceiling the excised ceiling integrand is the unexcised one, and the ceiling still reads the cusp order.

Main declarations

• TauCeti.ModularForm.intervalIntegral_fdBoundarySegment5_eq_circleIntegral_logDeriv_cuspFunction (the ceiling bridge).
• TauCeti.ModularForm.not_exists_norm_fdBoundary_sub_le_of_mem_Icc_four_five (the excision never fires on the ceiling) and intervalIntegral_excised_logDeriv_fdBoundarySegment5_eq_two_pi_I_mul_qExpansionOrderAtCusp (same namespace; the fully qualified name does not fit the line limit — so the excised ceiling integral is still 2πi · ord_∞).

References

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

theorem TauCeti.ModularForm.intervalIntegral_fdBoundarySegment5_eq_circleIntegral_logDeriv_cuspFunction {g : UpperHalfPlane → ℂ} {H : ℝ} (hper : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) 1) : ∫ (t : ℝ) in 4..5, deriv (fdBoundary H) t • logDeriv (g ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) = circleIntegral (logDeriv (UpperHalfPlane.cuspFunction 1 g)) 0 (fdBoundaryQRadius H)

The ceiling contour integral of the logarithmic derivative of a width-1 periodic function on the upper half-plane is the q-circle integral of its cusp function's logarithmic derivative: the contour derivative is 1 on the ceiling, the q-parameter carries the ceiling onto the q-circle, and the logarithmic derivative factors through the cusp function.

theorem TauCeti.ModularForm.not_exists_norm_fdBoundary_sub_le_of_mem_Icc_four_five {H ε : ℝ} {S : Finset ℂ} (hlt : ∀ s ∈ S, s.im + ε < H) {t : ℝ} (ht : t ∈ Set.Icc 4 5) : ¬∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε

The excision never fires on the ceiling. The ceiling runs at height H, so a centre whose height clears ε below it — s.im + ε < H — has no ceiling point within ε. This is the exact condition; callers with centres on the unit circle get it from ε < H - 1.

theorem TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundarySegment5_eq_two_pi_I_mul_qExpansionOrderAtCusp {g : UpperHalfPlane → ℂ} {H ε : ℝ} {S : Finset ℂ} (hlt : ∀ s ∈ S, s.im + ε < H) (hper : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) 1) (hga : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 g) q) (hgz : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 g q ≠ 0) : (∫ (t : ℝ) in 4..5, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else deriv (fdBoundary H) t • logDeriv (g ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t)) = 2 * ↑Real.pi * Complex.I * ↑(qExpansionOrderAtCusp 1 g)

The excised ceiling integral is the plain one. The excision never fires on the ceiling, so the excised integrand agrees with the unexcised one there and the ceiling still evaluates through the q-circle to 2πi · ord_∞.