The boundary principal value of a level-one logarithmic derivative #
intervalIntegral_excised_logDeriv_fdBoundary assembles the boundary integral at a fixed
ε, as 2πi·ord_∞ − (k/2)·∫₁³ (excised logDeriv γ). Two further facts turn that into a
principal value:
- the excised integrand is integrable for every
ε(ExcisedIntegrability), so the assembly's assumed hypotheses hold, and the first clause ofHasCauchyPVWithis immediate; - the arc term converges, to
(π/3)·I(ArcExcisionMeasure).
So the excised integrals converge, and the limit is 2πi·ord_∞ − k·(π/6)·I — the same constant
the unexcised assembly produces, as it must be, since the excision only buys tolerance of zeros
on the contour.
Main results #
TauCeti.ModularForm.hasCauchyPVWith_fdBoundary_logDeriv_comp_ofComplex: the boundary principal value oflogDeriv (f ∘ ofComplex)is2πi·ord_∞ − k·(π/6)·I, for a unit-norm inversion-closed excision set.hasCauchyPVWith_fdBoundary_logDeriv_arcSingularSet_union_verticalSingularSet(inTauCeti.ModularForm): the same principal value for the union-shaped excision setarcSingularSet S ∪ verticalSingularSet S, which tolerates contour zeros on the vertical edges as well as on the arc.TauCeti.ModularForm.two_pi_I_mul_sum_windingNumber_mul_order_eq: equating either with the argument principle gives2πi·Σ n_z·ord z = 2πi·ord_∞ − k·(π/6)·I, the analytic identity the valence formula rests on.TauCeti.ModularForm.sum_windingNumber_mul_orderOfVanishingAt_eq: that identity divided by2πi, givingΣ n_z·ord z = ord_∞ − k/12.TauCeti.ModularForm.sum_orderOfVanishingAt_add_qExpansionOrderAtCusp_eq: the valence formulaΣ_q ord_q + ord_∞ = k/12when every divisor point — zero or pole — lies in the strict interior of the truncated fundamental domain.TauCeti.ModularForm.sum_orderOfVanishingAt_add_elliptic_add_qExpansionOrderAtCusp_eq: the valence formulaΣ_int ord_q + Σ_leftVert ord_q + Σ_{leftArc∖ρ} ord_q + ½·ord_i + ⅓·ord_ρ + ord_∞ = k/12for a nonzero level-one form and a divisor set that is complete for the closed fundamental domain and confined to it: every point of𝒟of nonzero order lies inS(hcomp), and every point ofSof nonzero order lies in𝒟(hSfd). The divisor may meet the corners, the vertical edges and the unit arc — each boundary pair enters by its left representative — and the truncation height and every analytic input are chosen internally.finsum_orderOfVanishingOnOrbit_mem_image_add_elliptic_add_qExpansionOrderAtCusp_eq(inTauCeti.ModularForm): the same identity with the interior sum reindexed over the orbits its points represent. ⚠ That sum covers only the orbits met by the divisor setS, not the whole non-elliptic orbit space.
References #
- AINTLIB
LeanModularForms(commit2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck) — the valence-formula development. Theε → 0step followsForMathlib/ValenceFormula/PVChain/Assembly.lean(cpv_modular_side_tendsto), the identification with the argument principle followsForMathlib/ValenceFormulaFinal.lean, and the internal-height threshold assembly followsvalence_formula_general_S_FMinForMathlib/ValenceFormula.lean, all ported onto the current Mathlib pin. The two-excision-set formulation and the route throughHasCauchyPV.uniqueare Tau Ceti's. - J.-P. Serre, A Course in Arithmetic, VII §3 Theorem 3 — the classical statement and contour argument this file formalizes.
The boundary principal value of a level-one logarithmic derivative. The excised integrals
converge as ε → 0⁺, to 2πi·ord_∞ − k·(π/6)·I.
The hypotheses are those of the fixed-ε assembly, with the two ε-dependent ones replaced by
their ε-free sources: hHgt (each excision centre sits below the ceiling) gives hlt once ε
is small, and hoffγ — analytic and nonvanishing off the centres at the contour points —
gives the differentiability and nonvanishing side conditions at every ε, as well as the
integrability. Stating it along the contour rather than on an open set is what keeps this
excision set independent of the argument principle's divisor set.
The boundary principal value against the union excision set. The excised integrals
for arcSingularSet S ∪ verticalSingularSet S converge as ε → 0⁺, to the same constant
2πi·ord_∞ − k·(π/6)·I as the unit-norm assembly: the union shape buys tolerance of contour
zeros on the vertical edges as well as on the arc, which is exactly what a divisor set
complete for the closed fundamental domain can force. Compare
hasCauchyPVWith_fdBoundary_logDeriv_comp_ofComplex, the unit-norm inversion-closed shape.
The weighted order sum equals the cusp order minus the weight term. Both sides are the
same Cauchy principal value along the boundary contour: hasCauchyPV_fdBoundary_logDeriv
evaluates it by the argument principle, as 2πi times the winding-weighted sum of orders over
the divisor set T — orders, not zero-counts: a point of T where the form has a pole
contributes negatively, while hpv evaluates it by an excised assembly, excising some
boundary set. Principal values are unique even across different excision sets, so the two
agree.
Keeping the excision set and T separate is what makes the statement useful: the assemblies
constrain their excision sets — to the unit circle
(hasCauchyPVWith_fdBoundary_logDeriv_comp_ofComplex) or to the two singular families
(hasCauchyPVWith_fdBoundary_logDeriv_arcSingularSet_union_verticalSingularSet) — whereas the
divisor set is unrestricted, so zeros in the interior are allowed.
This is the analytic identity the valence formula rests on: dividing by 2πi and reading off the
corner winding numbers — which are negative, the contour running clockwise: -(1/2) at i
and -(1/6) at each ρ-corner, against -1 at an interior point — turns it into
ord_∞ + ½·ord_i + ⅓·ord_ρ + Σ ord_q = k/12.
The valence identity, divided through. Cancelling the common factor 2πi puts the
identity in the shape the valence formula is usually written in: the winding-weighted sum of
orders inside the contour equals the cusp order minus k/12. The orders are meromorphic orders,
so a pole contributes negatively.
The weight term matches because k·(π/6)·I = 2πi·(k/12).
The valence formula for a divisor supported in the strict interior. When every divisor
point — pole as well as zero — lies in the strict interior of the truncated fundamental domain,
each winding number is -1 (windingNumber_fdBoundary_eq_neg_one_of_interior), so the weighted
count collapses to the plain sum of orders and the identity reads
Σ_q ord_q + ord_∞ = k/12.
The hypothesis is stronger than merely having no elliptic zeros: hin excludes every boundary
divisor point, elliptic or not, and poles along with zeros. The general case allows divisor
points on the boundary, and picks up the ½ and ⅓ terms from the corner winding numbers at
i and ρ.
The valence formula for a nonzero level-one modular form. Beyond nonvanishing, the
divisor set is only asked to capture the closed fundamental domain's divisor in both
directions — every point of 𝒟 of nonzero order lies in S (hcomp), and every point of
S of nonzero order lies in 𝒟 (hSfd); the truncation height and every analytic input
are constructed in the fixed-height layer above.
The height is internal, following valence_formula_general_S_FM in
ForMathlib/ValenceFormula.lean of AINTLIB (github.com/CBirkbeck/AINTLIB, revision
2baa76f742bdb4fb8ee323fabba41203bd390e08): exists_height_bound dominates the divisor set,
and exists_threshold_cuspFunction_ne_zero supplies the threshold above which the q-disk
of radius fdBoundaryQRadius H = exp (-2πH) sits inside the cusp function's non-vanishing
neighbourhood — the maximum of the two serves, and above it the cusp-function non-vanishing
hgz holds.
The valence formula, with its interior divisor sum reindexed over orbits. The divisor
set is captured in both directions as in the point-sum statement — every point of 𝒟 of
nonzero order lies in S (hcomp), every point of S of nonzero order lies in 𝒟
(hSfd). The order is constant along the SL₂(ℤ)-action, so the interior divisor points may
be replaced by the orbits they represent; this is faithful because distinct points of the
open fundamental domain lie in distinct orbits. The boundary families stay as point sums: the
closed domain's boundary identifications are exactly what the left-representative filters
already quotient by.
⚠ The sum here runs over the orbits met by the divisor set S, not over the whole
non-elliptic orbit space, which is what the roadmap's Layer-1 target states. Reaching that
needs the further step that an orbit missed by S contributes 0
(orderOfVanishingOnOrbit_eq_zero_of_notMem).
Level one is forced: orderOfVanishingOnOrbit is defined for 𝒮ℒ-invariant forms, so this
theorem takes the level-one class rather than a general Γ.