Demonstrandum verified artifacts: five papers in combinatorics (counterexamples, records, theorems, and Lean formalizations)

Complete verification artifacts accompanying five papers by John Erlbacher: (1) a proof of the Elizalde–Luo conjecture on nonnesting pattern-avoiding multiset permutations, with a full Lean 4 formalization; (2) new records for the no-5-on-a-sphere problem in integer grids, including C(13) ≥ 36 and a general construction; (3) a disproof of Conjecture 4.6 of Z.-W. Sun (arXiv:2108.07723) by exact cyclotomic computation; (4) a Lean-kernel-verified disproof of the lattice-Borsuk cube-characterization conjecture (arXiv:2508.20009, Conjecture 3); (5) counterexamples to Graffiti conjectures 143 and 154 on graph eigenvalues. Every result is mechanically checkable: run python verify_all.py in the bundle root; Lean projects build with the pinned toolchains. Produced with Demonstrandum, a verification-first multi-agent AI pipeline (Anthropic Claude; OpenAI GPT-5.5/Codex as adversarial referee), under the direction of the author, who takes full responsibility for all claims.