7. The valence formula🔗

We now state the headline result of the modular side of the project: the classical valence formula for weight-k modular forms on \operatorname{SL}_2(\mathbb{Z}). The argument follows the textbook proof of Diamond–Shurman, Theorem 3.1.1: take the logarithmic derivative f'/f of f around the fundamental-domain boundary at height H, identify each residue with an order of vanishing, and match the resulting weighted sum against k/12 via the Hungerbühler–Wasem residue theorem and modular invariance.

Theorem7.1

Statement uses 4

Statement dependency previews

Preview

Definition 3.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let k \in \mathbb{Z} and let f be a weight-k modular form on \operatorname{SL}_2(\mathbb{Z}) (f \in M_k(\Gamma(1))). Let S \subseteq \mathcal{D} be a finite subset of the standard fundamental domain such that every order-non-zero point of f in \mathcal{D} lies in S. Assume there exists a height H and a full winding-data bundle D on \partial \mathcal{D}_H (i.e. the interior winding number -1, the elliptic winding numbers -\tfrac{1}{2}, -\tfrac{1}{6}, -\tfrac{1}{6} at i, \rho, \rho+1 respectively, and the smooth-boundary winding -\tfrac{1}{2} at every other on-curve point of \partial \mathcal{D}_H) for which every s \in S has \operatorname{Im}(s) < H and the PV chain identity \sum_{s \in S} \operatorname{gWN}\!\bigl(D.\mathrm{boundary},\, s\bigr) \cdot \operatorname{ord}_{s}(f) \;=\; -\bigl(k/12 - \operatorname{ord}_\infty(f)\bigr) holds. Then \operatorname{ord}_\infty(f) + \tfrac{1}{2}\,\operatorname{ord}_{i}(f) + \tfrac{1}{3}\,\operatorname{ord}_{\rho}(f) + \sum_{s \in \mathrm{INT}}\operatorname{ord}_{s}(f) + \sum_{s \in \mathrm{sLeftVert}} \operatorname{ord}_{s}(f) + \sum_{s \in \mathrm{LeftArc}} \operatorname{ord}_{s}(f) = \frac{k}{12}, where

\mathrm{INT} is the subset of S of strictly interior points (non-elliptic, \|s\| > 1, |\operatorname{Re} s| < 1/2);
\mathrm{sLeftVert} is the canonical-rep subset of S on the left vertical edge \operatorname{Re} s = -1/2;
\mathrm{LeftArc} is the subset of S on the left half of the unit-circle arc \|s\| = 1, \operatorname{Re} s < 0 and s \ne \rho.

Definition 3.1 Theorem 6.1 Theorem 6.2 Theorem 6.3

Lean code for Theorem7.1●1 theorem

theoremdefined in LeanModularForms/ForMathlib/CoreIdentityProof.lean

complete

