AownLarge #
Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.
theorem
ConwaySoifer.Simplified.aown_large
{T : Configuration}
{r s : ℝ}
(H : Canonical ContactCase.Aown T r s)
(hs : 7 / 20 ≤ s)
:
The large-Aown complement from the forbidden corner section and the full-endpoint cone restriction.