Missing reusable determinant API
We need a Mathlib-shaped determinant recurrence for finite lower-Hessenberg matrices with a variable diagonal, one fixed first superdiagonal, and two varying lower bands. The existing RealRooted.lowerHessenbergTwo_det_recurrence is too specialized: its diagonal is constantly 1, so it cannot represent characteristic-matrix pencils with diagonal entries X - C beta_i.
For a commutative ring R, sequences d a b : Nat -> R, a fixed x : R, and N : Nat, define the N x N matrix indexed by Fin N by
if i.val = j.val then d i.val
else if j.val = i.val + 1 then x
else if i.val = j.val + 1 then a i.val
else if i.val = j.val + 2 then b i.val
else 0
Writing D N for its determinant, the reusable target is
D (n + 3) =
d (n + 2) * D (n + 2) -
a (n + 2) * x * D (n + 1) +
b (n + 2) * x ^ 2 * D nThe expected proof expands the final row. Only the last three entries survive. The final cofactor is the preceding leading section; the penultimate cofactor has determinant x * D (n + 1); and the antepenultimate cofactor has determinant x^2 * D n, obtained by one and two final-column expansions respectively. A useful bounded first milestone is the matrix definition plus these cofactor identities and the determinant recurrence, all over CommRing R. If the full recurrence is unexpectedly tedious, isolate the smallest missing Matrix.det expansion/cofactor lemma instead of introducing a scaffold or admission.
Immediate consumer: OEIS A318107
For the transposed characteristic matrix of the explicit A318107 Hessenberg section, instantiate over R = Real[X] with
d i = X - C (beta i)
x = -1
a i = -C (gamma i)
b i = -C (delta i)
The generic recurrence becomes
D (n + 3) =
(X - C (beta (n + 2))) * D (n + 2) -
C (gamma (n + 2)) * D (n + 1) -
C (delta (n + 2)) * D n.This is exactly the already formalized recurrence for the sign-adjusted monic reversals A318107PosRev. After the three initial ranks and det_transpose, induction identifies A318107PosRev N = (A318107H N).charpoly. The later oscillatory/interlacing step remains separately tracked by #421.
No sorry, axiom, or proposition scaffold should count as completion.
Missing reusable determinant API
We need a Mathlib-shaped determinant recurrence for finite lower-Hessenberg matrices with a variable diagonal, one fixed first superdiagonal, and two varying lower bands. The existing
RealRooted.lowerHessenbergTwo_det_recurrenceis too specialized: its diagonal is constantly1, so it cannot represent characteristic-matrix pencils with diagonal entriesX - C beta_i.For a commutative ring
R, sequencesd a b : Nat -> R, a fixedx : R, andN : Nat, define theN x Nmatrix indexed byFin NbyWriting
D Nfor its determinant, the reusable target isThe expected proof expands the final row. Only the last three entries survive. The final cofactor is the preceding leading section; the penultimate cofactor has determinant
x * D (n + 1); and the antepenultimate cofactor has determinantx^2 * D n, obtained by one and two final-column expansions respectively. A useful bounded first milestone is the matrix definition plus these cofactor identities and the determinant recurrence, all overCommRing R. If the full recurrence is unexpectedly tedious, isolate the smallest missingMatrix.detexpansion/cofactor lemma instead of introducing a scaffold or admission.Immediate consumer: OEIS A318107
For the transposed characteristic matrix of the explicit A318107 Hessenberg section, instantiate over
R = Real[X]withd i = X - C (beta i) x = -1 a i = -C (gamma i) b i = -C (delta i)The generic recurrence becomes
This is exactly the already formalized recurrence for the sign-adjusted monic reversals
A318107PosRev. After the three initial ranks anddet_transpose, induction identifiesA318107PosRev N = (A318107H N).charpoly. The later oscillatory/interlacing step remains separately tracked by #421.No
sorry, axiom, or proposition scaffold should count as completion.