Add banded lower-Hessenberg determinant recurrence

[PerAlexandersson]

Summary

• define Matrix.bandedLowerHessenberg over an arbitrary commutative ring, with variable diagonal, fixed first superdiagonal, and two varying lower bands
• prove Matrix.det_bandedLowerHessenberg_add_three by final-row expansion, with private cofactor reductions for the two lower bands
• expose the definition across the Lean module boundary and add the single sorted umbrella import

The public recurrence is

det B(n + 3) =
  d(n + 2) * det B(n + 2) -
  a(n + 2) * x * det B(n + 1) +
  b(n + 2) * x ^ 2 * det B(n)

This is the reusable determinant milestone for #425. It does not close the issue or any later analytic/interlacing work.

Verification

• AXLE Lean 4.31 final-file check: zero errors, warnings, or failed declarations; all linters passed (request d97dd57d-d7c7-401b-9a7b-5c492d96e8af)
• lake-workspace build RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.BandedHessenberg: 2,967 jobs passed; the target emitted no Lean warnings
• lake-workspace build RealRooted: 9,026 jobs passed
• the full replay displayed pre-existing warnings in unrelated compound-spectrum, Perron–Frobenius, Gantmacher–Krein, and TN-charpoly modules; none came from the new module
• scripts/check_root_imports.py: all 467 modules imported
• generated OEIS coverage check passed
• proof-status self-test and project audit passed: no sorry, admit, source axioms, or unclassified low-use statements
• direct axiom audit: bandedLowerHessenberg_apply uses only Quot.sound; det_bandedLowerHessenberg_add_three uses only propext, Classical.choice, and Quot.sound
• committed-range diff check, 100-column check, and forbidden-source-token check passed

Refs #425.