Enrich mean-value-theorem-oq-02-oq-04: fix stale post-retraction annotations

[rjwalters]

Summary

Cleanup of mean-value-theorem-oq-02-oq-04 after the S2 retraction (researcher-8, 2026-05-14). Two related improvements:

1. Stale post-retraction annotations (commit 1)

S2 removed the false S1 axiom analytic_taylor_remainder_uniform_bound and its false-by-inheritance n=0 corollary analytic_remainder_zero_bound from Proofs/MeanValueTheoremOQ02OQ04.lean, leaving just a docstring + empty namespace (128 lines). The annotations.json was never updated and still pointed at lines 95-173 — including the deleted axiom (95-134), corollary (136-167), and a #check verification block (168-173) that no longer exist.

Rewrote all annotations to match the actual file. 7 annotations (was 5), all with mathContext, significance, relatedConcepts, prerequisites:

1. Imports (1-2): Mathlib + parent OQ-02 file
2. OQ-04 question (4-12): the open question as originally posed; pedagogical motivation; the real-vs-complex ambiguity in "disk of radius R" that S1 missed
3. Runge counterexample (14-39): mathematical refutation at $(f, a, R, M, r, n, x) = (1/(1+x^2), 0, 100, 1, 1, 0, 1)$; LHS=1/2, RHS=1/99; named the Runge phenomenon (Runge 1901)
4. S2 action (41-67): what was removed and the False-witness hazard the deletion closed (any consumer importing both this file and the child slug's refutation could otherwise derive False)
5. Bookkeeping + family (69-102): axiomCount: 1 → 0, sibling slug tree, the (a)-vs-(b) path-forward decision to keep the file as a doc-only retraction record
6. References (104-111): Runge 1901 and pointer to the corrected complex-disk statement analytic_taylor_remainder_uniform_bound_complex
7. Empty namespace (114-128): retraction made concrete; three reasons the namespace is kept (import stability, identifier reservation, gallery slug stability)

2. Split docstring into 8 sections (commit 2)

The retracted file is mostly a docstring (lines 4-111), previously summarized as a single "header-and-imports" section covering lines 1-112. That collapsed six logically-distinct passages into one opaque block.

New sections array: 8 entries (was 2) — imports, six docstring sub-sections, and namespace-setup. Each section's summary records the substantive content of that passage rather than just "this is part of the docstring."

Quality score

94 → 100 (sections subscore 4 → 10; annotations subscore unchanged at 25/25 with all required fields populated).

Test plan

• jq -e . validates both meta.json and annotations.json
• pnpm annotations:build reports zero errors for this slug
• All annotation range values fall within the file's 128 lines
• All section startLine/endLine values fall within the file's 128 lines
• find-targets.ts confirms quality score = 100 after both commits

🤖 Generated with Claude Code