q-Secant inversion-enumerator interfaces

Definition

frame_2026_qsecant_interfaces

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

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

View graph