feat(matrix): derive irreducibility from adjacent positivity

[PerAlexandersson]

Progresses #421 with the first upstream-shaped graph-theoretic leaf of the classical oscillatory-matrix criterion.

This PR adds only RealRooted/Mathlib/LinearAlgebra/Matrix/Oscillatory.lean. It proves:

• Matrix.isIrreducible_of_nonneg_of_adjacent_pos for a nonnegative finite-chain matrix with positive adjacent sub- and superdiagonals;
• Matrix.IsTotallyNonneg.isIrreducible_of_det_ne_zero_of_adjacent_pos, including the one-dimensional endpoint.

This exposes the existing Perron/primitive APIs without claiming the still-missing Whitney reduction or Gantmacher--Krein nodal theorem. The latter remains the formalization boundary needed for the full principal-section interlacing result discussed in #421 and PR #423.

The RealRooted.lean umbrella import is deliberately deferred because PRs #426 and #427 currently own that overlapping file.

Verification performed before publication:

• focused lake-workspace build of RealRooted.Mathlib.LinearAlgebra.Matrix.Oscillatory passed (2972 jobs);
• proof-status self-test and full scan passed;
• both public theorems depend only on propext, Classical.choice, and Quot.sound;
• git diff --check and the 100-column audit passed.