The crossed root--edge (1,2) obstruction

This file excludes the crossed term in the root--edge minimax. The proof uses the positive separator with weights 1, 1, 2. Three scalar norm tangents reduce it to one fixed rational Gram certificate; radial secants use only the sibling separation and the unit-ball bounds.

noncomputable def LeanPool.Besicovitch.redRootEdgeType12Slack (c M r₂ b₁ b₂ rootToBlueFirst secondCross : ℝ) : ℝ

Failure slack of the crossed (1,2) term for a red root--second-child edge.

Equations

• LeanPool.Besicovitch.redRootEdgeType12Slack c M r₂ b₁ b₂ rootToBlueFirst secondCross = r₂ + rootToBlueFirst + secondCross + M - 2 * c * (r₂ + (b₁ + b₂ + M) / 2)

theorem LeanPool.Besicovitch.rootEdge_type12_expanded_lt {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) (hredSeparation : barC ≤ ‖p₁ - p₂‖) (hblueSeparation : barC ≤ ‖w₁ - w₂‖) : ‖e - p₁ - w₁‖ + 3 / 2 * ‖e - p₂ - w₂‖ + ‖e - w₁‖ + (2 - 3 * barC) / 2 * ‖p₁ - p₂‖ + (7 - 9 * barC) / 4 * ‖w₁ - w₂‖ + (1 - 5 * barC) / 4 * ‖w₁‖ - (1 + 5 * barC) / 4 * ‖w₂‖ + (1 - 2 * barC) * ‖p₂‖ - 1 / 2 < 0

The exact Gram separator for the crossed root--edge term.

theorem LeanPool.Besicovitch.rootEdge_type12_separator_lt {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) (hredSeparation : barC ≤ ‖p₁ - p₂‖) (hblueSeparation : barC ≤ ‖w₁ - w₂‖) : matchingFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖e - p₁ - w₁‖ ‖e - p₂ - w₂‖ + redEndpointFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖w₁‖ ‖w₂‖ ‖e - p₁ - w₁‖ + 2 * redRootEdgeType12Slack barC ‖w₁ - w₂‖ ‖p₂‖ ‖w₁‖ ‖w₂‖ ‖e - w₁‖ ‖e - p₂ - w₂‖ < 0

Matching, endpoint, and crossed root--edge slacks have a strictly negative separator.

theorem LeanPool.Besicovitch.redRootEdgeType12Slack_neg {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) (hredSeparation : barC ≤ ‖p₁ - p₂‖) (hblueSeparation : barC ≤ ‖w₁ - w₂‖) (hmatching : 0 ≤ matchingFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖e - p₁ - w₁‖ ‖e - p₂ - w₂‖) (hendpoint : 0 ≤ redEndpointFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖w₁‖ ‖w₂‖ ‖e - p₁ - w₁‖) : redRootEdgeType12Slack barC ‖w₁ - w₂‖ ‖p₂‖ ‖w₁‖ ‖w₂‖ ‖e - w₁‖ ‖e - p₂ - w₂‖ < 0

A matching and its first coincident endpoint exclude the crossed red root--edge term.

theorem LeanPool.Besicovitch.SixPointConfiguration.redRootEdgeType12Slack_neg_of_matching_endpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hendpoint : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) : redRootEdgeType12Slack barC (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right)) < 0

In an admissible configuration, the selected matching and endpoint code 0 exclude the red crossed (left,right) root--edge term.