Evidence package for "w(2;3,21) = 416, settled with LPM (Large Proof Model)"

Evidence package for the paper "w(2;3,21) = 416, settled with LPM (Large Proof Model)" by Eitan Nahmias (Hupyy), which proves that every red-blue colouring of 1, ..., 416 contains a red three-term or a blue 21-term arithmetic progression, and that some colouring of 1, ..., 415 contains neither (resolving a conjecture of Kullmann, 2010). The result is a Lean 4 theorem whose hypotheses state that the leaf formulas and the cover formulas of the 209 cases are unsatisfiable; each refutation was checked by the verified checker cake_lpr and bound by digest to its Lean term. The same pipeline checks w(2;3,20) = 389. Files: WP1-w2321-VERIFICATION-PACKAGE-RELEASE-20261028.zip: the Lean 4 sources, the case files, the per-leaf checker records of all 195 cases at t = 20, the t = 21 case table and binding record, the checker build sources, and the package's own SHA256SUMS and LISTING. WP1-w2321-RECORDS-20261029d.zip: the records folder cited by the paper's records table (ledger, provenance, replay table, review records), with records/LISTING.tsv. T21-DELIVERED-SETS-207.zip and T21-DELIVERED-SETS-207.SHA256SUMS: the delivered sets (manifest, split list, item list) of 207 of the 209 t = 21 cases; the other two ship inside the package zip. t21-replay-kit-v3-20261028.zip: the replay kit for t = 21 (instructions in t21-replay/REPLAY-T21.md). LEAF-T21-..., ITEM-T21-..., CPU-DISCREPANCIES-T21-...: the per-leaf, per-item and CPU-accounting tables of the t = 21 computation. RESPONSE-TO-REVIEW-b13.md: the response document to the internal and external reviews. PACKAGE-LISTING.tsv, RECORDS-LISTING.tsv, SHA256SUMS: listings and the SHA-256 digests of every file in this record. Verification: download all files into one folder and run "shasum -a 256 -c SHA256SUMS" (or "sha256sum -c SHA256SUMS"); every line must read OK. The paper's records table names each cited file by path and SHA-256 digest; the digests resolve against the two zips and the files beside them. Third-party files included for reproducibility (the cake_lpr checker sources) remain under their own licences.