The first stage of the six-point failure tree

For an admissible endpoint configuration, either a packing already has nonnegative score or one of the two perfect matchings of the four children satisfies the exact matching obstruction.

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

Every admissible endpoint configuration has a nonnegative packing or an obstructing child matching.