Annular Obstructions and Skew-Shape Block Identities
Adam Tilèpe
math.CO
Nov 10, 2026 · v2
TL;DR
A companion Lean 4/Mathlib development formalizes the order-ideal specializations, the annular mutation counterexample polynomials, the tableau-transfer matrix lemmas, and the skew-shape block-statistic identity.
Abstract
We give three principal results on weighted order ideals, cluster coefficients, and block-statistic enumerators. First, in the rank-two annular exchange model, the frozen row $(2,-3)$ yields the specialized polynomial $1+q^2$, which is not unimodal. Its interpretation as a single-lamination counterexample to Theorem 14 of Kang, Lee and Lim (European Journal of Combinatorics, 2026) depends on identifying this row with the shear coordinates of a bridging curve in the same triangulation. We discuss this geometric correspondence using published annular examples; it is not established by the algebraic calculation or formalized in Lean. Second, the same polynomial fails log-concavity, and the frozen row $(1,-2)$ gives the full-support polynomial $1+2q+7q^2+10q^3+9q^4+4q^5+q^6$, likewise violating log-concavity. These calculations provide obstructions relevant to their Conjecture 1, subject to the same geometric identification. Third, for arbitrary finite skew Young diagrams, we prove the block-statistic identity of Kahane's Conjecture 4.7 (arXiv:2607.11225v2), using an explicit correction of the root convention. The proof uses commuting tableau-transfer matrices, a connected-block inverse kernel, and finite polynomial differential equations, with companion Lean 4/Mathlib formalizations. As a consequence, we obtain a bivariate block refinement that is coefficientwise nonnegative in $t-1$ after a common monomial shift in $q$.
Problem
Kang, Lee and Lim asserted that single-lamination specialized cluster c-polynomials are unimodal and conjectured that they are log-concave. Kahane conjectured a block-statistic identity relating labelings of skew Young diagrams to order polynomials.
Approach
A bivariate enumerator over weighted order ideals links the two settings. In the rank-two annular exchange model, explicit mutations with frozen rows taken from Felikson–Tumarkin's bridging curves yield candidate obstructions. For skew shapes, the proof uses commuting tableau-transfer matrices, a vertical-strip inverse kernel, and finite polynomial matrix differential equations, under a root-excluded block convention. The statements are mapped to named declarations in a Lean 4/Mathlib file, and an axiom audit is reported.
Results
The frozen row (2,-3) gives 1+q^2, which is neither unimodal nor log-concave. The row (1,-2) gives a full-support polynomial that fails log-concavity. Both count as counterexamples only if the rows are the shear coordinates of bridging curves, which is not formalized. Kahane's Conjecture 4.7 is proved for all finite skew diagrams, with a bivariate refinement nonnegative in t-1, and Lean checks it using only the standard axioms.
