Incidences in the sibling--triangle branch

This file encodes the finite incidence ledger for simultaneous failures of supports 67 and 76. Endpoint and balanced witnesses use the four codes from the paper, and the orbit types are exactly the six, eight, and seven cases left by the fixed diagonal matching.

def LeanPool.Besicovitch.incidenceChild : Fin 2 → SixPointLabel

The child at one coordinate of an incidence code.

Equations

• LeanPool.Besicovitch.incidenceChild 0 = LeanPool.Besicovitch.SixPointLabel.left
• LeanPool.Besicovitch.incidenceChild 1 = LeanPool.Besicovitch.SixPointLabel.right

def LeanPool.Besicovitch.otherChild : Fin 2 → Fin 2

The other child index.

Equations

• LeanPool.Besicovitch.otherChild 0 = 1
• LeanPool.Besicovitch.otherChild 1 = 0

def LeanPool.Besicovitch.incidenceFirst : Fin 4 → Fin 2

The first child coordinate in the code 2 i + j.

Equations

• LeanPool.Besicovitch.incidenceFirst 0 = 0
• LeanPool.Besicovitch.incidenceFirst 1 = 0
• LeanPool.Besicovitch.incidenceFirst 2 = 1
• LeanPool.Besicovitch.incidenceFirst 3 = 1

def LeanPool.Besicovitch.incidenceSecond : Fin 4 → Fin 2

The second child coordinate in the code 2 i + j.

Equations

• LeanPool.Besicovitch.incidenceSecond 0 = 0
• LeanPool.Besicovitch.incidenceSecond 1 = 1
• LeanPool.Besicovitch.incidenceSecond 2 = 0
• LeanPool.Besicovitch.incidenceSecond 3 = 1

inductive LeanPool.Besicovitch.SiblingTriangleWitness : Type

A sibling--triangle failure is witnessed by an endpoint or a balanced pair of terms.

• endpoint (code : Fin 4) : SiblingTriangleWitness
• balanced (code : Fin 4) : SiblingTriangleWitness

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqSiblingTriangleWitness : DecidableEq SiblingTriangleWitness

Equations

• LeanPool.Besicovitch.instDecidableEqSiblingTriangleWitness = LeanPool.Besicovitch.instDecidableEqSiblingTriangleWitness.decEq

def LeanPool.Besicovitch.instDecidableEqSiblingTriangleWitness.decEq (x✝ x✝¹ : SiblingTriangleWitness) : Decidable (x✝ = x✝¹)

Equations

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

def LeanPool.Besicovitch.swapEndpointCode : Fin 4 → Fin 4

Simultaneously swapping the two children sends an endpoint code a to 3 - a.

Equations

• LeanPool.Besicovitch.swapEndpointCode 0 = 3
• LeanPool.Besicovitch.swapEndpointCode 1 = 2
• LeanPool.Besicovitch.swapEndpointCode 2 = 1
• LeanPool.Besicovitch.swapEndpointCode 3 = 0

def LeanPool.Besicovitch.transposeEndpointCode : Fin 4 → Fin 4

Transposing the two colors transposes an endpoint's two coordinates.

Equations

• LeanPool.Besicovitch.transposeEndpointCode 0 = 0
• LeanPool.Besicovitch.transposeEndpointCode 1 = 2
• LeanPool.Besicovitch.transposeEndpointCode 2 = 1
• LeanPool.Besicovitch.transposeEndpointCode 3 = 3

def LeanPool.Besicovitch.transposeBlueEndpointWitness : SiblingTriangleWitness → SiblingTriangleWitness

Put a blue endpoint witness into the common (red child, blue child) code convention.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Besicovitch.transposeBlueEndpointWitness (LeanPool.Besicovitch.SiblingTriangleWitness.balanced code) = LeanPool.Besicovitch.SiblingTriangleWitness.balanced code

def LeanPool.Besicovitch.swapBalancedCode : Fin 4 → Fin 4

Simultaneously swapping the children exchanges balanced codes 0 and 3.

Equations

• LeanPool.Besicovitch.swapBalancedCode 0 = 3
• LeanPool.Besicovitch.swapBalancedCode 1 = 1
• LeanPool.Besicovitch.swapBalancedCode 2 = 2
• LeanPool.Besicovitch.swapBalancedCode 3 = 0

