Separated Euclidean distances with diameter below 0.74n^2 in a fixed dimension

For every integer n >= 68000, this manuscript constructs n points in the single Euclidean space R^458999, with nonzero distances at least one, distinct unordered-pair distances separated by at least one, and diameter strictly below (37/50)n^2. The archive preserves the manuscript, its complete 54-module Lean source closure, dependency pins, proof correspondence and recorded verification evidence from public Git commit 1e73a12ff1076dd11affadbf619ddbbef587133e. The owning proof-source revision is 35c67a69e009c9ca27267077608864987b7e2851. Recorded macOS and Linux runs each rebuilt all project modules from zero project .olean files and passed 56 commands including six trust-zero axiom audits. The Linux run also passed a fresh replay of the compiled transitive import environment through Lean's own kernel. Both runs used compiled upstream imports; neither establishes a source-only Mathlib build or independently implemented kernel verification. John Tripodo directed the research and curated the source and verification artifacts. The manuscript was prepared with substantial OpenAI ChatGPT assistance; the broader research program also used Anthropic Claude, without assigning particular steps of this proof to Claude. No independent human mathematical or historical priority review, journal acceptance, or arXiv deposit is claimed. The result does not establish a planar theorem or an optimal fixed dimension or constant. The Lean code and automation are MIT-licensed. The manuscript PDF and TeX source, including copies in the ZIP, retain the reserved-rights terms in LICENSE-PAPER.