Documentation

LeanPool.Besicovitch.SixPoint.RootEdgeClosed

Closing the root--edge failure stage #

The crossed (1,2) separator removes the second branch of each root--edge minimax. Thus the two root--edge supports either provide a nonnegative packing or both select their (1,1) terms.

source
theorem LeanPool.Besicovitch.redRootEdge_failure_forces_type11 {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

The selected matching and endpoint force a failed red root--edge support onto (1,1).

source
theorem LeanPool.Besicovitch.blueRootEdge_failure_forces_type11 {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

The selected matching and endpoint force a failed blue root--edge support onto (1,1).

source
theorem LeanPool.Besicovitch.exists_nonnegative_score_or_rootEdge_type11_pair (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hredEndpoint : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hblueEndpoint : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) :
(∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS) ∨ 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 * blueRootEdgeTarget configuration < dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + blueRootRedTriangleReach configuration SixPointLabel.left + blueChildRedTriangleReach configuration SixPointLabel.right SixPointLabel.left

The two root--edge supports either win or both leave the active (1,1) inequalities.