AownSmall

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

theorem ConwaySoifer.Simplified.aown_double_core {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (j : Fin 6) (hj : j ≠ 0) (hj5 : j ≠ 5) : coreVertex (2 * s) j ∈ (T 0).carrier

Four vertices of the doubled adaptive core are forced into the centre.

theorem ConwaySoifer.Simplified.aown_half_core {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) (j : Fin 6) (hj : j ≠ 0) (hj5 : j ≠ 5) : (s / 2) • coreDir j ∈ (T 0).carrier

theorem ConwaySoifer.Simplified.aown_last_point {T : Configuration} {r s : ℝ} (H : Canonical ContactCase.Aown T r s) (hs : s ≤ 1 / 10) : (1 - 4 * s / 3, 0) ∈ (T 0).carrier

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

The small own-midpoint case uses the new cap, doubled sections and five-point geometry.