ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30

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 cotangent expansion computes $\sum_{n \in Z} 1 / (n^{2} + a^{2})$

Example

If $a \in C$ and $a \notin i Z$ , then

$\sum_{n \in Z} \frac{1}{n^{2} + a^{2}} = \frac{π}{a} \coth (π a) .$

Facts & Assumptions

Given: A complex number $a \notin i Z$ .

[L1]

For $z \notin Z$ , $π \cot (π z) = \sum_{n \in Z} 1 / (z - n)$ in the symmetric Mittag-Leffler sense (The Mittag-Leffler expansion of pi cotangent).

Verification

technique · direct

1.1

Substitute $z = i a$ into [L1]. Since $\frac{1}{i a - n} = \frac{- i a - n}{n^{2} + a^{2}},$ the terms for $n$ and $- n$ combine to $- 2 i a / (n^{2} + a^{2})$ , while the $n = 0$ term is $1 / (i a)$ .

L1givenalgebra

2.1

Thus $π \cot (π i a) = \frac{1}{i a} - 2 i a \sum_{n \geq 1} \frac{1}{n^{2} + a^{2}} = - i a \sum_{n \in Z} \frac{1}{n^{2} + a^{2}} .$ Using $\cot (i w) = - i \coth (w)$ and dividing by $- i a$ gives the displayed closed form.

step 1.1algebra∎

Depends on

The Mittag-Leffler expansion of pi cotangent

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

M. Weber, Complex Analysis, Example 3.3.1 (standard reference, not scraped)

The cotangent expansion computes ∑n∈Z1/(n2+a2)∑n∈Z​1/(n2+a2)