Every three-coloring of R^7 contains a monochromatic unit square

Every coloring of R^7 with three colors contains a monochromatic unit square, so d(3) <= 7 in the notation of Gasarch, Gezalyan and Parker (SIGACT News 56(3), 2025), whose column gives d(3) <= 10 and asks for better upper bounds. The witness is the 64 even-weight points of {0,1}^7 scaled by 1/sqrt(2). A short hand argument reduces the claim to 117 finite cases. This is a computer-assisted proof: a SAT solver refutes each case, and drat-trim and lrat-check accept the proofs. A separate Lean 4 proof has no sorry; it trusts compiled code at 118 steps (117 bv_decide, 1 native_decide), so it is not a kernel-only proof. Running "bash verify_all.sh" repeats the checks. I direct AI agents and built the checks; Claude did the detailed work. No mathematician has refereed this.