The S0/S0 sibling incidence

This file closes the balanced/balanced orbit S0/S0. Four norm tangents retain their full two-by-two incidence matrix. A rational positive-semidefinite factorization then separates the two colors, leaving two copies of the three-vertex radial estimate.

theorem LeanPool.Besicovitch.gramCertificate_s0s0 {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₂‖) : 22 / 15 * ‖e - p₁ - w₁‖ + 1 / 2 * ‖e - p₁ - w₂‖ + 1 / 2 * ‖e - p₂ - w₁‖ + 7 / 15 * ‖e - p₂ - w₂‖ - ((barC - 1) * (‖p₁‖ + ‖w₁‖) + (barC + 1) * (‖p₂‖ + ‖w₂‖)) / 2 - 14 / 15 * barC * (2 * barC - 1) + 2 * barC - 3 * barC ^ 2 < 0

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

theorem LeanPool.Besicovitch.balancedBalancedS0S0GramBound_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : 7 / 15 * diagonalMatchingReducedSlack configuration + redBalancedReducedSlack configuration 0 + blueBalancedReducedSlack configuration 0 < 0

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

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

The S0/S0 balanced/balanced representative is impossible.