Closing the matched-endpoint branch

At a matched sibling endpoint, failure of both root--edge packings makes the three active slacks strictly incompatible with the weighted geometric bound. The other matched endpoint follows by simultaneously swapping both pairs of children.

theorem LeanPool.Besicovitch.exists_nonnegative_score_of_matched_endpoint_zero (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) {lambda mu : ℝ} (hlambda : 0 < lambda) (hmu : 0 < mu) (hmatching : SelectedDiagonalMatchingFails configuration) (hred : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hblue : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hweighted : weightedPairScore configuration.rootDisplacement barC lambda mu (configuration.redDisplacement SixPointLabel.left) (configuration.redDisplacement SixPointLabel.right) (configuration.bluePullback SixPointLabel.left) (configuration.bluePullback SixPointLabel.right) ≤ 0) : ∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS

The weighted geometric bound closes the endpoint at the two left children.

theorem LeanPool.Besicovitch.exists_nonnegative_score_of_matched_endpoint_three (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) {lambda mu : ℝ} (hlambda : 0 < lambda) (hmu : 0 < mu) (hmatching : SelectedDiagonalMatchingFails configuration) (hred : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 3)) (hblue : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 3)) (hweighted : weightedPairScore (swapConfigurationChildren configuration).rootDisplacement barC lambda mu ((swapConfigurationChildren configuration).redDisplacement SixPointLabel.left) ((swapConfigurationChildren configuration).redDisplacement SixPointLabel.right) ((swapConfigurationChildren configuration).bluePullback SixPointLabel.left) ((swapConfigurationChildren configuration).bluePullback SixPointLabel.right) ≤ 0) : ∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS

The weighted geometric bound closes the endpoint at the two right children.