SextSmall

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

theorem ConwaySoifer.Simplified.sext_small {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) (hs : s ≤ 1 / 10) : False

Small external transfers: boundary propagation followed by the three new witnesses. The original nine-point checker is not used.

theorem ConwaySoifer.Simplified.sext_excluded {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Sext T r s) : False

The entire external-transfer case is now excluded along the simplified route.