Part of the Dual-Rail Carrier Program — the series hub (map, citation DAG, DOIs, release standards).

Wilf equivalences of inversion-sequence patterns: length-4 classification completed, length-5 openings, and the staircase-prefix invariant

Machine-discovered, machine-proved, kernel-checked combinatorics — with full disclosure of how it was made.

Author / operator: Won Chul Yang (independent researcher, wcy0969@gmail.com). Produced by: KoreoLoop, an autonomous multi-agent research loop developed and operated by the author, running frontier language models (Anthropic Claude family; OpenAI GPT family) for discovery, formalization, and adversarial verification, with the Lean 4 kernel as the final acceptance gate. The author directed the research programme and verified the pipeline; the mathematics itself was found and formalized by the loop. This repository is published in that spirit: every theorem labelled "(Lean)" is machine-checkable by anyone, independent of any claim of human or machine authorship.

Contents

note/ — Resolution of the last open case of the length-4 Wilf classification

Hong & Li (Electron. J. Combin. 29(4) (2022), #P4.37, Conjecture 20) classified length-4 patterns on inversion sequences up to Wilf equivalence, with a single case left open: 3012 ≡ 3201. The note proves it, completing the class {3012, 3201, 3210} and with it the length-4 classification.

• note/note.pdf, note/note.tex
• note/artifact/Wilf_3012_3201.lean — complete, self-contained kernel-checked proof (~1,800 lines; Lean 4.31.0 + Mathlib tag v4.31.0).

paper/ — Length-five Wilf equivalences and the staircase-prefix invariant (SPI)

Fifteen length-5 Wilf equivalences (nothing was previously known at length ≥ 5 in the classical setting), and the SPI programme: for max-first patterns, the first distinguishing length, the class sizes (Σ c!), and the constant gap Δ = 3.

New in v1.1.0: the gap theorem Δ = 3 is now proven unconditionally for all K ≥ 4 via a global counting identity (the certificate identity C(σ) = C₀(K) + 3·[σ ∈ SPI]) — no descent, no induction, no connectivity argument. The complete proof documents, an independent adversarial audit, and zero-violation machine checks live in paper/certificate/ (its README has one-command verification instructions).

• paper/paper.pdf, paper/paper.tex
• paper/certificate/ — the certificate-identity proof chain + Python probes.
• paper/artifact/ — 17 self-contained Lean files: SPIGen.lean, SPIGap.lean (∀K-generic theorems) + 15 per-pair length-5 proofs Wilf5_<P>_<Q>.lean, with its own README and verification instructions.

Verifying (no trust required)

Requires Lean 4.31.0 with Mathlib (tested at tag v4.31.0). In any Lake project depending on Mathlib:

lake env lean <file>.lean

Expected for every artifact file: exit 0, no errors (unused-variable linter warnings only), and every #print axioms line reporting a subset of [propext, Classical.choice, Quot.sound] — the standard Mathlib base. No sorry, no native_decide, no custom axioms, in any file.

Provenance and honesty

• Proof status is labelled throughout the paper: (Lean) = kernel-checked; (hand + verified K ≤ k) = hand proof with exhaustively machine-verified case analyses for the stated range; conjectures are labelled as such.
• A citation-graph sweep (OpenAlex, Semantic Scholar, arXiv) for prior resolutions of Conjecture 20 and for the length-5 equivalences was last run on 2026-07-20/21: no prior claims found. Corrections welcome — this is a standing invitation to falsify.

License

• Lean artifacts (*.lean): Apache License 2.0 (compatible with Mathlib).
• Manuscripts and text (*.pdf, *.tex, *.md): CC BY 4.0.

Citing

See CITATION.cff. Concept DOI (all versions): 10.5281/zenodo.21474657; v1.0.0 DOI: 10.5281/zenodo.21474658; v1.1.0 DOI: 10.5281/zenodo.21623328.