Inversion-sequence equinumerosity

Zhou Bowen · Independent Researcher

A self-contained proof and reproducible verification of the equality

$$ |I_n(101,102,110)|=|I_n(021,100,101)| $$

for ordinary inversion sequences 0 <= e_i < i (one-based positions). Pattern occurrences use arbitrary increasing indices, not necessarily consecutive, preserving inequalities and equalities. For positive n, the common count is binomial(2n-2,n-1) = n Catalan(n-1); both empty classes have one element.

Read, check, watch

• Paper: seven-page manuscript, LaTeX, bibliography.
• 中文导读： 从删除与插入到生成函数，包含 A→B、B→B 重数的详细解释。
• Formal proof: six Lean modules, rooted at Cardinality.lean.
• Independent checker: nanoda instructions and evidence.
• Earlier informal manuscripts: originals and their scope.
• Animation: MP4 (3:12.3, Chinese captions, silent) and render instructions.

The paper proves the two counts separately; it does not claim a direct left-to-right bijection. The Lean development formalizes the structural counting proof. The manuscript credits prior right-class enumeration and related parent/statistic frameworks and does not claim historical priority. AI assistance is disclosed in the paper; the author is responsible for its claims. No journal acceptance or arXiv identifier is asserted here.

Check the Lean proof

Install the pinned Lean toolchain with Elan, then run from the repository root:

lean --version
lake --version
lake exe cache get
lake --no-cache build
lake env lean -DwarningAsError=true --stdin < verification/LeanAudit.txt

The toolchain is Lean 4.31.0; lake-manifest.json fixes Mathlib at fabf563a7c95a166b8d7b6efca11c8b4dc9d911f and its dependencies. Do not run lake update as part of verification. The six explicit library roots avoid importing other research topics. Initial dependency setup may require several GB; caches are not distributed in this repository.

The final theorem has no assumed recurrence or generation rule:

InversionTriples.card_left_eq_right :
  ∀ n : ℕ, Fintype.card (InversionTriples.L n) = Fintype.card (InversionTriples.R n)

The two successor-length central-binomial formulas and both empty cases are also formalized. The axiom closure is limited to propext, Classical.choice, and Quot.sound. The audit input prints the original definitions and checks exact final types and axiom dependencies.

Optional replay with the same Lean kernel, distinct from nanoda:

for module in Equinumerosity LeftCounting LeftFibers CountingSeries FiniteCoefficients Cardinality; do
  LEAN_NUM_THREADS=1 lake env leanchecker -v "AiMathLab.InversionTriples.$module"
done

Finite diagnostics

Python 3.10 or later, standard library only:

python3 -B -m unittest discover -s tests -v
mkdir -p verification/local
python3 -B scripts/inversion_triples_verify.py --max-n 9 > verification/local/author-rerun.json

There are six topic-specific tests. Enumeration covers raw lengths 0–9 and the specified generation checks; it is a diagnostic, not a proof for all lengths. See verification records and limits.

Build the paper

cd paper
tectonic --untrusted --keep-logs --keep-intermediates --reruns 2 main.tex

The checked local build uses Tectonic 0.15.0 and ordinary article/AMS packages, without shell escape, figures or custom styles. main.bbl is included. The manuscript source consists of main.tex, references.bib, and main.bbl; the rest of this repository is not required to typeset it.

The preserved manuscript was prepared before this repository was published, so its statement that verification records are maintained separately refers to the materials now provided here. It is not silently rewritten after validation. No platform submission is implied by the name “arXiv v1”.

Integrity and provenance

VERSIONS.json records the tool/source revisions and important content hashes. Run:

sha256sum -c SHA256SUMS

This repository starts with a new, topic-only Git history. Original Lean and mathematical manuscript source bytes are preserved; the Chinese guide has only a public-facing introductory sentence adjustment. Build dependencies are fetched from the public repositories identified in the lock file. Internal reviews, correspondence, other research topics, private Git metadata, credentials and dependency caches are excluded.

License status

No general reuse license has yet been selected for the project's original paper, proof code, explanatory text or animation. Public visibility alone is not a grant of a broad reuse license, and the proposed arXiv distribution license does not license this whole repository. Third-party components and derived declarations retain their applicable licenses; see third-party notices. This status will be updated only following an explicit licensing decision.