An upper bound c_7 <= 1345 for the density Hales-Jewett number, with machine-checkable certificates

I report machine-checkable certificates supporting c7 ≤ 1345 for the largest line-free subset of {0,1,2}7. This improves the previously published upper bound of 1348 (stated in T. Tao's blog post of 4 March 2009) to 1345. I gratefully acknowledge D.H.J. Polymath: the argument builds entirely on the project's definitions, values through dimension six, and techniques. This deposit contains note.pdf, replay.sh, checksum manifests, generator scripts, ten lemma CNF/DRAT pairs, the 1302-point consistency control, logs, and compressed original CNF/LRAT and blind CNF/DRAT files. Put all files in one folder and run bash replay.sh; nothing is downloaded. A full replay in my test used about ten minutes of CPU time and about 5 GB of memory for cake_lpr; drat-trim and cake_lpr must be installed separately. bash replay.sh quick runs only the smaller checks and does not check the two main proofs. Use of AI. The author is not a professional researcher. The search, checks and drafting were carried out by AI models (Anthropic's Claude via Claude Code; OpenAI's Codex and ChatGPT as drafting aid and reviewer) under the author's direction. The author is responsible for the content. No human expert has reviewed the work to date. Corrections are welcome. Relative to c_1..c_5 (DRAT) and c_6 <= 450 (slicing). Upper bound only; c_7 is not determined.