Expand a nondegenerate left-bottom configuration until it touches a third side

Open

CirclePackingConstants.thirty_six_left_bottom_expand_to_three_sides

by WillR · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-packingdiscrete-geometrynormalisationscaling

A nondegenerate 36-point configuration in the unit square that touches the left and bottom sides can be uniformly expanded about the origin until it also touches the right or top side. The expansion stays in the unit square and never decreases any pairwise squared distance.

Preamble

import Definitions.Def_CirclePackingConstants

Formal statement

namespace CirclePackingConstants

theorem thirty_six_left_bottom_expand_to_three_sides :
    ∀ 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) →
      (∃ k, (p k).1 ≠ 0 ∨ (p k).2 ≠ 0) →
      ∃ q : Fin 36 → Point,
        (∀ i, 0 ≤ (q i).1 ∧ (q i).1 ≤ 1 ∧ 0 ≤ (q i).2 ∧ (q i).2 ≤ 1) ∧
        (∀ i j, sqDist (p i) (p j) ≤ sqDist (q i) (q j)) ∧
        (∃ i, (q i).1 = 0) ∧
        (∃ j, (q j).2 = 0) ∧
        ((∃ i, (q i).1 = 1) ∨ (∃ j, (q j).2 = 1)) := by sorry

end CirclePackingConstants

Source

Elementary normalisation. Let M be the larger of the maximum x-coordinate and maximum y-coordinate. Nondegeneracy gives M>0. Divide every coordinate by M. Since 0<M≤1, the new configuration remains in the unit square, retains the left/bottom contacts, touches right or top, and every pairwise squared distance is scaled by 1/M² ≥ 1.

View graph