Enrich mvt-oq-02-oq-04: align meta with S2 retraction state

[rjwalters]

Summary

The S2 (2026-05-14) retraction of mean-value-theorem-oq-02-oq-04 (PR #21806 fixed sections 5→2) left several other meta fields still describing the pre-retraction S1 state. This PR aligns them with reality.

What was misaligned

The Lean file is now a 128-line doc-only stub: 0 axioms, 0 theorems, 0 sorries — the false OQ-04 axiom was retracted after the child slug mean-value-theorem-oq-02-oq-04-oq-01 proved it false via Runge counterexample. But:

1. crossReferences did not include the child slug — the single most important link for this entry, since the child carries both the refutation (oq04_axiom_is_false) and the corrected complex-disk replacement (analytic_taylor_remainder_uniform_bound_complex).
2. conclusion.summary said "first research session for the slug (prior knowledge tier: EMPTY)" — S1 framing.
3. conclusion.implications had a "Resolving the axiom" paragraph laying out the discharge path, treating the axiom as pending rather than refuted.
4. conclusion.openQuestions Q1/Q2 asked how to prove / specialize a now-refuted axiom.
5. meta.originalContributions claimed the false axiom as a contribution.

Changes (single file, 14 insertions / 9 deletions)

• crossReferences[1]: add mean-value-theorem-oq-02-oq-04-oq-01 with relationship: "child-refutation-and-corrected-form".
• conclusion.summary: rewrite to describe S2 retraction state (128 lines, 0 axioms in this file, 1 inherited axiom from parent via additionalFiles).
• conclusion.implications: replace "Resolving the axiom" content with three substantive paragraphs: Runge-phenomenon-as-auditing-tool framing, complex-disk essentiality, formalization-process robustness.
• conclusion.openQuestions: drop Q1/Q2 (proving a refuted axiom), redirect Q1 to the corrected complex-disk form in the child slug, add three forward-looking questions (parameterized counterexample family, bounded-derivative Bernstein analog, distance-from-real hierarchy).
• meta.originalContributions: rewrite as "S2 retraction record" + Runge root-cause identification + cross-reference manifold.

Test plan

• JSON validates (python3 -c 'json.load(open(path))')
• crossReferences count: 4 → 5
• lineCount unchanged (128, matches wc -l proofs/Proofs/MeanValueTheoremOQ02OQ04.lean)
• No semantic changes to the Lean file or to the mainTheorems retraction records (which already correctly labeled the axiom as RETRACTED in PR fix(meta): mvt-oq-02-oq-04 retraction-stub sections (5→2) #21806)
• pnpm build is 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 covers the same retraction-coherence work on meta.json — same child cross-reference, same conclusion/summary/openQuestions rewrites — and also includes the corresponding annotations.json rewrite (covered separately by my #21872, now also closed) and an index.ts ?raw source wiring. I missed the prior PR in my pre-create search; closing this in favor of the earlier, more comprehensive PR.