Bounded positivity of stretched Littlewood--Richardson polynomials

This repository gives an exact computer-assisted proof that no negative monomial coefficient occurs for a stretched Littlewood--Richardson polynomial when all three partitions have length at most 7 and weight at most 30.

The motivating FrontierMath problem asks for a counterexample in precisely this box. The computation disproves the existence of such a counterexample; it does not prove the unrestricted King--Tollu--Toumazet conjecture.

Theorem verified

For integer partitions lambda, mu, and nu satisfying

len(lambda), len(mu), len(nu) <= 7
sum(lambda) = sum(mu) + sum(nu)
sum(lambda) <= 30

every coefficient of

P(t) = c^(t lambda)_(t mu,t nu)

in the monomial basis is nonnegative.

The unrestricted balanced domain contains 1,608,330,363 ordered triples (including the all-empty triple). Exact reductions, together with a deliberately unreduced rank-5 pass, leave 4,171,999 primitive rank-5--7 cases to evaluate. A further 679,873 low-rank cases with P(1) >= 3 are directly interpolated, so a full replay explicitly coefficient-checks 4,851,872 polynomial cases.

Effective rank	Primitive cases evaluated	Engine
5	1,261,039	direct lrcalc values, rational interpolation
6	1,640,377	exact LR-triangle Ehrhart series
7	1,270,583	exact LR-triangle Ehrhart series
Total	4,171,999

Counts by rank and outer weight are frozen in results/certified_census.json; the full raw domain count is in results/domain_census.json.

Reproduce

The supported environment is CPython 3.11 or newer on macOS or Linux.

./setup.sh
./verify.sh

./verify.sh is deliberately the full multi-hour replay. It runs the unit tests and independent checks first, then launches four deterministic shards per high rank. Change the process count with SHARDS=8 ./verify.sh.

For a quick installation and logic check suitable for continuous integration:

./setup.sh
./verify.sh --quick

The full command writes machine-readable runtime and software-version data to results/full_verification.json and complete per-shard logs to results/logs/. It fails on any missing shard, count mismatch, time limit, nonzero exit, or negative coefficient.

After a successful reference run, its report and logs can be frozen with their source commit and individual SHA-256 hashes using python scripts/freeze_full_verification.py --source-commit COMMIT.

To build and visually inspect the paper locally:

./paper/build.sh
./paper/package_arxiv.sh

The paper build uses Tectonic when available, with latexmk as a fallback.

Why the enumeration is complete

The proof separates mathematical reductions from direct calculation:

1. Iterated determinant normalization preserves the whole stretched polynomial and lowers rank or weight.
2. Cases with P(1) equal to 0, 1, or 2 follow respectively from saturation, the multiplicity-one theorem, and Ikenmeyer's multiplicity-two theorem.
3. The S_3 symmetry of the associated SL(n) invariant multiplicity selects one canonical representative; it commutes with stretching.
4. Equality on an essential Horn facet factors the entire stretched polynomial into lower-rank stretched LR polynomials. Strict Horn interiors are the only primitive cases.
5. Every low-rank P(1) >= 3 case in the finite box is also checked directly, so the bounded theorem does not depend on the recent general rank-four preprint.

The generator produces 3, 12, 41, 142, 521, and 2,042 essential Horn inequalities in ranks 2 through 7. Small-box tests independently verify coproduct completeness, repeated determinant normalization, orbit invariance, Horn slack signs, and routing into a primitive or lower-rank case. The detailed audit is in AUDIT.md.

Exact arithmetic and degree

An LR triangle with rank n has affine dimension at most D_n = binom(n-1,2). In ranks at most 5, integer LR values P(0),...,P(D_n) are evaluated directly. In ranks 6 and 7, Normaliz supplies the exact affine dimension and exact Ehrhart values. Production interpolation uses finite differences over Python Fraction; an independent verifier solves the Vandermonde system over the rationals. Floating point is never used for a coefficient or sign decision. NumPy is used only for bounded integer subset-sum tables (all entries are at most 30).

Closest case found

The minimum coefficient including absent terms is zero. The least strictly positive monomial coefficient among the primitive polynomials checked is

1/119750400

for

lambda_ = [9, 8, 6, 3, 2, 1, 1]
mu      = [5, 4, 3, 2, 1]
nu      = [5, 4, 3, 2, 1]

The full coefficient vector and direct values are in results/certificate.json. Searches of the exact fraction, triple, and related literature found no prior published tabulation; the paper therefore records this as a reproducible finite-range statistic, not as a claim of literature-wide novelty or a universal lower bound.

Independent verification

• independent_lr.py is a dependency-free LR-tableau backtracker, separate from both lrcalc and the LR-triangle model.
• verify_certificate.py compares Normaliz Ehrhart values with direct stretched LR values on fixed cases and 100 deterministic random cases.
• tests/test_core.py contains exhaustive small-box and cross-engine tests.
• MANIFEST.sha256 covers the proof source, scripts, tests, paper source, and frozen result summaries.
• results/release_artifacts.json records deterministic SHA-256 hashes for the locally generated PDF and arXiv bundle.

Paper and status

The preprint is authored by Ramiz Arda Ünal. Source is in paper/; the arXiv source bundle is generated by paper/package_arxiv.sh.

Public repository: https://github.com/RamizUnal/stretched-lr-positivity

This is currently an exact computational result awaiting independent human review and archival publication. Do not describe it as peer reviewed or published until a journal has accepted it. Epoch explicitly says that a bounded nonexistence claim cannot be handled by its construction verifier and must be settled through the ordinary mathematical process.

Primary sources

• Derksen and Weyman, On the Littlewood--Richardson polynomials, Journal of Algebra (2002).
• Knutson and Tao, saturation, JAMS (1999).
• Knutson, Tao, and Woodward, Horn facets and multiplicity one, JAMS (2004).
• King, Tollu, and Toumazet, Horn-boundary factorization, JCTA (2009).
• Ikenmeyer, multiplicity two, J. Algebraic Combinatorics (2016).
• Pak and Vallejo, LR triangles, European J. Combinatorics (2005).

License and citation

The code is released under the MIT License. Citation metadata is provided in CITATION.cff. The paper remains copyright Ramiz Arda Ünal.