theorem valence_formula_orbit_sum_of_pvChain {k : ℤ}
  (f :
    ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma 1))
      k)
  (S : Finset UpperHalfPlane) (hS : ∀ p ∈ S, p ∈ ModularGroup.fd)
  (hS_complete :
    ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S)
  (h_pvChain :
    ∃ H D,
      (∀ s ∈ S, (↑s).im < H) ∧
        ∑ s ∈ S,
            generalizedWindingNumber D.boundary ↑s *
              ↑(orderOfVanishingAt' (⇑f) s) =
          -(↑k / 12 - ↑(orderAtCusp' f))) :
  ↑(orderAtCusp' f) +
              1 / 2 * ↑(orderOfVanishingAt' (⇑f) ellipticPointI') +
            1 / 3 * ↑(orderOfVanishingAt' (⇑f) ellipticPointRho') +
          ∑ s ∈ S with
            s ≠ ellipticPointI' ∧
              s ≠ ellipticPointRho' ∧
                s ≠ ellipticPointRhoPlusOne' ∧
                  ‖↑s‖ > 1 ∧ |(↑s).re| < 1 / 2,
            ↑(orderOfVanishingAt' (⇑f) s) +
        ∑ s ∈ sLeftVertFM S, ↑(orderOfVanishingAt' (⇑f) s) +
      ∑ s ∈ S with s ≠ ellipticPointRho' ∧ ‖↑s‖ = 1 ∧ (↑s).re < 0,
        ↑(orderOfVanishingAt' (⇑f) s) =
    ↑k / 12

theorem valence_formula_orbit_sum_of_pvChain
  {k : ℤ}
  (f :
    ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma 1))
      k)
  (S : Finset UpperHalfPlane)
  (hS : ∀ p ∈ S, p ∈ ModularGroup.fd)
  (hS_complete :
    ∀ p ∈ ModularGroup.fd,
      orderOfVanishingAt' (⇑f) p ≠ 0 →
        p ∈ S)
  (h_pvChain :
    ∃ H D,
      (∀ s ∈ S, (↑s).im < H) ∧
        ∑ s ∈ S,
            generalizedWindingNumber
                D.boundary ↑s *
              ↑(orderOfVanishingAt' (⇑f)
                  s) =
          -(↑k / 12 -
              ↑(orderAtCusp' f))) :
  ↑(orderAtCusp' f) +
              1 / 2 *
                ↑(orderOfVanishingAt' (⇑f)
                    ellipticPointI') +
            1 / 3 *
              ↑(orderOfVanishingAt' (⇑f)
                  ellipticPointRho') +
          ∑ s ∈ S with
            s ≠ ellipticPointI' ∧
              s ≠ ellipticPointRho' ∧
                s ≠
                    ellipticPointRhoPlusOne' ∧
                  ‖↑s‖ > 1 ∧
                    |(↑s).re| < 1 / 2,
            ↑(orderOfVanishingAt' (⇑f)
                s) +
        ∑ s ∈ sLeftVertFM S,
          ↑(orderOfVanishingAt' (⇑f) s) +
      ∑ s ∈ S with
        s ≠ ellipticPointRho' ∧
          ‖↑s‖ = 1 ∧ (↑s).re < 0,
        ↑(orderOfVanishingAt' (⇑f) s) =
    ↑k / 12

**OrbitFM-sum valence formula**, conditional on the PV chain identity.

The hypothesis `h_pvChain` bundles:
- `FDWindingDataFull H` for some large `H` (with all winding numbers)
- The PV chain identity: the winding-weighted sum equals `-(k/12 - ord_∞)`

This is dischargeable from ForMathlib ingredients:
1. `FDWindingDataFull` from InteriorContourIntegral + CrossingAtI/Rho + BoundaryWinding
2. The PV chain identity from GeneralizedResidueTheorem + ModularContourIntegral

Given this, the proof substitutes explicit weights and pairs orbits to obtain
the textbook orbit-sum form matching `valence_formula_textbook_orbit_finsum`
in `ForMathlib/ValenceFormula.lean`.

Proof for Theorem 7.1

Proof uses 4

Proof dependency previews

Preview

Theorem 5.5

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

The PV chain identity gives a weighted sum of orders over S matching -(k/12 - \operatorname{ord}_\infty(f)). Substituting the three explicit elliptic winding numbers (-\tfrac{1}{2} at i, -\tfrac{1}{6} at \rho and at \rho+1, see Theorem 6.1, Theorem 6.2, Theorem 6.3), and using the interior winding number -1 at strictly interior points and the smooth-boundary winding -\tfrac{1}{2} at every other on-curve point, replaces \operatorname{gWN} in each term by an explicit numerical weight. The right and left boundary subsets are paired via modular invariance (the T-translation identifies the two vertical edges, and the S-action identifies the two halves of the unit-circle arc), reducing each pair to a single canonical representative. The orders at \rho and \rho+1 are equal by modular invariance; absorbing this identity gives the \tfrac{1}{3}\operatorname{ord}_\rho(f) term. Rearranging yields the claimed equality.

Theorem 6.1 Theorem 6.2 Theorem 6.3 Theorem 5.5

Theorem7.2

uses 1used by 0✓L∃∀N

Let k \in \mathbb{Z} and let f \in M_k(\Gamma(1)) be a weight-k modular form on the full modular group \operatorname{SL}_2(\mathbb{Z}) with f \ne 0. Then \operatorname{ord}_\infty(f) + \tfrac{1}{2}\,\operatorname{ord}_{i}(f) + \tfrac{1}{3}\,\operatorname{ord}_{\rho}(f) + \sum_{q \in \mathrm{NonEllOrbit}} \operatorname{ord}_{q}(f) \;=\; \frac{k}{12}, where the last sum runs over the \operatorname{SL}_2(\mathbb{Z})-orbits in \mathbb{H} that are neither the orbit of i nor the orbit of \rho, and \operatorname{ord}_q(f) is the order of vanishing of f at any representative of q (well-defined by modular invariance).

Theorem 7.1

Lean code for Theorem7.2●1 theorem

theoremdefined in LeanModularForms/ForMathlib/ValenceFormulaFinal.lean

complete

theorem valence_formula_textbook {k : ℤ}
  (f :
    ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma 1))
      k)
  (hf : f ≠ 0) :
  ↑(orderAtCusp' f) +
          1 / 2 * ↑(orderOfVanishingAt' (⇑f) ellipticPointI') +
        1 / 3 * ↑(orderOfVanishingAt' (⇑f) ellipticPointRho') +
      ∑ᶠ (q : NonEllOrbitFM), ordOrbitQ f q =
    ↑k / 12

theorem valence_formula_textbook {k : ℤ}
  (f :
    ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma 1))
      k)
  (hf : f ≠ 0) :
  ↑(orderAtCusp' f) +
          1 / 2 *
            ↑(orderOfVanishingAt' (⇑f)
                ellipticPointI') +
        1 / 3 *
          ↑(orderOfVanishingAt' (⇑f)
              ellipticPointRho') +
      ∑ᶠ (q : NonEllOrbitFM),
        ordOrbitQ f q =
    ↑k / 12

**The Valence Formula** for weight-`k` modular forms on `SL₂(ℤ)`.

For any nonzero modular form `f` of weight `k` for `SL₂(ℤ)`:

$$\operatorname{ord}_\infty(f) + \tfrac{1}{2}\operatorname{ord}_i(f)
+ \tfrac{1}{3}\operatorname{ord}_\rho(f)
+ \sum_{q\;\text{non-ell}} \operatorname{ord}_q(f) = \frac{k}{12}$$

where the sum runs over all non-elliptic `SL₂(ℤ)`-orbits.

Proof for Theorem 7.2

Proof uses 2

Proof dependency previews

Preview

Theorem 5.5

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

The proof is a culmination of the entire Hungerbühler–Wasem apparatus and the orbit machinery. Apply the Hungerbühler–Wasem generalised residue theorem (Theorem 5.5) to the function f'/f around the fundamental-domain boundary \partial \mathcal{D}_H at a sufficiently large height H. The simple poles of f'/f on \mathcal{D} are precisely the zeros of f; the residue of f'/f at a zero of f is the order of vanishing. The Hungerbühler–Wasem identity therefore takes the form \operatorname{PV}_S\!\!\int_{\partial \mathcal{D}_H} \frac{f'(z)}{f(z)}\,\mathrm{d}z \;=\; \sum_{s \in S} 2 \pi i \, \operatorname{gWN}(\partial \mathcal{D}_H, s) \, \operatorname{ord}_{s}(f). The left-hand side is in turn computed by the modular contour integral around the closed boundary \partial \mathcal{D}_H to equal 2\pi i \, (\operatorname{ord}_\infty(f) - k/12) — the textbook contour-integral calculation, in which the top horizontal segment contributes \operatorname{ord}_\infty(f) via the q-expansion, the two vertical edges cancel by T-invariance, and the two arcs are related by S-invariance, summing to -k/12. Equating the two sides and dividing by 2 \pi i gives the PV chain identity that hypothesises Theorem 7.1. The orbit-sum identity of that theorem rewrites the right-hand side as \operatorname{ord}_\infty(f) + \tfrac{1}{2}\operatorname{ord}_i(f) + \tfrac{1}{3}\operatorname{ord}_\rho(f) + \sum_{q \in \mathrm{NonEllOrbit}} \operatorname{ord}_{q}(f) = k/12, which is the textbook valence formula.

Theorem 7.1 Theorem 5.5