Reusable Lean library

The formalization produced reusable Lean infrastructure for q-analogs and recurrence-defined special numbers — not only one-off proofs of the paper. This page is a curated guide to the modules you can import and build on. Every declaration below is kernel-checked in Lean 4 (no sorry, Mathlib axioms aside).

How to import

import OreAlgebraLib.Special.QAnalog
import OreAlgebraLib.Special.QEulerian
import OreAlgebraLib.Benchmarks.OEIS

A tiny session (values verified with lake env lean):

import OreAlgebraLib.Special.QAnalog
import OreAlgebraLib.Special.QEulerian

open OreAlgebraLib.Special.QAnalog
open OreAlgebraLib.Special.QEulerian

#eval qNat ℚ 2 5        -- 31          (= 1 + 2 + 4 + 8 + 16)
#eval qBinom ℚ 2 5 2    -- 155         (Gaussian binomial (5 choose 2)_2)
#eval qEulerian ℚ 2 3 2 -- 12          (Carlitz q-Eulerian E1(3,2) at q = 2)

All three modules are generic. Type-class requirements per declaration in QAnalog: qNat and qStirling2 work over any CommSemiring R; qBinom, qStirling1, and qStirling1Tilde are currently CommRing R (their recurrences involve subtraction or a constant 1 on the additive side). QEulerian is entirely CommSemiring R; the OEIS benchmarks are specialized to ℚ.

`OreAlgebraLib.Special.QAnalog`

q-numbers, Gaussian binomials, and q-Stirling triangles. Source: OreAlgebraLib/Special/QAnalog.lean.

Declaration	Kind	Description
`qNat R q n`	def	The q-integer `[n]_q = ∑ i < n, q^i`
`qNat_zero`, `qNat_succ`	simp lemmas	`[0]_q = 0`, `[n+1]_q = [n]_q + q^n`
`qBinom R q n k`	def	Gaussian binomial `(n choose k)_q`, by the Pascal recurrence `C(n+1,k+1)_q = C(n,k+1)_q + q^(n−k)·C(n,k)_q`
`qStirling1 R q n k`	def	q-Stirling numbers of the first kind (unweighted), `S₁ᵠ(n+1,k+1) = S₁ᵠ(n,k) − [n]_q·S₁ᵠ(n,k+1)`; needs `CommRing R`
`qStirling2 R q n k`	def	q-Stirling numbers of the second kind, `S₂ᵠ(n+1,k+1) = q^k·S₂ᵠ(n,k) + [k+1]_q·S₂ᵠ(n,k+1)`
`qStirling1Tilde R q n k`	def	The corrected first-kind analog `S̃₁` found by the Id. 3 CAS search: `S̃₁(n+1,k+1) = S̃₁(n,k) − ([n]_q + q^k − 1)·S̃₁(n,k+1)`

For each of qStirling1, qStirling2, qStirling1Tilde the module proves the full triangular skeleton: *_zero_zero, *_zero_succ, *_succ_zero, *_succ_succ (the recurrence itself), plus *_eq_zero_of_lt (vanishing above the diagonal) and, for qStirling1Tilde, qStirling1Tilde_self (diagonal is all ones).

Notes carried from the formalization:

qStirling1 is deliberately the unweighted first kind — the paper's Gould q^(1−n)-weighted variant does not match the verified Identity 2 (see the coverage table, Id. 2).
qStirling1Tilde reduces to the classical signed Stirling recurrence at q = 1, and is the analog for the corrected generic-q Id. 3.

`OreAlgebraLib.Special.QEulerian`

Carlitz q-Eulerian numbers with recurrence and support lemmas. Source: OreAlgebraLib/Special/QEulerian.lean.

Declaration	Kind	Description
`qEulerian R q n k`	def	Carlitz `E1(n,k)` by the recurrence `E1(n+1,k) = [n+2−k]_q·E1(n,k−1) + q^(n+1−k)·[k]_q·E1(n,k)`, initial row `E1(0,k) = δ_{k,1}`, columns 1-indexed
`qEulerian_zero_zero`, `qEulerian_zero_one`, `qEulerian_zero_succ_succ`, `qEulerian_succ_zero`, `qEulerian_zero_col`	simp lemmas	Initial row and vanishing zeroth column
`qEulerian_succ_succ`	simp lemma	The recurrence in triangular form at column `k+1`
`qEulerian_succ`	theorem	The paper's printed recurrence in uniform form for `1 ≤ k`
`qEulerian_eq_zero_of_lt`	theorem	Upper support: `E1(n,k) = 0` for `n+1 < k`
`qEulerian_top_zero`	theorem	Top entry `E1(n+1,n+2) = 0`
`qEulerian_diag`	theorem	Right diagonal `E1(n+1,n+1) = 1`
`qEulerian_succ_one`	theorem	First-column propagation `E1(n+1,1) = q^n·E1(n,1)` (so the first column is `q^(n(n−1)/2)`; it is not constant)

The initial row E1(0,k) = δ_{k,1} is fixed by the CAS audit (cas/check_qeulerian_convention.py): with it, the q-Worpitzky linear system has a unique solution matching the recurrence in both directions, so the recurrence definition and the Worpitzky definition are interchangeable.

`OreAlgebraLib.Benchmarks.OEIS`

Recurrence benchmark examples and uniqueness checks. Source: OreAlgebraLib/Benchmarks/OEIS.lean. Each entry pairs an OEIS-style spec (a normalized recurrence plus initial values) with an independently computed closed form, and concludes spec = closed via the D-finite uniqueness kernel Dfinite.eq_of_initial_and_normalized_recurrence.

Entry	Lean theorem	Shape
A000045 Fibonacci	`fibSpec_eq_fibClosed`	order-2 constant coefficients vs. pair iteration
A000142 Factorial	`factSpec_eq_factClosed`	order-1 vs. `Nat.factorial`
A000079 Powers of two	`pow2Spec_eq_pow2Closed`	order-1 doubling
A000073 Tribonacci	`tribSpec_eq_tribClosed`	order-3 constant coefficients
A000984 Central binomial	`centralSpec_eq_centralClosed`	rational `n`-dependent coefficient with a denominator side condition
A007318 (diagonal)	`pathsDiagSpec_eq_centralSpec`	grid-path dynamic program equals central binomials
A007318 (row sums)	`rowSum_eq_rowSumSpec`	Pascal row-sum DP equals `2^m`
A000225 Prefix sums	`prefixSums_eq_onesSpec`	affine (non-homogeneous) recurrence, `2^n − 1`

This exercises the trusted recurrence-checking kernel (see the blueprint) on many small examples — the practical bridge from paper identities to recurrence-defined program behavior. Machine-readable descriptors live under data/oeis/.

Future: generated API docs

The longer-term upgrade is generated Lean API documentation with doc-gen4, so readers can browse the actual declarations module-by-module including full statements and proof-term links. This guide is the interim curated face of the library. If you have Lean + elan installed, you can generate docs locally with:

lake doc   # requires doc-gen4 in lakefile require