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

Open

QSecantCubic.cubicCongruence

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

Theorems.QSecantCubic / QSecantCubic.cubicCongruence

For every natural number $n$ , let

E_{2n}(X)= \sum_{\substack{\sigma\in S_{2n}\\ \sigma(0)<\sigma(1)>\sigma(2)<\sigma(3)>\cdots}} X^{\operatorname{inv}(\sigma)},

where the displayed alternation means precisely that every adjacent comparison with even zero-based index is a rise and every one with odd index is a fall, and $\operatorname{inv}(\sigma)$ counts pairs $i<j$ with $\sigma(j)<\sigma(i)$ . The theorem asserts exact divisibility in $\mathbb Z[X]$ :

(1+X)^3\mid E_{2n}(X)- \left( X^{\,2n(n-1)} -\binom n2(1+X)^2 \right).

Here $n-1$ is natural-number subtraction, hence is truncated to $0$ at $n=0$ , and $\binom n2$ is coerced from $\mathbb N$ to the integer constant polynomial. Equivalently, the literal divisibility claim is that for every $n$ there exists $H_n(X)\in\mathbb Z[X]$ such that

E_{2n}(X)-X^{\,2n(n-1)} +\binom n2(1+X)^2=(1+X)^3H_n(X).

There are no hypotheses on $n$ , so the statement is not vacuous. At $n=0$ , $E_0(X)=1$ , the exponent is $0$ , and the binomial coefficient is $0$ , making the dividend $0$ . At $n=1$ , the sole up-down permutation of two elements is the identity, so $E_2(X)=1$ , the exponent is again $0$ , and the binomial coefficient is $0$ , making that dividend $0$ as well.

Human review

Endorsed by Shuze Chen · Aug 26, 2026
Endorsed by ShouqiaoWang · Aug 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph