Root--edge packings

This file develops the one-dimensional minimax for a root--child edge against the full opposite triangle. It also proves the exact rational separator that excludes an internal triangle primitive on the matching branch of the endpoint failure tree.

def LeanPool.Besicovitch.rootEdgeCrossMaximum (R x : ℝ) (rootReach childReach : SixPointLabel → ℝ) : ℝ

The cross-color part of a root-edge split with edge length R.

Equations

• LeanPool.Besicovitch.rootEdgeCrossMaximum R x rootReach childReach = max (x + LeanPool.Besicovitch.triangleMaximum rootReach) (R - x + LeanPool.Besicovitch.triangleMaximum childReach)

def LeanPool.Besicovitch.rootEdgeSplitDiameter (R M x : ℝ) (rootReach childReach : SixPointLabel → ℝ) : ℝ

The diameter of a root-edge split after its same-color terms are reduced to 2M.

Equations

• LeanPool.Besicovitch.rootEdgeSplitDiameter R M x rootReach childReach = max (2 * M) (LeanPool.Besicovitch.rootEdgeCrossMaximum R x rootReach childReach)

theorem LeanPool.Besicovitch.exists_rootEdge_split_iff {R M T : ℝ} {rootReach childReach : SixPointLabel → ℝ} (hR : 0 ≤ R) : (∃ (x : ℝ), 0 ≤ x ∧ x ≤ R ∧ rootEdgeSplitDiameter R M x rootReach childReach ≤ T) ↔ 2 * M ≤ T ∧ (∀ (label : SixPointLabel), rootReach label ≤ T) ∧ (∀ (label : SixPointLabel), childReach label ≤ T) ∧ ∀ (rootLabel childLabel : SixPointLabel), R + rootReach rootLabel + childReach childLabel ≤ 2 * T

Exact threshold form of the sixteen-term root-edge minimax.

theorem LeanPool.Besicovitch.rootEdge_failure_routing {R M T : ℝ} {rootReach childReach : SixPointLabel → ℝ} (hR : 0 ≤ R) (hfail : ∀ (x : ℝ), 0 ≤ x → x ≤ R → T < rootEdgeSplitDiameter R M x rootReach childReach) : T < 2 * M ∨ (∃ (label : SixPointLabel), T < rootReach label) ∨ (∃ (label : SixPointLabel), T < childReach label) ∨ ∃ (rootLabel : SixPointLabel) (childLabel : SixPointLabel), 2 * T < R + rootReach rootLabel + childReach childLabel

Failure of every root-edge split selects one of its sixteen routing terms.

theorem LeanPool.Besicovitch.rootEdge_failure_reduces_to_three_types {R M T : ℝ} {rootReach childReach : SixPointLabel → ℝ} (hR : 0 < R) (hrootRoot : rootReach SixPointLabel.root ≤ T - R) (hchildRoot : childReach SixPointLabel.root ≤ T - R) (hleftLower : T - R ≤ rootReach SixPointLabel.left) (hleftLargest : rootReach SixPointLabel.right < rootReach SixPointLabel.left) (hclose : ∀ (label : SixPointLabel), label ≠ SixPointLabel.root → rootReach label - R ≤ childReach label) (hroute : T < 2 * M ∨ (∃ (label : SixPointLabel), T < rootReach label) ∨ (∃ (label : SixPointLabel), T < childReach label) ∨ ∃ (rootLabel : SixPointLabel) (childLabel : SixPointLabel), 2 * T < R + rootReach rootLabel + childReach childLabel) : T < 2 * M ∨ 2 * T < R + rootReach SixPointLabel.left + childReach SixPointLabel.left ∨ 2 * T < R + rootReach SixPointLabel.left + childReach SixPointLabel.right

The sixteen root-edge terms reduce pointwise to internal, (1,1), or (1,2).

noncomputable def LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) : SixPointPacking configuration