inductive LeanPool.Besicovitch.EndpointEndpointOrbit : Type

The six endpoint--endpoint orbits relative to the diagonal matching.

• matchedCoincident : EndpointEndpointOrbit
• offMatchingCoincident : EndpointEndpointOrbit
• adjacentFirst : EndpointEndpointOrbit
• adjacentSecond : EndpointEndpointOrbit
• matchingDisjoint : EndpointEndpointOrbit
• offMatchingDisjoint : EndpointEndpointOrbit

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqEndpointEndpointOrbit : DecidableEq EndpointEndpointOrbit

Equations

• LeanPool.Besicovitch.instDecidableEqEndpointEndpointOrbit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive LeanPool.Besicovitch.EndpointBalancedOrbit : Type

The eight endpoint--balanced orbits after orienting the endpoint from red to blue.

• e0s0 : EndpointBalancedOrbit
• e0s1 : EndpointBalancedOrbit
• e0s2 : EndpointBalancedOrbit
• e0s3 : EndpointBalancedOrbit
• e1s0 : EndpointBalancedOrbit
• e1s1 : EndpointBalancedOrbit
• e1s2 : EndpointBalancedOrbit
• e1s3 : EndpointBalancedOrbit

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqEndpointBalancedOrbit : DecidableEq EndpointBalancedOrbit

Equations

• LeanPool.Besicovitch.instDecidableEqEndpointBalancedOrbit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive LeanPool.Besicovitch.BalancedBalancedOrbit : Type

The seven balanced--balanced orbits relative to the diagonal matching.

• s0s0 : BalancedBalancedOrbit
• s0s3 : BalancedBalancedOrbit
• s0s1 : BalancedBalancedOrbit
• s0s2 : BalancedBalancedOrbit
• s1s1 : BalancedBalancedOrbit
• s1s2 : BalancedBalancedOrbit
• s2s2 : BalancedBalancedOrbit

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqBalancedBalancedOrbit : DecidableEq BalancedBalancedOrbit

Equations

• LeanPool.Besicovitch.instDecidableEqBalancedBalancedOrbit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanPool.Besicovitch.endpointEndpointOrbit : Fin 4 → Fin 4 → EndpointEndpointOrbit

Classify an ordered pair of endpoint codes under child swap and color transposition.

Equations

• LeanPool.Besicovitch.endpointEndpointOrbit 0 0 = LeanPool.Besicovitch.EndpointEndpointOrbit.matchedCoincident
• LeanPool.Besicovitch.endpointEndpointOrbit 3 3 = LeanPool.Besicovitch.EndpointEndpointOrbit.matchedCoincident
• LeanPool.Besicovitch.endpointEndpointOrbit 1 1 = LeanPool.Besicovitch.EndpointEndpointOrbit.offMatchingCoincident
• LeanPool.Besicovitch.endpointEndpointOrbit 2 2 = LeanPool.Besicovitch.EndpointEndpointOrbit.offMatchingCoincident
• LeanPool.Besicovitch.endpointEndpointOrbit 0 1 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentFirst
• LeanPool.Besicovitch.endpointEndpointOrbit 3 2 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentFirst
• LeanPool.Besicovitch.endpointEndpointOrbit 2 0 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentFirst
• LeanPool.Besicovitch.endpointEndpointOrbit 1 3 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentFirst
• LeanPool.Besicovitch.endpointEndpointOrbit 0 2 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentSecond
• LeanPool.Besicovitch.endpointEndpointOrbit 3 1 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentSecond
• LeanPool.Besicovitch.endpointEndpointOrbit 1 0 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentSecond
• LeanPool.Besicovitch.endpointEndpointOrbit 2 3 = LeanPool.Besicovitch.EndpointEndpointOrbit.adjacentSecond
• LeanPool.Besicovitch.endpointEndpointOrbit 0 3 = LeanPool.Besicovitch.EndpointEndpointOrbit.matchingDisjoint
• LeanPool.Besicovitch.endpointEndpointOrbit 3 0 = LeanPool.Besicovitch.EndpointEndpointOrbit.matchingDisjoint
• LeanPool.Besicovitch.endpointEndpointOrbit 1 2 = LeanPool.Besicovitch.EndpointEndpointOrbit.offMatchingDisjoint
• LeanPool.Besicovitch.endpointEndpointOrbit 2 1 = LeanPool.Besicovitch.EndpointEndpointOrbit.offMatchingDisjoint

