Enrich mvt-oq-02-oq-04: rewrite annotations for S2 retraction stub

[rjwalters]

Summary

The 5 annotations in mean-value-theorem-oq-02-oq-04/annotations.json still described S1 file content that no longer exists after the S2 (2026-05-14) retraction. This PR rewrites them to match the current 128-line doc-only retraction stub.

What was wrong

Old annotation	Old range	Problem
ann-mvt02oq04-uniform-axiom	95–134	Describes the removed S1 axiom block; lines 95–134 of the current file are inside the retraction docstring, not the axiom (which was deleted).
ann-mvt02oq04-zero-corollary	136–167	Describes the removed n = 0 corollary; lines 136–167 don't exist (file ends at line 128).
ann-mvt02oq04-verification	168–173	Describes #check commands that were never in the S2 file; lines 168–173 are past EOF.

The file is now 128 lines: import Mathlib + import Proofs.MeanValueTheoremOQ02 + a 109-line retraction docstring + namespace MeanValueTheoremOQ02OQ04 ... end MeanValueTheoremOQ02OQ04 with a 9-line inline S2 retraction comment between them. No axioms, no theorems, no definitions, no sorries.

New annotations (all ranges in [1, 128])

1. ann-mvt02oq04-imports (1–2): Mathlib + parent import preserved for build closure + structural-kinship documentation.
2. ann-mvt02oq04-retraction-header (4–39): OQ-04 question verbatim, S1 axiom name, child slug Runge counterexample $(1/(1+x^2),,0,,100,,1,,1,,0,,1) \Rightarrow |1/2| > 1/99$, root-cause analysis.
3. ann-mvt02oq04-retraction-action (41–67): S2 retraction action and build-closure soundness argument (a False-derivation would be possible if the refuted axiom remained alongside oq04_axiom_is_false).
4. ann-mvt02oq04-sibling-references (69–102): parent (Lagrange remainder, unchanged), child (refutation + corrected complex-disk form), cousin taylor-theorem-oq-02 (qualitative $R_n \to 0$, Runge-robust).
5. ann-mvt02oq04-empty-namespace (104–128): References block (Runge 1901, child slug §2/§3) + empty namespace with inline S2 comment.

All 5 carry mathContext, significance, relatedConcepts, prerequisites. No annotation now references a line outside the actual file.

Test plan

• JSON validates (python3 -c 'json.load(open(path))')
• All 5 annotation range.endLine values $\le 128$ (current wc -l).
• No annotations.source.json exists, so this file is the source of truth (per [[project_annotations_source_vs_generated_drift]]).
• pnpm build blocked locally on better-sqlite3 native rebuild (node v26 vs node-gyp); JSON-only change is structurally safe.

[rjwalters]

Closing as duplicate of #21867 (enricher-1, 2026-06-01 07:41) which already includes the annotations.json rewrite with overlapping line ranges (1-2, 4-13, 14-39, 41-67, 69-100, 101-128) — comparable retraction-stub-appropriate content, 6 annotations vs my 5. I missed the prior PR in my pre-create search; closing in favor of the earlier PR.