The sibling-triangle stage of the six-point failure tree

Once the diagonal matching obstruction is selected, supports 67 and 76 either provide a nonnegative-score packing or route their simultaneous failures into the finite incidence ledger.

theorem LeanPool.Besicovitch.exists_nonnegative_score_or_siblingIncidenceOutcome (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) : (∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS) ∨ SiblingIncidenceOutcome configuration

Under the diagonal matching obstruction, the two sibling-triangle supports either win or produce one of the residual incidence outcomes.

theorem LeanPool.Besicovitch.exists_nonnegative_score_or_siblingIncidence_or_antiDiagonal (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) : (∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS) ∨ SiblingIncidenceOutcome configuration ∨ (2 * barC - 1) * (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.right) + dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.left)

The first two packing stages leave only a sibling incidence or the anti-diagonal matching.