def LeanPool.Besicovitch.endpointBalancedOrbit : Fin 4 → Fin 4 → EndpointBalancedOrbit

Classify an endpoint code and a balanced code under simultaneous child swap.

Equations

• LeanPool.Besicovitch.endpointBalancedOrbit 0 0 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s0
• LeanPool.Besicovitch.endpointBalancedOrbit 3 3 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s0
• LeanPool.Besicovitch.endpointBalancedOrbit 0 1 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s1
• LeanPool.Besicovitch.endpointBalancedOrbit 3 1 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s1
• LeanPool.Besicovitch.endpointBalancedOrbit 0 2 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s2
• LeanPool.Besicovitch.endpointBalancedOrbit 3 2 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s2
• LeanPool.Besicovitch.endpointBalancedOrbit 0 3 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s3
• LeanPool.Besicovitch.endpointBalancedOrbit 3 0 = LeanPool.Besicovitch.EndpointBalancedOrbit.e0s3
• LeanPool.Besicovitch.endpointBalancedOrbit 1 0 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s0
• LeanPool.Besicovitch.endpointBalancedOrbit 2 3 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s0
• LeanPool.Besicovitch.endpointBalancedOrbit 1 1 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s1
• LeanPool.Besicovitch.endpointBalancedOrbit 2 1 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s1
• LeanPool.Besicovitch.endpointBalancedOrbit 1 2 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s2
• LeanPool.Besicovitch.endpointBalancedOrbit 2 2 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s2
• LeanPool.Besicovitch.endpointBalancedOrbit 1 3 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s3
• LeanPool.Besicovitch.endpointBalancedOrbit 2 0 = LeanPool.Besicovitch.EndpointBalancedOrbit.e1s3

def LeanPool.Besicovitch.balancedBalancedOrbit : Fin 4 → Fin 4 → BalancedBalancedOrbit

Classify an ordered pair of balanced codes under child swap and color transposition.

Equations

• LeanPool.Besicovitch.balancedBalancedOrbit 0 0 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s0
• LeanPool.Besicovitch.balancedBalancedOrbit 3 3 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s0
• LeanPool.Besicovitch.balancedBalancedOrbit 0 3 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s3
• LeanPool.Besicovitch.balancedBalancedOrbit 3 0 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s3
• LeanPool.Besicovitch.balancedBalancedOrbit 0 1 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s1
• LeanPool.Besicovitch.balancedBalancedOrbit 3 1 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s1
• LeanPool.Besicovitch.balancedBalancedOrbit 1 0 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s1
• LeanPool.Besicovitch.balancedBalancedOrbit 1 3 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s1
• LeanPool.Besicovitch.balancedBalancedOrbit 0 2 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s2
• LeanPool.Besicovitch.balancedBalancedOrbit 3 2 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s2
• LeanPool.Besicovitch.balancedBalancedOrbit 2 0 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s2
• LeanPool.Besicovitch.balancedBalancedOrbit 2 3 = LeanPool.Besicovitch.BalancedBalancedOrbit.s0s2
• LeanPool.Besicovitch.balancedBalancedOrbit 1 1 = LeanPool.Besicovitch.BalancedBalancedOrbit.s1s1
• LeanPool.Besicovitch.balancedBalancedOrbit 1 2 = LeanPool.Besicovitch.BalancedBalancedOrbit.s1s2
• LeanPool.Besicovitch.balancedBalancedOrbit 2 1 = LeanPool.Besicovitch.BalancedBalancedOrbit.s1s2
• LeanPool.Besicovitch.balancedBalancedOrbit 2 2 = LeanPool.Besicovitch.BalancedBalancedOrbit.s2s2

theorem LeanPool.Besicovitch.endpointEndpointOrbit_eq_matchedCoincident_iff (redCode blueCode : Fin 4) : endpointEndpointOrbit redCode blueCode = EndpointEndpointOrbit.matchedCoincident ↔ redCode = 0 ∧ blueCode = 0 ∨ redCode = 3 ∧ blueCode = 3

The matched coincident orbit consists exactly of the two diagonal coincidences.

