The closed sibling-incidence ledger

The five lens separators, together with the direct outside-orbit exclusions, rule out every simultaneous sibling failure except the two matched endpoint coincidences.

theorem LeanPool.Besicovitch.siblingIncidenceExclusions_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) : SiblingIncidenceExclusions (redSiblingTriangleFailure configuration) (blueSiblingTriangleFailure configuration)

Every non-matched sibling-incidence cell is excluded at the exact endpoint.

theorem LeanPool.Besicovitch.exists_nonnegative_score_or_matched_sibling_endpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) : (∃ (packing : SixPointPacking configuration), 0 ≤ packing.score barS) ∨ ∃ (code : Fin 4), (code = 0 ∨ code = 3) ∧ redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

The sibling supports either give a nonnegative packing or fail at one matched endpoint.