[refactor][P0] Reuse generic banded-Hessenberg determinants in the array-polynomial recurrence

[PerAlexandersson]

Planning issue from the 2026-09-08 source audit of current main (cfa0179b). This proposes refactoring existing checked mathematics; no Lean changes or new build verification were performed for the survey.

Problem and evidence

RealRooted/ArrayPolynomialDeterminantRecurrence.lean:39 repeats the exact last-column Laplace-expansion proof in RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/BandedHessenberg.lean:43. The duplication extends to penultimate/antepenultimate cofactor calculations and the final recurrence (application:190, generic:201).

The generic shim is 286 lines with a two-module local closure. The 272-line application currently has a 102-module closure and does not consume that generic recurrence. We should specialize the generic theorem rather than maintain parallel cofactor proofs.

The generic variable-diagonal recurrence was already delivered by #425 / PR #427.
This issue only routes the array-polynomial specialization through that existing API.

Exact bridge to check first

-- Proposed bridge; exact indexing follows the two source definitions.
theorem lowerHessenbergTwo_eq_bandedLowerHessenberg
    {R : Type*} [CommRing R] (a b : ℕ → R) (x : R) (n : ℕ) :
    lowerHessenbergTwo a b x n =
      Matrix.bandedLowerHessenberg
        (fun _ => 1) (fun i => -a (i + 1)) (fun i => b (i + 1)) x n := by
  ...

Specializing Matrix.det_bandedLowerHessenberg_add_three through this bridge gives
the application's positive a (n+3) * x term from the generic
-a (n+2) * x term. The index shift and sign are acceptance-critical.

Staged plan and shared ownership

1. Prove the matrix equality entrywise, then reprove only lowerHessenbergTwo_det_recurrence from the generic endpoint. This is the smallest useful checkpoint.
2. Move the last-column expansion to the existing
   RealRooted/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
   in namespace Matrix, under a name such as
   det_eq_last_mul_det_submatrix_of_lastColumn_above_eq_zero.
   Keep RealRooted.det_eq_last_apply_mul_det_castSucc as a compatibility wrapper.
   Check Mathlib's determinant/block-triangular API before introducing a new theorem.
3. Audit consumers of all public application cofactor definitions and lemmas.
   Preserve their names/statement shapes; express them through the generic machinery
   where doing so eliminates meaningful duplication.
4. Keep generic cofactor helpers private unless an actual second consumer needs
   them. Do not expose the entire implementation merely to reduce application lines.
5. Review whether the application needs both ArrayPolynomialDeterminant and
   ArrayPolynomialWeights after specialization. Use the smallest imports;
   retain a compatibility facade if narrowing would otherwise remove established exports.

Validation

Build the generic Basic/BandedHessenberg shims, the recurrence module, and
ArrayPolynomialDeterminantIdentification. Include direct bridge and recurrence
checks at n = 0 and n = 1, arbitrary commutative rings, and characteristic two;
the proof must not require order, division, or nonzero x. Keep the empty determinant
convention and all Fin.castSucc indexing intact.

Validation and completion

Keep public declaration names, named arguments, attributes, and old module imports compatible. Run focused builds and affected consumers with the designated sole Lean worker, then the full integration build. Run the root-import, import-architecture, proof-status, and OEIS-coverage guards, plus git diff --check. Audit representative moved endpoints with #print axioms; no new proof assumptions or warning suppression. Keep mechanical moves and proof golfing in separate commits.

[PerAlexandersson]

Resolved on main by 0191f4b and 83eec48 (included in a485baa). lowerHessenbergTwo_det_recurrence now specializes Matrix.det_bandedLowerHessenberg_add_three through the checked matrix bridge, with the required shifted indices and signs. The last-column determinant proof has one Matrix owner in the determinant Basic shim; the old RealRooted name is a compatibility wrapper. Public cofactor APIs remain intact. Statements retain arbitrary CommRing, all n (including 0 and 1), and no order/division/nonzero-x assumption, so characteristic two is included. The designated builder passed focused owner/application/identification checks, standard-only axiom audits, guards, and the 9,545-job integrated full build. GitHub CI for the latest published checkpoint is running.