@[simp]

theorem LeanPool.Besicovitch.endpointEndpointOrbit_swap (redCode blueCode : Fin 4) : endpointEndpointOrbit (swapEndpointCode redCode) (swapEndpointCode blueCode) = endpointEndpointOrbit redCode blueCode

The endpoint--endpoint classifier is unchanged by simultaneous child swap.

@[simp]

theorem LeanPool.Besicovitch.endpointEndpointOrbit_transpose (redCode blueCode : Fin 4) : endpointEndpointOrbit (transposeEndpointCode blueCode) (transposeEndpointCode redCode) = endpointEndpointOrbit redCode blueCode

The endpoint--endpoint classifier is unchanged by color transposition.

@[simp]

theorem LeanPool.Besicovitch.endpointBalancedOrbit_swap (endpointCode balancedCode : Fin 4) : endpointBalancedOrbit (swapEndpointCode endpointCode) (swapBalancedCode balancedCode) = endpointBalancedOrbit endpointCode balancedCode

The endpoint--balanced classifier is unchanged by simultaneous child swap.

@[simp]

theorem LeanPool.Besicovitch.balancedBalancedOrbit_swap (redCode blueCode : Fin 4) : balancedBalancedOrbit (swapBalancedCode redCode) (swapBalancedCode blueCode) = balancedBalancedOrbit redCode blueCode

The balanced--balanced classifier is unchanged by simultaneous child swap.

theorem LeanPool.Besicovitch.balancedBalancedOrbit_transpose (redCode blueCode : Fin 4) : balancedBalancedOrbit blueCode redCode = balancedBalancedOrbit redCode blueCode

The balanced--balanced classifier is unchanged by color transposition.

def LeanPool.Besicovitch.siblingTriangleWitnessExceeds (L T : ℝ) (leftReach rightReach : SixPointLabel → ℝ) : SiblingTriangleWitness → Prop

The threshold inequality selected by an endpoint or balanced sibling witness.

Equations

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

theorem LeanPool.Besicovitch.exists_siblingTriangleWitnessExceeds_of_failure {L M T : ℝ} {leftReach rightReach : SixPointLabel → ℝ} (hL : L ≤ 2) (hsameL : 2 * L ≤ T) (hsameM : 2 * M ≤ T) (hleftRoot : L - 1 + leftReach SixPointLabel.root ≤ T) (hrightRoot : L - 1 + rightReach SixPointLabel.root ≤ T) (hbalancedRoot : ∀ (leftLabel rightLabel : SixPointLabel), leftLabel = SixPointLabel.root ∨ rightLabel = SixPointLabel.root → L + leftReach leftLabel + rightReach rightLabel ≤ 2 * T) (hfail : ∀ (x : ℝ), L - 1 ≤ x → x ≤ 1 → T < siblingTriangleSplitDiameter L M x leftReach rightReach) : ∃ (witness : SiblingTriangleWitness), siblingTriangleWitnessExceeds L T leftReach rightReach witness

Removing root-labelled primitives turns the minimax route into one of the eight incidences.

noncomputable def LeanPool.Besicovitch.rootedTriangleTotalRadius (configuration : SixPointConfiguration) (color : SixPointColor) : ℝ

The total canonical radius of one color's rooted triangle.

Equations

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

noncomputable def LeanPool.Besicovitch.redSiblingTriangleTarget (configuration : SixPointConfiguration) : ℝ

The diameter threshold for support 67 at the exact endpoint.

Equations

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

noncomputable def LeanPool.Besicovitch.blueSiblingTriangleTarget (configuration : SixPointConfiguration) : ℝ

The diameter threshold for support 76 at the exact endpoint.

Equations

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

def LeanPool.Besicovitch.redSiblingTriangleFailure (configuration : SixPointConfiguration) : SiblingTriangleWitness → Prop

The exact endpoint or balanced failure inequality for support 67.

Equations

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

def LeanPool.Besicovitch.blueSiblingTriangleFailure (configuration : SixPointConfiguration) : SiblingTriangleWitness → Prop

The exact endpoint or balanced failure inequality for support 76.

Equations

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

noncomputable def LeanPool.Besicovitch.matchedChildAverage (configuration : SixPointConfiguration) (child : Fin 2) : ℝ

