A left-and-bottom touching 36-point configuration contains a close pair
OpenCirclePackingConstants.thirty_six_left_bottom_close_pairboundary-normal-formcircle-packingdiscrete-geometrypoint-separation
If 36 points lie in the unit square and the configuration touches both the left side and the bottom side, then two distinct points are at Euclidean distance at most 1/5.
Preamble
import Definitions.Def_CirclePackingConstants
Formal statement
namespace CirclePackingConstants
theorem thirty_six_left_bottom_close_pair :
∀ p : Fin 36 → Point,
(∀ i, 0 ≤ (p i).1 ∧ (p i).1 ≤ 1 ∧ 0 ≤ (p i).2 ∧ (p i).2 ≤ 1) →
(∃ i, (p i).1 = 0) →
(∃ j, (p j).2 = 0) →
∃ i j, i ≠ j ∧ sqDist (p i) (p j) ≤ (1 : ℝ) / 25 := by sorry
end CirclePackingConstantsSource
Boundary-normal geometric core obtained from CirclePackingConstants.thirty_six_unit_square_close_pair by translation invariance. This remains the genuine hard geometric obligation; no use is made of the disputed Kirchner-Wengerodt optimality argument.