The independent, unconditional assembly of the third-pass simplified proof.

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

theorem ConwaySoifer.lowerBound_simplified : LowerBound

Ten congruent closed equilateral triangles covering the whole side-three triangle have common side at least one, by the simplified proof.

theorem ConwaySoifer.one_le_side_of_cover_simplified (r : ℝ) (T : Configuration) (hside : CommonSide T r) (hcover : Covers T) : 1 ≤ r

theorem ConwaySoifer.no_ten_unit_triangle_cover_simplified (ε : ℝ) (hε : 0 < ε) (T : Configuration) (hs : ∀ (i : Fin 10), (T i).side = 1) (hcover : ∀ p ∈ (1 + ε / 3) • target, ∃ (i : Fin 10), p ∈ (T i).carrier) : False

The scaled consequence for ten unit triangles and target side 3 + ε.