Prove full Jacobi–Trudi noncontainment case

[faabian]

Summary

This is a stacked follow-up to facebookresearch#3. It adds the remaining raw-TeX case in which the inner partition is not contained in the outer partition; merge/update PR facebookresearch#3 first.

• defines an unbundled skewSchurFullMN for arbitrary weakly decreasing lam and mu, equal to the existing tableau sum when mu ≤ lam and zero otherwise, matching the source convention that a noncontained shape has no tableaux
• proves the Jacobi–Trudi determinant is zero under noncontainment using the Leibniz expansion and a finite pigeonhole argument
• exposes jacobiTrudi_h_mn_full, with independent row count M and alphabet size N, and no containment hypothesis
• preserves the existing contained-case API

Mathematical argument

Choose k with lam k < mu k. In every determinant summand, a pigeonhole argument gives a selected entry in a row at least k and a column at most k. Weak decrease then makes that complete-homogeneous index negative, hence the entry and the summand vanish. The skew Schur side is zero by the source convention.

Validation

• lake env lean AlgebraicCombinatorics/SymmetricFunctions/JacobiTrudiMN.lean
• lake build (8079 jobs; succeeds; only pre-existing sorry warnings in unrelated/base declarations)
• no new sorry, admit, axioms, unsafe declarations, custom elaborators, or native computation escapes

Diff size

Against the stacked base (codex/jacobi-trudi-m-n): 1 file, +80/-0.

Combined eventual diff against upstream main (including PR facebookresearch#3): 2 files, +970/-87.