Documentation

LeanPool.Besicovitch.SixPoint.RowColumnRescue

The row and column rescue #

This file proves the first strict exit in the endpoint failure tree. A row or column obstruction for the four-child packing forces the corresponding root against the full opposite triangle to have nonnegative score.

source
theorem LeanPool.Besicovitch.row_obstruction_excludes_root_triangle_endpoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p w₁ w₂ : E) (he : ‖e‖ = 1) (hp : ‖p‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hseparation : barC ≤ ‖w₁ - w₂‖) (hrow : 4 * barC ^ 2 - 3 * barC + 2 ≤ ‖e - p - w₁‖ + ‖e - p - w₂‖) :
‖e - w₁‖ < barC - 1 + ((barC - 1) * (‖w₁‖ + barC) + (barC + 1) * ‖w₂‖) / 2

A four-child row obstruction is incompatible with the corresponding root-triangle endpoint.

source
noncomputable def LeanPool.Besicovitch.redRootBlueTrianglePacking (configuration : SixPointConfiguration) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) :
SixPointPacking configuration

Support 17: the red root of radius one against the canonical blue triangle.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LeanPool.Besicovitch.blueRootRedTrianglePacking (configuration : SixPointConfiguration) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) :
    SixPointPacking configuration

    Support 71: the blue root of radius one against the canonical red triangle.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LeanPool.Besicovitch.redRootBlueTrianglePacking_totalRadius (configuration : SixPointConfiguration) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) :
      (redRootBlueTrianglePacking configuration hblueLeft hblueRight).totalRadius = 1 + (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) + dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) / 2

      The total radius of support 17 is one plus the blue semiperimeter.

      source
      theorem LeanPool.Besicovitch.blueRootRedTrianglePacking_totalRadius (configuration : SixPointConfiguration) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) :
      (blueRootRedTrianglePacking configuration hredLeft hredRight).totalRadius = 1 + (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) + dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) / 2

      The total radius of support 71 is one plus the red semiperimeter.

      source
      theorem LeanPool.Besicovitch.red_root_blue_triangle_score_nonnegative_of_row_obstruction (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) (hrow : 2 + 2 * (barC - 1) * dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) + (2 * barC - 1) * dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) ≤ dist (configuration SixPointColor.red redLabel) (configuration SixPointColor.blue SixPointLabel.left) + dist (configuration SixPointColor.red redLabel) (configuration SixPointColor.blue SixPointLabel.right)) :
      0 ≤ (redRootBlueTrianglePacking configuration ⋯ ⋯).score barS

      A row obstruction makes support 17 a nonnegative-score endpoint packing.

      source
      theorem LeanPool.Besicovitch.blue_root_red_triangle_score_nonnegative_of_column_obstruction (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (blueLabel : SixPointLabel) (hblueLabel : blueLabel ≠ SixPointLabel.root) (hcolumn : 2 + 2 * (barC - 1) * dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) + (2 * barC - 1) * dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) ≤ dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue blueLabel) + dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue blueLabel)) :
      0 ≤ (blueRootRedTrianglePacking configuration ⋯ ⋯).score barS

      A column obstruction makes support 71 a nonnegative-score endpoint packing.