The average of the two root-to-child distances at a matched child index.

Equations

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

theorem LeanPool.Besicovitch.sibling_distance_mem_endpoint_interval {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (color : SixPointColor) : barC ≤ dist (configuration color SixPointLabel.left) (configuration color SixPointLabel.right) ∧ dist (configuration color SixPointLabel.left) (configuration color SixPointLabel.right) ≤ 2

Each sibling length in an endpoint-admissible configuration lies between barC and two.

theorem LeanPool.Besicovitch.rootedTriangleTotalRadius_mem_endpoint_interval {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (color : SixPointColor) : dist (configuration color SixPointLabel.left) (configuration color SixPointLabel.right) ≤ rootedTriangleTotalRadius configuration color ∧ rootedTriangleTotalRadius configuration color ≤ 2

The canonical triangle total lies between its sibling side and two.

theorem LeanPool.Besicovitch.exists_redSiblingTriangleFailure_of_split_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfail : ∀ (x : ℝ), dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) - 1 ≤ x → x ≤ 1 → redSiblingTriangleTarget configuration < siblingTriangleSplitDiameter (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) x (redSiblingBlueTriangleReach configuration SixPointLabel.left) (redSiblingBlueTriangleReach configuration SixPointLabel.right)) : ∃ (witness : SiblingTriangleWitness), redSiblingTriangleFailure configuration witness

Failure of every radius split in support 67 has a child-labelled incidence witness.

theorem LeanPool.Besicovitch.exists_blueSiblingTriangleFailure_of_split_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfail : ∀ (y : ℝ), dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) - 1 ≤ y → y ≤ 1 → blueSiblingTriangleTarget configuration < siblingTriangleSplitDiameter (dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) y (blueSiblingRedTriangleReach configuration SixPointLabel.left) (blueSiblingRedTriangleReach configuration SixPointLabel.right)) : ∃ (witness : SiblingTriangleWitness), blueSiblingTriangleFailure configuration witness

Failure of every radius split in support 76 has a child-labelled incidence witness.

noncomputable def LeanPool.Besicovitch.redSiblingTrianglePackingAtEndpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (x : ℝ) (hxLower : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) - 1 ≤ x) (hxUpper : x ≤ 1) : SixPointPacking configuration

The support 67 packing with its actual sibling length at the exact endpoint.

Equations

• LeanPool.Besicovitch.redSiblingTrianglePackingAtEndpoint configuration h x hxLower hxUpper = LeanPool.Besicovitch.redSiblingBlueTrianglePacking configuration ⋯ ⋯ hxLower hxUpper ⋯ ⋯

noncomputable def LeanPool.Besicovitch.blueSiblingTrianglePackingAtEndpoint (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) (y : ℝ) (hyLower : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) - 1 ≤ y) (hyUpper : y ≤ 1) : SixPointPacking configuration

The support 76 packing with its actual sibling length at the exact endpoint.

Equations

• LeanPool.Besicovitch.blueSiblingTrianglePackingAtEndpoint configuration h y hyLower hyUpper = LeanPool.Besicovitch.blueSiblingRedTrianglePacking configuration ⋯ ⋯ hyLower hyUpper ⋯ ⋯

def LeanPool.Besicovitch.RedSiblingTriangleFails (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) : Prop

Every feasible support 67 radius split has negative endpoint score.

Equations

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

def LeanPool.Besicovitch.BlueSiblingTriangleFails (configuration : SixPointConfiguration) (h : configuration.IsAdmissibleAt barS) : Prop

Every feasible support 76 radius split has negative endpoint score.

Equations

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

theorem LeanPool.Besicovitch.exists_redSiblingTriangleFailure_of_score_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfailure : RedSiblingTriangleFails configuration h) : ∃ (witness : SiblingTriangleWitness), redSiblingTriangleFailure configuration witness

Negative score for every support 67 split yields a child-labelled failure witness.

theorem LeanPool.Besicovitch.exists_blueSiblingTriangleFailure_of_score_failure {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hfailure : BlueSiblingTriangleFails configuration h) : ∃ (witness : SiblingTriangleWitness), blueSiblingTriangleFailure configuration witness

Negative score for every support 76 split yields a child-labelled failure witness.

