bibkey: hardin2013a222001 authors: R. H. Hardin; Colin Barker year: 2013 title: “OEIS A222001, Number of n X 3 arrays with permutation rows and compatible descent and lexicographic orders” doi: null url: https://oeis.org/A222001 claim: “For every n >= 1, the number of n X 3 permutation-row arrays with nondecreasing downstep counts and lexicographically nonincreasing rows is 2+(n+1)(n+2)(n+3)/6.” strata_touched:

D5/S3/Combinatorics/PermutationArrays/DescentLexCount license: citation-only triage: anchor

OEIS A222001: descent and lexicographic orders on permutation arrays

Verified locator

https://oeis.org/A222001, NAME:

Number of n X 3 arrays with each row a permutation of 1..3 having at least as many downsteps as the preceding row, with rows in lexicographically nonincreasing order.

The sequence is attributed to R. H. Hardin (2013). The displayed formula a(n) = 2 + (1 + n)*(2 + n)*(3 + n) / 6 is attributed to Colin Barker (2018), under the entry’s Conjectures heading, with OFFSET 1,1. The independent source audit records revision 10 (2018) with that same Conjectures label. This note records source attribution and scope; it does not assert later literature status, official acceptance, publication priority, or worldwide uniqueness.

Exact carrier and source correspondence

Row is Equiv.Perm (Fin 3). Column coordinates 0,1,2 label source columns 1,2,3. The executable definition sourceEntry r j = (r j).val+1 relabels 0,1,2 as 1,2,3; this strictly increasing bijection preserves equality, both adjacent descent tests, and lexicographic order.

descents sums the indicators for the actual adjacent comparisons in columns (0,1) and (1,2). lexLE compares the first actual source entry, then the second on equality, then the third on equality of both preceding entries. Arrays n is the subtype of actual functions Fin n → Row whose descent counts are nondecreasing and whose rows are lexicographically nonincreasing. These are conditions on the original row positions, and repeated rows are permitted.

The primary endpoint is DescentLexCount.count_arrays (n : ℕ) (hn : 1 ≤ n):

Nat.card (Arrays n) = 2 + (n + 1) * (n + 2) * (n + 3) / 6.

The carrier contains actual permutations and order predicates. It is not defined by the conjectured sequence, recurrence, or formula.

Exhaustive decomposition

In increasing lexicographic order, the six actual rows are 123,132,213,231,312,321, with descent counts 0,1,1,1,1,2. Lexicographic decrease makes this count nonincreasing. The source condition makes it nondecreasing, so every row of a given array has the same descent count.

The zero-descent class contains only 123 and the two-descent class contains only 321; at positive length these yield two different constant arrays. The one-descent class consists of exactly the four middle permutations. Every nonincreasing word on these four rows is permitted, and every permitted array in this class is such a word. Taking its multiset and sorting in decreasing order are inverse constructions, retaining all repetitions. The private arrayDecomposition gives the concrete equivalence

Arrays n ≃ Bool ⊕ Sym (Fin 4) n

under 1 ≤ n. The generic count is reused from Mathlib Sym.card_sym_eq_choose; sorted-word uniqueness is reused from List.Perm.eq_of_sortedGE, with Multiset.pairwise_sort, Multiset.sort_eq, and Multiset.length_sort. Binomial symmetry and Nat.choose_eq_descFactorial_div_factorial give the displayed cubic.

At n=0, all three constructions collapse to the same empty array, so the positive-length equivalence is unavailable. There is exactly one empty array, while substituting zero in the source cubic gives three.

Supplier and search boundary

The bounded repository and Mathlib search found no whole actual-array theorem for this target. Mathlib’s symmetric-multiset cardinality and sorting results supply the generic pieces reused by the Lean proof; they do not themselves state this carrier count. External sequencelib and joeis entries are arithmetic sequence implementations and are not proofs about this actual array carrier.

Scope and evidence boundary

The mathematical source is D5/S3/Combinatorics/PermutationArrays/DescentLexCount.lean, with matching Blueprint Scribe. Its public theorem is the count for every positive length. The six-row classification and the decomposition are proof components of this unbounded result, not a finite-prefix claim. The proof uses Lean proof terms and Mathlib counting and sorting theorems.

The theorem establishes no report, freeze, gate, official acceptance, publication priority, or delivery status. Information-escape registration is unfinished under the repository’s registration suspension; no Reg source or valid registration is supplied.