Exact Three-Symbol Density Hales–Jewett Numbers in Dimensions Seven Through Ten

We determine the exact three-symbol density Hales–Jewett numbers in dimensions seven through ten: c(7,3) = 1302, c(8,3) = 3780, c(9,3) = 11340, and c(10,3) = 32864. Here c(n,3) is the maximum cardinality of a subset of the ternary cube containing no combinatorial line. These construction sizes were previously known; the contribution is matching upper bounds for arbitrary subsets, together with ordinary Lean proofs. The dimension-nine upper bound follows by coordinate slicing from dimension eight. The accompanying proof supplement contains explicit witnesses, complete selected proof dependencies, pinned public Lean and Mathlib versions, and verification instructions. Verification does not require the proprietary discovery implementation.