theorem LeanPool.Besicovitch.q2_strict_of_matched_endpoint_zero {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hblue : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) : ((barC - 1) * matchedChildAverage configuration 0 + (barC + 1) * matchedChildAverage configuration 1 + 3 * barC ^ 2 - 3 * barC + 2) / 2 < dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left)

Coincident endpoint failures at B11 imply the first exact q2 inequality.

theorem LeanPool.Besicovitch.q2_strict_of_matched_endpoint_three {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 3)) (hblue : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 3)) : ((barC - 1) * matchedChildAverage configuration 1 + (barC + 1) * matchedChildAverage configuration 0 + 3 * barC ^ 2 - 3 * barC + 2) / 2 < dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right)

Coincident endpoint failures at B22 imply the child-swapped exact q2 inequality.

theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueEndpoint_three {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 3))

The selected-matching disjoint endpoint incidence is impossible.

theorem LeanPool.Besicovitch.not_redEndpoint_one_and_blueEndpoint_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) : ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 2))

The off-matching disjoint endpoint incidence is impossible.

structure LeanPool.Besicovitch.SiblingIncidenceExclusions (redFailure blueFailure : SiblingTriangleWitness → Prop) : Prop

The analytic exclusions required by the complete sibling-incidence ledger.

• endpointEndpoint (redCode blueCode : Fin 4) : endpointEndpointOrbit redCode blueCode ≠ EndpointEndpointOrbit.matchedCoincident → ¬(redFailure (SiblingTriangleWitness.endpoint redCode) ∧ blueFailure (SiblingTriangleWitness.endpoint blueCode))
• endpointBalanced (endpointCode balancedCode : Fin 4) : ¬(redFailure (SiblingTriangleWitness.endpoint endpointCode) ∧ blueFailure (SiblingTriangleWitness.balanced balancedCode))
• balancedEndpoint (balancedCode endpointCode : Fin 4) : ¬(redFailure (SiblingTriangleWitness.balanced balancedCode) ∧ blueFailure (SiblingTriangleWitness.endpoint endpointCode))
• balancedBalanced (redCode blueCode : Fin 4) : ¬(redFailure (SiblingTriangleWitness.balanced redCode) ∧ blueFailure (SiblingTriangleWitness.balanced blueCode))

theorem LeanPool.Besicovitch.exists_matched_endpoint_of_siblingIncidenceExclusions {redFailure blueFailure : SiblingTriangleWitness → Prop} (hexclusions : SiblingIncidenceExclusions redFailure blueFailure) (hred : ∃ (witness : SiblingTriangleWitness), redFailure witness) (hblue : ∃ (witness : SiblingTriangleWitness), blueFailure witness) : ∃ (code : Fin 4), (code = 0 ∨ code = 3) ∧ redFailure (SiblingTriangleWitness.endpoint code) ∧ blueFailure (SiblingTriangleWitness.endpoint code)

Complete incidence routing: the only simultaneous failures select one diagonal endpoint.

theorem LeanPool.Besicovitch.exists_matched_endpoint_of_siblingTriangle_score_failures {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : RedSiblingTriangleFails configuration h) (hblue : BlueSiblingTriangleFails configuration h) (hexclusions : SiblingIncidenceExclusions (redSiblingTriangleFailure configuration) (blueSiblingTriangleFailure configuration)) : ∃ (code : Fin 4), (code = 0 ∨ code = 3) ∧ redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

If supports 67 and 76 both fail, the incidence ledger selects one diagonal endpoint.

theorem LeanPool.Besicovitch.q2_strict_of_siblingTriangle_score_failures {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : RedSiblingTriangleFails configuration h) (hblue : BlueSiblingTriangleFails configuration h) (hexclusions : SiblingIncidenceExclusions (redSiblingTriangleFailure configuration) (blueSiblingTriangleFailure configuration)) : ((barC - 1) * matchedChildAverage configuration 0 + (barC + 1) * matchedChildAverage configuration 1 + 3 * barC ^ 2 - 3 * barC + 2) / 2 < dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.left) ∨ ((barC - 1) * matchedChildAverage configuration 1 + (barC + 1) * matchedChildAverage configuration 0 + 3 * barC ^ 2 - 3 * barC + 2) / 2 < dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.right)

Simultaneous 67 and 76 failures force the exact q2 inequality at one matched child.