Supports 37 and 57: a red root--child edge against the full blue triangle.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking_radius_root (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (hmem : (SixPointColor.red, SixPointLabel.root) ∈ (redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).support) : ↑((redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).radius ⟨(SixPointColor.red, SixPointLabel.root), hmem⟩) = x

The radius at the red root is the split variable.

@[simp]

theorem LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking_radius_child (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (hmem : (SixPointColor.red, redLabel) ∈ (redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).support) : ↑((redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).radius ⟨(SixPointColor.red, redLabel), hmem⟩) = R - x

The radius at the selected red child is the complementary split.

@[simp]

theorem LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking_radius_blue (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (label : SixPointLabel) (hmem : (SixPointColor.blue, label) ∈ (redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).support) : ↑((redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).radius ⟨(SixPointColor.blue, label), hmem⟩) = canonicalTriangleRadius (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) label

Blue radii in a red root-edge packing are the canonical triangle radii.

theorem LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking_totalRadius (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) : (redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).totalRadius = R + (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.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) / 2

The total radius of a red root-edge packing is its edge length plus a semiperimeter.

noncomputable def LeanPool.Besicovitch.redRootBlueTriangleReach (configuration : SixPointConfiguration) (label : SixPointLabel) : ℝ

Cross reach from the red root to a labelled blue triangle ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.redChildBlueTriangleReach (configuration : SixPointConfiguration) (redLabel blueLabel : SixPointLabel) : ℝ

Cross reach from a red child to a labelled blue triangle ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.blueRootEdgeRedTrianglePacking (configuration : SixPointConfiguration) (blueLabel : SixPointLabel) (hblueLabel : blueLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue blueLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) : SixPointPacking configuration

Supports 73 and 75: a blue root--child edge against the full red triangle.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.redRootEdgeBlueTrianglePacking_virtualDiameter (configuration : SixPointConfiguration) (redLabel : SixPointLabel) (hredLabel : redLabel ≠ SixPointLabel.root) {R M x : ℝ} (hRdist : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red redLabel) = R) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hR_one : R ≤ 1) (hM : 1 ≤ M) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) : (redRootEdgeBlueTrianglePacking configuration redLabel hredLabel hRdist hR_one hx_zero hx_R hblueLeft hblueRight).virtualDiameter = rootEdgeSplitDiameter R M x (redRootBlueTriangleReach configuration) (redChildBlueTriangleReach configuration redLabel)

The virtual diameter of supports 37 and 57 is the root-edge split diameter.

theorem LeanPool.Besicovitch.blueRootEdgeRedTrianglePacking_totalRadius (configuration : SixPointConfiguration) (blueLabel : SixPointLabel) (hblueLabel : blueLabel ≠ SixPointLabel.root) {R x : ℝ} (hRdist : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue blueLabel) = R) (hR_one : R ≤ 1) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) : (blueRootEdgeRedTrianglePacking configuration blueLabel hblueLabel hRdist hR_one hx_zero hx_R hredLeft hredRight).totalRadius = R + (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) + dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) / 2

The total radius of a blue root-edge packing is its edge length plus a semiperimeter.

noncomputable def LeanPool.Besicovitch.blueRootRedTriangleReach (configuration : SixPointConfiguration) (label : SixPointLabel) : ℝ

Cross reach from the blue root to a labelled red triangle ball.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.blueChildRedTriangleReach (configuration : SixPointConfiguration) (blueLabel redLabel : SixPointLabel) : ℝ

Cross reach from a blue child to a labelled red triangle ball.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.blueRootEdgeRedTrianglePacking_virtualDiameter (configuration : SixPointConfiguration) (blueLabel : SixPointLabel) (hblueLabel : blueLabel ≠ SixPointLabel.root) {R L x : ℝ} (hRdist : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue blueLabel) = R) (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hR_one : R ≤ 1) (hL : 1 ≤ L) (hx_zero : 0 ≤ x) (hx_R : x ≤ R) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) : (blueRootEdgeRedTrianglePacking configuration blueLabel hblueLabel hRdist hR_one hx_zero hx_R hredLeft hredRight).virtualDiameter = rootEdgeSplitDiameter R L x (blueRootRedTriangleReach configuration) (blueChildRedTriangleReach configuration blueLabel)

The virtual diameter of supports 73 and 75 is the root-edge split diameter.

theorem LeanPool.Besicovitch.midpoint_crossDistance_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e p w : E) : ‖e - p - w‖ ≤ (‖e - 2 • p‖ + ‖e - 2 • w‖) / 2

Midpoint convexity splits a cross distance into one term for each color.

theorem LeanPool.Besicovitch.rootEdge_internal_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₂‖) : 25 * ‖e - p₁ - w₁‖ + 19 * ‖e - p₂ - w₂‖ + (3 - 15 * barC) * ‖w₁‖ - (15 * barC + 3) * ‖w₂‖ - 24 * barC * ‖p₂‖ + 95 * barC - 97 * barC ^ 2 - 6 < 0

