Documentation

LeanPool.Erdos132ConvexK3.ResidualBounds

Residual one-sided and four-edge bounds #

Arithmetic and finite-package kernel for draft Section 6.1--6.3. The geometric circle/half-plane arguments supply the package-cardinality hypotheses; this file proves the exact degree consequences, the surviving penultimate anti-saturation step, and the two metric regimes of the conditional four-edge cage.

theorem LeanPool.Erdos132ConvexK3.same_half_plane_fixed_radii_card_le_one {a b : Point ℝ} (hab : a ≠ b) {S : Finset (Point ℝ)} {radiusA radiusB : ℝ} (hS : ∀ p ∈ S, sqDist a p = radiusA ∧ sqDist b p = radiusB ∧ InLeftOpenHalfPlane a b p) :

A fixed pair of radii contributes at most one point in one open half-plane of the line of distinct centers.

theorem LeanPool.Erdos132ConvexK3.two_circle_families_card_le_two {S A B : Finset (Point ℝ)} (hcover : S ⊆ A ∪ B) (hA : A.card ≤ 1) (hB : B.card ≤ 1) :

A branch covered by two fixed-radius circle families has at most two points once each family has the half-plane uniqueness bound.

theorem LeanPool.Erdos132ConvexK3.three_circle_families_card_le_three {S A B C : Finset (Point ℝ)} (hcover : S ⊆ A ∪ B ∪ C) (hA : A.card ≤ 1) (hB : B.card ≤ 1) (hC : C.card ≤ 1) :

A branch covered by three fixed-radius circle families has at most three points.

theorem LeanPool.Erdos132ConvexK3.one_sided_shared_tip_d2_degree_bound {degree leftArc rightArc : ℕ} (hdegree : degree ≤ leftArc + rightArc + 1) (hleft : leftArc ≤ 2) (hright : rightArc ≤ 2) :

degree ≤ 5

Draft (6.3): two circle slots on either boundary arc, plus the shared tip, give degree at most five when the tip is a d₂ partner.

theorem LeanPool.Erdos132ConvexK3.one_sided_shared_tip_d1_degree_bound {degree leftArc rightArc : ℕ} (hdegree : degree ≤ leftArc + rightArc + 1) (hleft : leftArc ≤ 3) (hright : rightArc ≤ 3) :

degree ≤ 7

Draft (6.4): three circle slots on either boundary arc, plus the shared tip, give degree at most seven when the tip is a diameter partner.

theorem LeanPool.Erdos132ConvexK3.one_sided_shared_tip_low_degree_bound {degree : ℕ} (hdegree : degree ≤ 1) :

degree ≤ 1

Unique farthest immediately gives the low-tip branch of Section 6.1.

theorem LeanPool.Erdos132ConvexK3.one_penultimate_anti_saturation {d₁ d₂ Vs Vp : ℝ} (hVpClasses : Vp ≤ d₁ ∧ (Vp < d₁ → Vp ≤ d₂)) (hUniqueFarthest : Vp < Vs) (hED : Vs + d₂ < Vp + d₁) :

Vs ≠ d₁

Attempt 12, Section 1. ED across the surviving d₂ rung contradicts the top-two gap and strict unique-farthest inequality if Vs=d₁.

theorem LeanPool.Erdos132ConvexK3.one_penultimate_shared_tip_degree_le_five {degree : ℕ} {Vs d₁ d₂ d₃ : ℝ} (hSplit : Vs = d₁ ∨ Vs = d₂ ∨ Vs ≤ d₃) (hNotD₁ : Vs ≠ d₁) (hD₂ : Vs = d₂ → degree ≤ 5) (hLow : Vs ≤ d₃ → degree ≤ 1) :

degree ≤ 5

Combining the anti-saturation exclusion with the one-sided d₂ and low-tip bounds gives the four saturation words degree at most five.

inductive LeanPool.Erdos132ConvexK3.CageDistanceBand :

The four possible distance bands for either central cage endpoint.

Instances For

@[instance_reducible]

