SintSmall

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

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

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

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

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