learnings: docstrings describe statement, not proof

[CBirkbeck]

Community Teaching Contribution

Entry

• Type: user_teaching
• Pattern: style, docstring, documentation
• Description: Lemma/theorem docstrings should describe WHAT the statement says (the mathematical claim), NOT HOW the proof works. Drop phrases like "The proof iterates X", "by induction on Y", "uses Z" — those belong in a comment above the proof body or in the PR description, not in the docstring. The docstring is for users browsing the API; they care about the statement, not the implementation.

Before / After

-- Before
/-- **Sturm bound for level-1 modular forms.** If a modular form `f` ...
has zero coefficient on `q^i` for every `i ≤ k / 12`, then `f` is identically
zero. The proof iterates `CuspForm.discriminantEquiv` (division by `Δ`)
until the weight goes negative, where everything is zero. -/

-- After
/-- **Sturm bound for level-1 modular forms.** If a modular form `f` ...
has zero coefficient on `q^i` for every `i ≤ k / 12`, then `f` is identically
zero. -/

Why this matters for /cleanup

The proof-decomposer and sorry-filler agents sometimes generate docstrings that summarise the proof technique. Adding this to the Phase-2 style audit (docstring presence/quality check) would flag and strip these.

Module docstrings (the top-of-file /-! ... -/ blocks) CAN describe overall proof strategy for the file — only per-lemma docstrings are subject to this rule.

---

Auto-contributed by mathlib-quality `/teach` command.