q-Secant inversion-enumerator interfaces

Definition

frame_2026_qsecant_interfaces

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

enumerative-combinatoricspermutationspolynomialsq-analogues

This definition bundle formalizes up--down permutations of Fin (2*n), their inversion numbers, the integer-polynomial $q$ -secant enumerator, and polynomial congruence as divisibility. It fixes the empty-permutation convention at $n=0$ and supplies the transparent objects used by the cubic-congruence mission.

Definition code

import Mathlib

/-!
# Concrete definitions for the q-secant inversion enumerator

These declarations are separated from the open theorem so that a Prove2me
proposal can publish the definitions before presenting the congruence as its
goal item.
-/

namespace QSecantCubic

open Polynomial

/-- A zero-based version of the paper's up-down condition
`sigma_1 < sigma_2 > sigma_3 < sigma_4 > ...`. -/
def IsUpDown {m : ℕ} (sigma : Equiv.Perm (Fin m)) : Prop :=
  ∀ (i : ℕ) (hi : i + 1 < m),
    if Even i then
      sigma ⟨i, Nat.lt_of_succ_lt hi⟩ < sigma ⟨i + 1, hi⟩
    else
      sigma ⟨i + 1, hi⟩ < sigma ⟨i, Nat.lt_of_succ_lt hi⟩

/-- Number of inversions of a permutation. -/
def inversionNumber {m : ℕ} (sigma : Equiv.Perm (Fin m)) : ℕ :=
  ((Finset.univ : Finset (Fin m × Fin m)).filter
    (fun ij => ij.1 < ij.2 ∧ sigma ij.2 < sigma ij.1)).card

/-- The q-secant inversion enumerator `E_{2n}(q)` in `Z[q]`. -/
noncomputable def qSecant (n : ℕ) : Polynomial ℤ := by
  classical
  exact
    ((Finset.univ : Finset (Equiv.Perm (Fin (2 * n)))).filter
      IsUpDown).sum
      (fun sigma => Polynomial.X ^ inversionNumber sigma)

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, DOI 10.37236/15666, definitions in Eq. (1.2) and Theorem 1.1 on physical p. 3: https://doi.org/10.37236/15666

Read-back

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

Definitions.QSecantInterfaces / definition bundle

QSecantCubic.IsUpDown. For $m\in\mathbb N$ and a permutation $\sigma$ of $\{0,\ldots,m-1\}$ , this says that for every $i\in\mathbb N$ together with a proof that $i+1<m$ , one has $\sigma(i)<\sigma(i+1)$ if $i$ is even, and $\sigma(i+1)<\sigma(i)$ otherwise. Thus it literally imposes alternating inequalities beginning with a rise at position $0$ . For $m=0$ or $m=1$ , there is no such $i$ , so every permutation satisfies the condition vacuously.

QSecantCubic.inversionNumber. For a permutation $\sigma$ of $\operatorname{Fin}(m)$ , this is the cardinality of the set of ordered pairs $(i,j)$ of indices satisfying $i<j$ and $\sigma(j)<\sigma(i)$ . It is a natural number and is zero when $m\le1$ .

QSecantCubic.qSecant. For every $n\in\mathbb N$ , this is the polynomial in $\mathbb Z[X]$

\sum_{\substack{\sigma\in S_{2n}\\ \forall i+1<2n,\; i\ {\rm even}\Rightarrow\sigma(i)<\sigma(i+1),\; i\ {\rm odd}\Rightarrow\sigma(i+1)<\sigma(i)}} X^{\operatorname{inv}(\sigma)}.

The sum is over every permutation of $\operatorname{Fin}(2n)$ passing the exact predicate above, with one monomial per permutation; equal inversion numbers therefore contribute repeated integer coefficients. At $n=0$ , the unique permutation of the empty finite type passes the condition vacuously and has zero inversions, so $qSecant(0)=1$ .

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