Analytic separators for sibling lens cells

The off-matching coincident endpoint cell has a short global proof. Three norm tangents preserve the correlation between its cross distances. A rational two-by-two Gram majorant then separates the two colors, leaving a convex quadratic on the three radial vertices.

theorem LeanPool.Besicovitch.offMatchingCoincidentTangentCertificate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 14 * ‖e - p₁ - w₁‖ + 6 * ‖e - p₁ - w₂‖ + 6 * ‖e - p₂ - w₁‖ - 7 / 2 * ((barC - 1) * (‖p₁‖ + ‖w₁‖) + (barC + 1) * (‖p₂‖ + ‖w₂‖)) - 14 + 33 * barC - 45 * barC ^ 2 < 0

A global rational tangent separator for the off-matching coincident endpoint cell.

theorem LeanPool.Besicovitch.offMatchingCoincidentLensBound_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : OffMatchingCoincidentLensBound configuration

The off-matching coincident lens bound holds for every admissible configuration.

theorem LeanPool.Besicovitch.not_redEndpoint_one_and_blueEndpoint_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) : ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1))

The off-matching coincident endpoint representative is impossible.