The exact two-point tangent certificate for the root-edge internal separator.

def LeanPool.Besicovitch.matchingFailureSlack (c L M B₁₁ B₂₂ : ℝ) : ℝ

Failure slack for the diagonal four-child matching.

Equations

• LeanPool.Besicovitch.matchingFailureSlack c L M B₁₁ B₂₂ = B₁₁ + B₂₂ - (2 * c - 1) * (L + M)

noncomputable def LeanPool.Besicovitch.redEndpointFailureSlack (c L M b₁ b₂ B₁₁ : ℝ) : ℝ

Failure slack for the red coincident endpoint on the first matching edge.

Equations

• LeanPool.Besicovitch.redEndpointFailureSlack c L M b₁ b₂ B₁₁ = L - 1 + B₁₁ + (b₁ + M - b₂) / 2 - c * (L + (b₁ + b₂ + M) / 2)

noncomputable def LeanPool.Besicovitch.redRootEdgeInternalSlack (c M r₂ b₁ b₂ : ℝ) : ℝ

Internal failure slack for the red root--second-child edge.

Equations

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

noncomputable def LeanPool.Besicovitch.blueEndpointFailureSlack (c L M r₁ r₂ B₁₁ : ℝ) : ℝ

Failure slack for the blue coincident endpoint on the first matching edge.

Equations

• LeanPool.Besicovitch.blueEndpointFailureSlack c L M r₁ r₂ B₁₁ = M - 1 + B₁₁ + (r₁ + L - r₂) / 2 - c * (M + (r₁ + r₂ + L) / 2)

noncomputable def LeanPool.Besicovitch.blueRootEdgeInternalSlack (c L b₂ r₁ r₂ : ℝ) : ℝ

Internal failure slack for the blue root--second-child edge.

Equations

• LeanPool.Besicovitch.blueRootEdgeInternalSlack c L b₂ r₁ r₂ = 2 * L - c * (b₂ + (r₁ + r₂ + L) / 2)

theorem LeanPool.Besicovitch.rootEdge_internal_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₂‖) : 19 * matchingFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖e - p₁ - w₁‖ ‖e - p₂ - w₂‖ + 6 * redEndpointFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖w₁‖ ‖w₂‖ ‖e - p₁ - w₁‖ + 24 * redRootEdgeInternalSlack barC ‖w₁ - w₂‖ ‖p₂‖ ‖w₁‖ ‖w₂‖ < 0

The internal root-edge slack has a strictly negative positive separator.

theorem LeanPool.Besicovitch.redRootEdgeInternalSlack_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₁‖) : redRootEdgeInternalSlack barC ‖w₁ - w₂‖ ‖p₂‖ ‖w₁‖ ‖w₂‖ < 0

A matching and its coincident endpoint exclude the red internal root-edge failure.

theorem LeanPool.Besicovitch.blueRootEdge_internal_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₂‖) : 19 * matchingFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖e - p₁ - w₁‖ ‖e - p₂ - w₂‖ + 6 * blueEndpointFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖p₁‖ ‖p₂‖ ‖e - p₁ - w₁‖ + 24 * blueRootEdgeInternalSlack barC ‖p₁ - p₂‖ ‖w₂‖ ‖p₁‖ ‖p₂‖ < 0

The color-transposed internal root-edge slack has the same strict separator.

theorem LeanPool.Besicovitch.blueRootEdgeInternalSlack_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 ≤ blueEndpointFailureSlack barC ‖p₁ - p₂‖ ‖w₁ - w₂‖ ‖p₁‖ ‖p₂‖ ‖e - p₁ - w₁‖) : blueRootEdgeInternalSlack barC ‖p₁ - p₂‖ ‖w₂‖ ‖p₁‖ ‖p₂‖ < 0

A matching and its coincident endpoint exclude the blue internal root-edge failure.

theorem LeanPool.Besicovitch.SixPointConfiguration.redRootEdgeInternalSlack_neg_of_matching_endpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (hmatching : 0 ≤ matchingFailureSlack barC (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left)) (dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right))) (hendpoint : 0 ≤ redEndpointFailureSlack barC (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue 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.left) (configuration SixPointColor.blue SixPointLabel.left))) : redRootEdgeInternalSlack 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)) < 0

In an admissible configuration, a diagonal matching and its red coincident endpoint rule out the red root-edge internal primitive.