AcrossLarge #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.across_large
{T : Configuration}
{r s : ℝ}
(H : Canonical ContactCase.Across T r s)
(hs : 3 / 25 ≤ s)
:
The fixed witness (0, 9/10) excludes the expanded large-Across regime.