fix(meta): cayley-hamilton-minpoly-oq-04 register Backward orphan

[rjwalters]

Fix

Register Proofs/CayleyHamiltonMinpolyOQ04Backward.lean (480 LOC, 1 sorry, 0 axioms) as an additionalFile for the cayley-hamilton-minpoly-oq-04 slug. The file was an unregistered orphan; only its Aristotle companion (...BackwardAristotle.lean) was previously registered.

Evidence

Before — both meta.additionalFiles and leanFile.additionalFiles listed only the Aristotle companion:

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

After — both fields list both companions:

"additionalFiles": [
  "Proofs/CayleyHamiltonMinpolyOQ04Backward.lean",
  "Proofs/CayleyHamiltonMinpolyOQ04BackwardAristotle.lean"
]

Provenance — CayleyHamiltonMinpolyOQ04Backward.lean declares itself the Backward Direction: Nonderogatory → Cyclic Vector (Infinite Fields) continuation of cayley-hamilton-minpoly-oq-04. From its docstring:

Theorem: Over an infinite field K, if M ∈ M_n(K) is nonderogatory (minpoly = charpoly), then M has a cyclic vector. This eliminates the axiom from CayleyHamiltonMinpolyOQ04.lean for all infinite fields, which includes all algebraically closed fields.

It implements the third of the three approaches listed in the slug's keyInsights[4] ("union of proper subspaces (infinite fields only)").

Sorry/axiom disclosure — the file contains 1 sorry (line 372, nonderogatory_has_cyclic_vector_infinite) — an API integration issue with Mathlib.RingTheory.UniqueFactorizationDomain.Basic (whose import breaks DecidableEq resolution in the rest of the file). The mathematical proof is documented in the surrounding comments. 8 supporting lemmas are fully proved (e.g. aeval_ne_zero_of_ne_zero, not_union_proper_subspaces, powers_linearIndependent, gcd_aeval_mulVec_eq_zero).

This registration does not alter the primary file (Proofs/CayleyHamiltonMinpolyOQ04.lean, 316 LOC, 0 sorries, 1 axiom) and its top-level meta.sorries: 0 / meta.axiomCount: 1 claims remain accurate for the canonical proof. Auditor scans proofRepoPath by default; the companion's sorry remains separately tracked.

Both fields updated together per the mirror convention (PRs #21818 / #21816 / #21817 / #21819 / #21829 / #21831 / #21835 / #21836 / #21838 / #21893 / #21894 / #21895 / #21897 / #21899 / #21901 / #21903 / #21904).

---

Automated fix by lean-mechanic agent.