The root--edge stage of the six-point failure tree

After the sibling supports choose the coincident endpoint B11, the two root--edge supports use the opposite children. This file connects their geometric packings to the root--edge minimax and records the elementary reductions shared by the two color directions.

noncomputable def LeanPool.Besicovitch.redRootEdgeTarget (configuration : SixPointConfiguration) : ℝ

The endpoint diameter target for the red root--second-child support.

Equations

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

noncomputable def LeanPool.Besicovitch.blueRootEdgeTarget (configuration : SixPointConfiguration) : ℝ

The endpoint diameter target for the blue root--second-child support.

Equations

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

noncomputable def LeanPool.Besicovitch.redRootEdgePackingAtEndpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (x : ℝ) (hxZero : 0 ≤ x) (hxEdge : x ≤ dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) : SixPointPacking configuration

Support 57, with the red root--second-child radius split at x.

Equations

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

noncomputable def LeanPool.Besicovitch.blueRootEdgePackingAtEndpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (x : ℝ) (hxZero : 0 ≤ x) (hxEdge : x ≤ dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) : SixPointPacking configuration

Support 75, with the blue root--second-child radius split at x.

Equations

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

theorem LeanPool.Besicovitch.redRootEdgePackingAtEndpoint_score_nonnegative (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (x : ℝ) (hxZero : 0 ≤ x) (hxEdge : x ≤ dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) (hdiameter : rootEdgeSplitDiameter (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) x (redRootBlueTriangleReach configuration) (redChildBlueTriangleReach configuration SixPointLabel.right) ≤ redRootEdgeTarget configuration) : 0 ≤ (redRootEdgePackingAtEndpoint configuration h x hxZero hxEdge).score barS

A feasible red root--edge split below its target gives nonnegative score.

theorem LeanPool.Besicovitch.blueRootEdgePackingAtEndpoint_score_nonnegative (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (x : ℝ) (hxZero : 0 ≤ x) (hxEdge : x ≤ dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) (hdiameter : rootEdgeSplitDiameter (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) x (blueRootRedTriangleReach configuration) (blueChildRedTriangleReach configuration SixPointLabel.right) ≤ blueRootEdgeTarget configuration) : 0 ≤ (blueRootEdgePackingAtEndpoint configuration h x hxZero hxEdge).score barS

A feasible blue root--edge split below its target gives nonnegative score.

def LeanPool.Besicovitch.RedRootEdgeFails (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) : Prop

Every feasible split of support 57 has negative score.

Equations

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

def LeanPool.Besicovitch.BlueRootEdgeFails (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) : Prop

Every feasible split of support 75 has negative score.

Equations

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

theorem LeanPool.Besicovitch.redRootEdge_split_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfailure : RedRootEdgeFails configuration h) (x : ℝ) (_hxZero : 0 ≤ x) (_hxEdge : x ≤ dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) : redRootEdgeTarget configuration < rootEdgeSplitDiameter (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) x (redRootBlueTriangleReach configuration) (redChildBlueTriangleReach configuration SixPointLabel.right)

Failure of support 57 makes every feasible root--edge split exceed its target.

theorem LeanPool.Besicovitch.blueRootEdge_split_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfailure : BlueRootEdgeFails configuration h) (x : ℝ) (_hxZero : 0 ≤ x) (_hxEdge : x ≤ dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) : blueRootEdgeTarget configuration < rootEdgeSplitDiameter (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) x (blueRootRedTriangleReach configuration) (blueChildRedTriangleReach configuration SixPointLabel.right)

Failure of support 75 makes every feasible root--edge split exceed its target.

theorem LeanPool.Besicovitch.SixPointConfiguration.blueRootEdgeInternalSlack_neg_of_matching_endpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : 0 ≤ matchingFailureSlack barC (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right))) (hendpoint : 0 ≤ blueEndpointFailureSlack barC (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (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.blue SixPointLabel.left))) : blueRootEdgeInternalSlack barC (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) < 0

The selected matching and blue coincident endpoint exclude the blue internal primitive.

theorem LeanPool.Besicovitch.redRootEdge_failure_routes_to_child_balanced {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hendpoint : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hfailure : RedRootEdgeFails configuration h) : 2 * redRootEdgeTarget configuration < dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + redRootBlueTriangleReach configuration SixPointLabel.left + redChildBlueTriangleReach configuration SixPointLabel.right SixPointLabel.left ∨ 2 * redRootEdgeTarget configuration < dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + redRootBlueTriangleReach configuration SixPointLabel.left + redChildBlueTriangleReach configuration SixPointLabel.right SixPointLabel.right

On the selected endpoint branch, failure of the red root--edge support can only use one of the two child-labelled balanced terms.

theorem LeanPool.Besicovitch.blueRootEdge_failure_routes_to_child_balanced {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hendpoint : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hfailure : BlueRootEdgeFails configuration h) : 2 * blueRootEdgeTarget configuration < dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + blueRootRedTriangleReach configuration SixPointLabel.left + blueChildRedTriangleReach configuration SixPointLabel.right SixPointLabel.left ∨ 2 * blueRootEdgeTarget configuration < dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + blueRootRedTriangleReach configuration SixPointLabel.left + blueChildRedTriangleReach configuration SixPointLabel.right SixPointLabel.right

The color-reversed root--edge failure has the same two surviving balanced terms.