The E1/S0 sibling incidence

This file closes the endpoint/balanced orbit E1/S0. A rational factorization of its cross-term matrix preserves the correlation between the three positive distances. The resulting two colorwise quadratics are bounded on the three radial vertices.

theorem LeanPool.Besicovitch.gramCertificate_e1s0 {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₂‖) : 37 / 20 * ‖e - p₁ - w₁‖ + 21 / 8 * ‖e - p₁ - w₂‖ + 27 / 20 * ‖e - p₂ - w₂‖ - ((barC - 1) * ‖p₁‖ + (barC + 1) * ‖p₂‖) / 2 - 17 / 16 * ((barC + 1) * ‖w₁‖ + (barC - 1) * ‖w₂‖) - 17 / 8 + 551 / 80 * barC - 807 / 80 * barC ^ 2 < 0

A rational Gram separator for the E1/S0 incidence representative.

theorem LeanPool.Besicovitch.endpointBalancedE1S0GramBound_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : 27 / 20 * diagonalMatchingReducedSlack configuration + 17 / 8 * redEndpointReducedSlack configuration 1 + blueBalancedReducedSlack configuration 0 < 0

The alternative positive separator is strictly negative for every admissible configuration.

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

The E1/S0 endpoint/balanced representative is impossible.