instance LeanPool.Erdos132ConvexK3.instDecidableEqCageDistanceBand :

DecidableEq CageDistanceBand

Equations

LeanPool.Erdos132ConvexK3.instDecidableEqCageDistanceBand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanPool.Erdos132ConvexK3.instFintypeCageDistanceBand :

Fintype CageDistanceBand

Equations

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

def LeanPool.Erdos132ConvexK3.fourEdgeGeneralPackage :

CageDistanceBand → ℕ

General row of draft package table (6.5).

Equations

Instances For

def LeanPool.Erdos132ConvexK3.fourEdgeLongPackage :

CageDistanceBand → ℕ

Long-metric row of draft package table (6.5).

Equations

Instances For

Kernel rendering of both rows of the exact package table (6.5).

theorem LeanPool.Erdos132ConvexK3.four_edge_cage_long_high_degree_forces_d1d1 {degree : ℕ} {left right : CageDistanceBand} (hdegree : 7 ≤ degree) (hpackage : degree ≤ fourEdgeLongPackage left + fourEdgeLongPackage right) :

left = CageDistanceBand.d1 ∧ right = CageDistanceBand.d1

Draft (6.6): in the long metric regime, degree at least seven forces both central endpoint distances into the diameter band.

theorem LeanPool.Erdos132ConvexK3.four_edge_cage_short_high_degree_forces_three_states {degree : ℕ} {left right : CageDistanceBand} (hdegree : 7 ≤ degree) (hpackage : degree ≤ fourEdgeGeneralPackage left + fourEdgeGeneralPackage right) :

left = CageDistanceBand.d1 ∧ right = CageDistanceBand.d2 ∨ left = CageDistanceBand.d2 ∧ right = CageDistanceBand.d1 ∨ left = CageDistanceBand.d1 ∧ right = CageDistanceBand.d1

Draft (6.7): in the short metric regime, degree at least seven forces exactly one of the three displayed central states.

theorem LeanPool.Erdos132ConvexK3.four_edge_cage_long_min_degree_le_six {degreeP degreeQ : ℕ} {leftP rightP leftQ rightQ : CageDistanceBand} (hpackageP : degreeP ≤ fourEdgeLongPackage leftP + fourEdgeLongPackage rightP) (hpackageQ : degreeQ ≤ fourEdgeLongPackage leftQ + fourEdgeLongPackage rightQ) (hUniqueD1D1 : ¬(leftP = CageDistanceBand.d1 ∧ rightP = CageDistanceBand.d1 ∧ leftQ = CageDistanceBand.d1 ∧ rightQ = CageDistanceBand.d1)) :

min degreeP degreeQ ≤ 6

Long-regime half-plane uniqueness turns (6.6) into (6.8).

theorem LeanPool.Erdos132ConvexK3.four_edge_cage_short_min_degree_le_six {degreeP degreeQ : ℕ} {leftP rightP leftQ rightQ : CageDistanceBand} (hpackageP : degreeP ≤ fourEdgeGeneralPackage leftP + fourEdgeGeneralPackage rightP) (hpackageQ : degreeQ ≤ fourEdgeGeneralPackage leftQ + fourEdgeGeneralPackage rightQ) (hP12 : ¬(leftP = CageDistanceBand.d1 ∧ rightP = CageDistanceBand.d2)) (hP21 : ¬(leftP = CageDistanceBand.d2 ∧ rightP = CageDistanceBand.d1)) (hQ12 : ¬(leftQ = CageDistanceBand.d1 ∧ rightQ = CageDistanceBand.d2)) (hQ21 : ¬(leftQ = CageDistanceBand.d2 ∧ rightQ = CageDistanceBand.d1)) (hUniqueD1D1 : ¬(leftP = CageDistanceBand.d1 ∧ rightP = CageDistanceBand.d1 ∧ leftQ = CageDistanceBand.d1 ∧ rightQ = CageDistanceBand.d1)) :

min degreeP degreeQ ≤ 6

Short-regime occupied-circle exclusions and uniqueness turn (6.7) into the conditional cage conclusion (6.8).