Normalization

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

theorem ConwaySoifer.Simplified.exists_canonical (r : ℝ) (T : Configuration) (hside : CommonSide T r) (hcover : Covers T) (hr : r < 1) : ∃ (c : ContactCase) (U : Configuration) (s : ℝ), Canonical c U r s

Unconditional geometric normalization for the simplified route. It uses no coreChecked, bridgeChecked, or midForbidChecked evaluations.