The four-child packing

This file constructs the split-radius packing on the four child labels and records its elementary routing algebra.

def LeanPool.Besicovitch.fourChildrenPacking (configuration : SixPointConfiguration) {L M x y : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) : SixPointPacking configuration

The packing on all four children with prescribed tangent radius splits.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.fourChildrenCrossMaximum (L M x y B11 B12 B21 B22 : ℝ) : ℝ

The largest cross-color diameter term for a four-child radius split.

Equations

• LeanPool.Besicovitch.fourChildrenCrossMaximum L M x y B11 B12 B21 B22 = max (B11 + x + y) (max (B12 + x + (M - y)) (max (B21 + (L - x) + y) (B22 + (L - x) + (M - y))))

def LeanPool.Besicovitch.fourChildrenSplitDiameter (L M x y B11 B12 B21 B22 : ℝ) : ℝ

The largest same-color or cross-color diameter term for a four-child split.

Equations

• LeanPool.Besicovitch.fourChildrenSplitDiameter L M x y B11 B12 B21 B22 = max (2 * L) (max (2 * M) (LeanPool.Besicovitch.fourChildrenCrossMaximum L M x y B11 B12 B21 B22))

theorem LeanPool.Besicovitch.fourChildrenPacking_totalRadius (configuration : SixPointConfiguration) {L M x y : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) : (fourChildrenPacking configuration hLdist hMdist hL hx_lower hx_upper hM hy_lower hy_upper).totalRadius = L + M

The total radius of the four-child packing is the sum of the two sibling lengths.

theorem LeanPool.Besicovitch.fourChildrenPacking_virtualDiameter (configuration : SixPointConfiguration) {L M x y : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) : (fourChildrenPacking configuration hLdist hMdist hL hx_lower hx_upper hM hy_lower hy_upper).virtualDiameter = fourChildrenSplitDiameter L M x y (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right))

The virtual diameter of the four-child packing is its explicit split minimax.

theorem LeanPool.Besicovitch.fourChildrenPacking_score_nonnegative (configuration : SixPointConfiguration) {c L M x y : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) (hc : 0 < c) (hdiameter : fourChildrenSplitDiameter L M x y (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right)) ≤ c * (L + M)) : 0 ≤ (fourChildrenPacking configuration hLdist hMdist hL hx_lower hx_upper hM hy_lower hy_upper).score (c / 2)

A split below c(L+M) gives the four-child packing nonnegative score at c/2.

theorem LeanPool.Besicovitch.exists_fourChildren_split_of_routing_bounds {L M T B11 B12 B21 B22 : ℝ} (hL : L ≤ 2) (hM : M ≤ 2) (h11 : L + M + B11 - 2 ≤ T) (h12 : L + M + B12 - 2 ≤ T) (h21 : L + M + B21 - 2 ≤ T) (h22 : L + M + B22 - 2 ≤ T) (hrow1 : L + M + L - 2 + B11 + B12 ≤ 2 * T) (hrow2 : L + M + L - 2 + B21 + B22 ≤ 2 * T) (hcolumn1 : L + M + M - 2 + B11 + B21 ≤ 2 * T) (hcolumn2 : L + M + M - 2 + B12 + B22 ≤ 2 * T) (hmatching1 : L + M + B11 + B22 ≤ 2 * T) (hmatching2 : L + M + B12 + B21 ≤ 2 * T) : ∃ (x : ℝ) (y : ℝ), L - 1 ≤ x ∧ x ≤ 1 ∧ M - 1 ≤ y ∧ y ≤ 1 ∧ B11 + x + y ≤ T ∧ B12 + x + (M - y) ≤ T ∧ B21 + (L - x) + y ≤ T ∧ B22 + (L - x) + (M - y) ≤ T

The routing bounds give a split whose four cross terms are all below the target.

theorem LeanPool.Besicovitch.exists_fourChildren_split_iff_routing_bounds {L M T B11 B12 B21 B22 : ℝ} (hL : L ≤ 2) (hM : M ≤ 2) : (∃ (x : ℝ) (y : ℝ), L - 1 ≤ x ∧ x ≤ 1 ∧ M - 1 ≤ y ∧ y ≤ 1 ∧ fourChildrenSplitDiameter L M x y B11 B12 B21 B22 ≤ T) ↔ 2 * L ≤ T ∧ 2 * M ≤ T ∧ L + M + B11 - 2 ≤ T ∧ L + M + B12 - 2 ≤ T ∧ L + M + B21 - 2 ≤ T ∧ L + M + B22 - 2 ≤ T ∧ L + M + L - 2 + B11 + B12 ≤ 2 * T ∧ L + M + L - 2 + B21 + B22 ≤ 2 * T ∧ L + M + M - 2 + B11 + B21 ≤ 2 * T ∧ L + M + M - 2 + B12 + B22 ≤ 2 * T ∧ L + M + B11 + B22 ≤ 2 * T ∧ L + M + B12 + B21 ≤ 2 * T

Exact threshold form of the two-by-two split minimax formula.

theorem LeanPool.Besicovitch.fourChildren_routing {L M T B11 B12 B21 B22 : ℝ} (hL : L ≤ 2) (hM : M ≤ 2) (hsameL : 2 * L ≤ T) (hsameM : 2 * M ≤ T) (hfail : ∀ (x y : ℝ), L - 1 ≤ x → x ≤ 1 → M - 1 ≤ y → y ≤ 1 → T < fourChildrenSplitDiameter L M x y B11 B12 B21 B22) : T < L + M + B11 - 2 ∨ T < L + M + B12 - 2 ∨ T < L + M + B21 - 2 ∨ T < L + M + B22 - 2 ∨ 2 * T < L + M + L - 2 + B11 + B12 ∨ 2 * T < L + M + L - 2 + B21 + B22 ∨ 2 * T < L + M + M - 2 + B11 + B21 ∨ 2 * T < L + M + M - 2 + B12 + B22 ∨ 2 * T < L + M + B11 + B22 ∨ 2 * T < L + M + B12 + B21

Failure of every split forces a single, row, column, or matching routing term.

theorem LeanPool.Besicovitch.fourChildren_row_column_or_matching {c L M B11 B12 B21 B22 : ℝ} (hc_one : 1 < c) (hc_two : c ≤ 2) (hcL : c ≤ L) (hcM : c ≤ M) (hL : L ≤ 2) (hM : M ≤ 2) (hsame_gap : 0 < c * (c + 2) - 4) (hsingle_gap : 1 < 2 * c * (c - 1)) (hB11 : B11 ≤ 3) (hB12 : B12 ≤ 3) (hB21 : B21 ≤ 3) (hB22 : B22 ≤ 3) (hfail : ∀ (x y : ℝ), L - 1 ≤ x → x ≤ 1 → M - 1 ≤ y → y ≤ 1 → c * (L + M) < fourChildrenSplitDiameter L M x y B11 B12 B21 B22) : 2 + 2 * (c - 1) * L + (2 * c - 1) * M ≤ B11 + B12 ∨ 2 + 2 * (c - 1) * L + (2 * c - 1) * M ≤ B21 + B22 ∨ 2 + (2 * c - 1) * L + 2 * (c - 1) * M ≤ B11 + B21 ∨ 2 + (2 * c - 1) * L + 2 * (c - 1) * M ≤ B12 + B22 ∨ (2 * c - 1) * (L + M) ≤ B11 + B22 ∨ (2 * c - 1) * (L + M) ≤ B12 + B21

In the endpoint range, four-child failure routes to a row, column, or matching.