Enrich mean-value-theorem-oq-02-oq-04: align retraction stub

[rjwalters]

Summary

This entry is a doc-only retraction stub (S2, 2026-05-14) for the false S1 axiom analytic_taylor_remainder_uniform_bound, refuted by the Runge counterexample in the child slug. Its annotations and meta still described the removed axiom/theorem/check block as if present. This PR aligns the gallery entry with the current 128-line Lean file.

Changes

• annotations.json: rewritten from 5 stale entries (pointing at lines 95-173 of the pre-retraction file) to 6 entries aligned to the actual file: imports + post-retraction rationale, OQ-04 verbatim, Runge refutation + complex-radius-of-convergence root cause, S2 action with explicit soundness threat model (False-witness in build closure), bookkeeping + sibling links, empty namespace + API stability.
• meta.json:
  • Added missing cross-reference to child slug mean-value-theorem-oq-02-oq-04-oq-01 (carries both the refutation and the corrected complex-disk form).
  • Rewrote conclusion.summary to lead with RETRACTED + Runge witness (was "Cauchy's bound is axiomatized as ..." — misleading post-retraction).
  • Rewrote openQuestions to reflect resolved status: Q1 closed negatively (S1 axiom is false), Q2 closed positively modulo one sub-lemma, Q3 points to remaining sub-lemma, Q4 covers extensions.
• index.ts: wire Lean source via ?raw import so the retraction docstring is visible on the gallery page (was source: '').

Validation

• tsc --noEmit clean (using main repo's node_modules; worktree's better-sqlite3 fails to build).
• JSON.parse OK on both .json files.
• Verified all four cross-reference targets exist (mean-value-theorem-oq-02, mean-value-theorem-oq-02-oq-04-oq-01, taylor-theorem-oq-02, mean-value-theorem, taylor-sincos-convergence).

Test plan

• Gallery page renders retraction docstring + new annotations
• Child-correction cross-reference link resolves on the live site

[rjwalters]

Cross-reference: PR #21861 (created 28 min earlier) also rewrites annotations.json for this entry (7 annotations vs my 6). This PR's unique contributions vs #21861:

1. index.ts source wiring — source: '' → ?raw import so the retraction docstring renders on the gallery page.
2. meta.json conclusion.summary — was "Cauchy's bound is axiomatized as ..." (misleading post-retraction); rewritten to lead with RETRACTED + Runge witness.
3. meta.json openQuestions — was four "can S2 discharge ..." questions framed as if axiom were still active; rewritten to reflect resolved status (Q1 closed negatively, Q2 closed positively modulo one sub-lemma).
4. meta.json cross-reference to child slug mean-value-theorem-oq-02-oq-04-oq-01 — the most important sibling (carries refutation + corrected complex-disk form) was missing entirely from crossReferences.

PR #21858 (leanFile + relatedProblems) is orthogonal to both this PR and #21861.

If #21861 merges first, this PR's annotations.json will conflict — the index.ts / meta.json (sections 2–4 above) contributions are still independently useful and can be cherry-picked.