fix(meta): mvt-oq-02-oq-04 strings in meta.additionalFiles

[rjwalters]

Fix

Convert meta.additionalFiles rich {path, purpose} entry to a plain string so the auditor follows the companion file.

Evidence

Before:

"additionalFiles": [
  {
    "path": "Proofs/MeanValueTheoremOQ02.lean",
    "purpose": "Parent file providing taylorPolynomial..."
  }
]

After:

"additionalFiles": [
  "Proofs/MeanValueTheoremOQ02.lean"
]

Why

scripts/auditor/find-targets.ts:169 skips non-string entries:

for (const af of additionalFiles) {
  if (typeof af !== 'string') continue
  ...
}

Rich-object meta entries silently disable chain-aggregate axiom/sorry counting. The slug claims axiomCount: 1 (inherited from the parent's taylor_lagrange_remainder); with the swap the auditor will correctly aggregate 0 (main) + 1 (parent) = 1 matching the claim.

Same pattern as PR #21874 (child slug mean-value-theorem-oq-02-oq-04-oq-01) and PR #21863 (picks-theorem-oq-03).

The purpose narrative is already preserved in this slug's assumptions, originalContributions, and description fields.

Validation

• jq -e . passes
• npx tsx scripts/auditor/find-targets.ts --issues --json returns [] (no new flags)
• Mirror-direction scan (meta.additionalFiles strings vs leanFile.additionalFiles) unchanged for this slug (leanFile is null here; PR Enrich mean-value-theorem-oq-02-oq-04: populate leanFile + relatedProblems #21858 is adding the leanFile object separately).

Concurrent PRs touching this slug

• Enrich mean-value-theorem-oq-02-oq-04: populate leanFile + relatedProblems #21858 (enricher: leanFile + relatedProblems) — touches lines ~54–72 + end-of-file
• Enrich mean-value-theorem-oq-02-oq-04: fix stale post-retraction annotations #21861 (enricher: stale annotations) — touches lines ~123–180
• Enrich mean-value-theorem-oq-02-oq-04: align retraction stub #21867 (enricher: retraction stub) — touches lines ~1–22 (index.ts/annotations.json) and ~138+ (conclusion)

This PR touches lines 43–50 only (the additionalFiles array). No line overlap.

---

Automated fix by lean-mechanic agent.