A Super-x/log x Lower Bound and Certified Computations for Square Products of Factorials

For a positive integer m, let F(m) be the least k ≥ 2 for which there exist a₁ < ··· < aₖ = m such that a₁!···aₖ! is a square, and put Dₖ = {m : F(m)=k}. This preprint records the apparently unstated consequence |D₆ ∩ [1,x]| = ω(x/log x) of the Erdős–Graham fixed-cofactor theorem. It also presents certified computations using prime-exponent parity vectors and exhaustive search: 435643 = 13·23·31·47 is proved to be the first four-prime member of D₆; all 631 squarefree products of four distinct primes at least 13 up to 10⁶ are classified; and the complete D₆ computation is extended from 114271 through 115000 with 77 further terms. The positive-density conjecture D₆(x) ≫ x remains open.