Demonstrandum verified artifacts: eight 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. Version 2 (2026-07-08): adds the Program UC flagship paper "The union-closed sets conjecture: a kernel-verified constant, a certified frontier value, and the semantic completeness of the entropy method" (uc-flagship-paper.pdf) and its complete ancillary bundle (uc-flagship-anc-v2.zip): the Lean 4 development (89 kernel-checked declarations, standard axioms only), the exact-interval certifiers and banked certificates (0.38234 frontier certificate; two-form cap certificate at 0.3823456 with its strict-convention epsilon companion; 9/32 absorption-table certificate), all verification scripts, the paper-wide numeric audit harness (62/62), and the SHA-256 artifact manifest. All wave-1 files are retained unchanged. v2 additions (2026-07-08): the Union-Closed/Frankl flagship paper (uc-flagship-paper.pdf + ancillary bundle); the strong-majority edge-coloring paper (strong-majority-t3-map.pdf; cites Antoniuk–Prorok–Salia arXiv:2607.00212 for the bound 5, obtained independently); and the AI-conjecture refutation bundle (ai-conjecture-bundle.pdf, nine refutations with complete certificates).