The S0/S3 sibling incidence

This file closes the balanced/balanced orbit S0/S3. A common quadratic tangent controls the three positive cross distances. Two secants of the square root retain enough of the two larger radial penalties, and three exact rational Gram factorizations cover the resulting radial ranges.

theorem LeanPool.Besicovitch.gramCertificate_s0s3 (e p₁ p₂ w₁ w₂ : EuclideanSpace ℝ (Fin 2)) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 17 * ‖e - p₁ - w₁‖ + 20 * ‖e - p₂ - w₁‖ + 17 * ‖e - p₂ - w₂‖ - 10 * (barC + 1) * (‖p₁‖ + ‖w₂‖) - 10 * (barC - 1) * (‖p₂‖ + ‖w₁‖) + 54 * barC - 88 * barC ^ 2 < 0

A two-secant rational Gram separator for the S0/S3 incidence representative.

theorem LeanPool.Besicovitch.balancedBalancedS0S3GramBound_of_admissible {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : 7 * diagonalMatchingReducedSlack configuration + 20 * redBalancedReducedSlack configuration 0 + 20 * blueBalancedReducedSlack configuration 3 < 0

The S0/S3 separator is strictly negative for every admissible configuration.

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

The S0/S3 balanced/balanced representative is impossible.