LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The boundary arc contribution in the valence computation

Statement

Let $k$ be even and let $0 \neq f \in M_{k}$ . On the unit-circle arc of the fundamental domain (away from the finitely many zeros and poles of $f$ ) one has the identity $d \log f (S τ) = d \log f (τ) + k d τ / τ$ with $S τ = - 1 / τ$ . Consequently, with the boundary orientation used in the argument-principle computation, the circular arc, traversed clockwise from $ω$ to $ω + 1$ , of the positively oriented boundary of the truncated fundamental domain contributes the net amount $π i k / 6$ to $\oint d \log f$ (hence $k / 12$ after division by $2 π i$ ), while the two vertical boundary sides cancel by $T$ -invariance. If zeros lie on the boundary, these contributions mean limits after deleting paired neighbourhoods under $S$ and $T$ ; the small indentation arcs are counted separately.

Facts & Assumptions

Given: Even $k$ , a nonzero modular form $f \in M_{k}$ (Level-one modular forms and cusp forms), and the standard domain $D$ with $S τ = - 1 / τ$ , $T τ = τ + 1$ , the arc being $∣ τ ∣ = 1$ between $ω = e^{2 π i / 3}$ and $ω + 1 = e^{i π / 3}$ through $i$ (The standard fundamental domain, boundary identifications and elliptic stabilisers).

[F1]

$f (S τ) = τ^{k} f (τ)$ for $S = (\begin{matrix} 0 & - 1 \\ 1 & 0 \end{matrix})$ and $f (T τ) = f (τ)$ (Level-one modular forms and cusp forms).

[F2]

Logarithmic derivative and the chain rule: on any region where a holomorphic $g$ has no zeros, $d \log g = g^{'} / g d τ$ ; for $c \neq 0$ , $\frac{d}{d τ} \log f (S τ) = \frac{f^{'} (S τ)}{f (S τ)} \cdot \frac{1}{τ^{2}}$ (The logarithmic derivative of a meromorphic function, The chain rule for complex derivatives, Linearity, product, reciprocal, and quotient rules for complex derivatives).

[F3]

For a closed contour, $\oint d \log f$ is computed by the argument principle; reversal changes the sign, concatenation adds, and $\int_{γ} d τ / τ$ over a contour from $a$ to $b$ equals the increment of a logarithm, in particular $\int_{ω}^{i} d τ / τ = \log i - \log ω$ (The integral of $d z / (z - p)$ along a contour is the increment of a continuous logarithm, Rectifiable complex contours, reversal, concatenation, closedness, and orientation, The contour integral of a constant c is c times the endpoint displacement).

Proof

1.1F1F2givenalgebra

On a neighbourhood avoiding zeros, differentiate $f (S τ) = τ^{k} f (τ)$ and divide by that equality. The chain and product rules [F2] give $\frac{f' (S τ)}{f (S τ)} τ^{- 2} = \frac{f' (τ)}{f (τ)} + k / τ$ , hence $d \log f (S τ) = d \log f (τ) + k d τ / τ$ . No global logarithm of $f$ is required.

2.1F3step 1.1givenalgebra

Let $L$ be the clockwise half-arc $ω \to i$ and $R$ the half-arc $i \to ω + 1$ . Since $S (L)$ is $R$ with reversed orientation, integrating 1.1 gives $- \int_{R} d \log f = \int_{L} d \log f + k \int_{L} d τ / τ$ . Thus $A : = \int_{L} d \log f + \int_{R} d \log f = - k \int_{L} d τ / τ = - k (i π / 2 - 2 π i / 3) = π i k / 6$ , and $A / (2 π i) = k / 12$ . When boundary zeros occur, delete matching subarcs under $S$ ; the same equality holds on the remaining half-arcs, and the omitted integral of $d τ / τ$ tends to zero. In particular it also applies when $i$ or the endpoints are zeros.

3.1F1F3givenalgebra∎

Vertical sides: the right vertical side of the truncated domain is the image under $T$ of the left vertical side, the map being orientation preserving on $H$ ; since $f (T τ) = f (τ)$ the logarithmic derivative is $T$ -invariant, and the two sides are traversed in opposite directions as parts of the boundary, so their contributions to $\oint d \log f$ cancel. Hence the net contribution of the boundary pieces lying on $\partial D$ is the arc contribution $π i k / 6$ .

Depends on

Used by

The level-one valence formula Theorem

Dependency tree · two levels

49 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Modular Functions and Modular Forms (v1.31, 2017) (standard reference, not scraped)
D. Zagier, Elliptic Modular Forms and Their Applications, in The 1-2-3 of Modular Forms (Universitext, Springer, 2008) (standard reference, not scraped)