Theorem 1.1 — Cubic congruence for the q-secant inversion enumerator

Proved

QSecantCubic.cubicCongruence

by ShouqiaoWang · Aug 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

enumerative-combinatoricspermutationspolynomialsq-congruences

Let $A(2n)$ be the set of up--down alternating permutations of $\{1,\ldots,2n\}$ , with the empty permutation included when $n=0$ . For $\sigma\in A(2n)$ , let $\operatorname{inv}(\sigma)$ be its inversion number, and define the $q$ -secant inversion enumerator

E_{2n}(q)=\sum_{\sigma\in A(2n)}q^{\operatorname{inv}(\sigma)}\in\mathbb Z[q].

For every natural number $n$ , prove the polynomial congruence

E_{2n}(q)\equiv q^{2n(n-1)}-\binom n2(1+q)^2 \pmod{(1+q)^3}.

Equivalently, $(1+q)^3$ divides the difference of the two displayed polynomials in $\mathbb Z[q]$ . This is the cubic refinement of the Andrews--Foata congruence and determines the quadratic correction at $q=-1$ .

Formalization Note Permutations use the zero-based type Fin (2*n), and congruence is represented by exact divisibility in Polynomial ℤ. The cases $n=0$ and $n=1$ are included in the single statement.

Preamble

import Definitions.Def_frame_2026_qsecant_interfaces

Formal statement

namespace QSecantCubic

open Polynomial

theorem cubicCongruence (n : ℕ) :
    (1 + X) ^ 3 ∣
      qSecant n -
        (X ^ (2 * n * (n - 1)) -
          C (Nat.choose n 2 : ℤ) * (1 + X) ^ 2) := by sorry

end QSecantCubic

Source

Ji-Cai Liu, A Combinatorial Proof of a Cubic Congruence for the q-Secant Inversion Enumerator, Electronic Journal of Combinatorics 33(3) (2026), P3.10, Theorem 1.1 and congruence (1.4), physical p. 3: https://doi.org/10.37236/15666

View graph