An all-n enumeration turns one entry in a conjecture table into a kernel-checked theorem.

The {1132, 3312} entry in Table 4 of S. Elizalde and A. Luo's Pattern avoidance in nonnesting permutations is proved here for every n ≥ 1 and formalized in Lean 4. The result replaces computation through n = 8 with an all-n theorem, supported by two complete proofs: a recurrence and structural count, and an explicit bijection onto a ternary language.

The table concerns permutations of the multiset {1,1,2,2,…,n,n} that avoid both patterns under the paper's biconditional containment convention, and cross-references the sequence to OEIS A168583. The paper appeared in 2025 as DMTCS 27:1, Permutation Patterns 2024, paper #13 (arXiv:2412.00336; DOI 10.46298/dmtcs.14885). Its conjecture table was unchanged, and no proof was found in the literature during the June 2026 campaign.

The frozen statement

Table 4, headed “Further research,” prints the row {1132,3312} & 3^n−3·2^{n−1}+1 & A168583, under the preamble “All the conjectures have been checked for n up to 8.”

For every n ≥ 1, the number of nonnesting permutations of {1,1,2,2,…,n,n} avoiding 1132 and 3312 equals 3ⁿ − 3·2ⁿ⁻¹ + 1.

The result

The recurrence proof and the bijective proof share the FIFO normal form, sign-word coordinates for prefix-extremal labelings, and the characterization of avoiders by arc-sign constraints. Their prose explains the enumeration; it corroborates, but is not load-bearing for, the kernel claim.

declaration: ElizaldeLuo.elizalde_luo_1132_3312
toolchain: leanprover/lean4:v4.30.0 with mathlib pinned
statement: count = 3ⁿ − 3·2ⁿ⁻¹ + 1 for every n ≥ 1

The axiom audit reports exactly [propext, Classical.choice, Quot.sound], with no sorryAx.

Corroborating computation

Exhaustive cross-checks extend beyond the paper's stated range. Theorem A was checked on all 2,162,160 shape-permutation pairs at n = 7 and all 57,657,600 pairs at n = 8. The end-to-end bijection was checked on all 85,514 avoiders for n ≤ 10, and the summation identity was checked exactly through n = 60. These computations corroborate the proof; they do not replace the kernel-checked theorem.

Artifacts

Limitations

The kernel guarantees the formal theorem as stated. The correspondence between the Lean avoider set and the convention in Table 4 is human-checked: the reading kit compares pinned quotations in the frozen definitions with the formalization and includes a kernel-checked small-n comparison against the paper's data.

The result has not been externally refereed. The authors were notified privately. Corrections will be logged, dated, and never silent.