Terminal d2-cage

Kernelization of draft (6.9)--(6.14) and attempt 12, Section 2. Distances are unsquared here because the edge--diagonal inequalities are additive. The finite branch counts are kept explicit, so the equality and q=d₃ boundaries cannot disappear inside prose.

theorem LeanPool.Erdos132ConvexK3.terminal_central_distance_order {d₂ q Vw Vs : ℝ} (hq : q ≤ d₂) (hleftED : Vw + d₂ < q + Vs) : Vw < Vs

The first inequality in (6.10), together with q≤d₂, gives Vw<Vs.

theorem LeanPool.Erdos132ConvexK3.terminal_central_distances {d₁ d₂ q Vw Vs : ℝ} (hq : q ≤ d₂) (hVsClasses : Vs ≤ d₁ ∧ (Vs < d₁ → Vs ≤ d₂)) (hVwClasses : Vw ≤ d₁ ∧ (Vw < d₁ → Vw ≤ d₂)) (hleftED : Vw + d₂ < q + Vs) (hrightED : Vs + d₂ < Vw + d₁) : Vs ≤ d₂ ∧ Vw < Vs

Draft (6.11): the two central ED inequalities and the top-two gap force Vs≤d₂ as well as Vw<Vs.

theorem LeanPool.Erdos132ConvexK3.terminal_left_d2_partner_forces_outer_d1 {d₁ d₂ xR : ℝ} (hxRClasses : xR ≤ d₁ ∧ (xR < d₁ → xR ≤ d₂)) (hED : d₂ + d₂ < xR + d₂) : xR = d₁

Left branch (6.12), Vs=d₂: a d₂ partner must lie on the d₁ circle about the opposite center.

theorem LeanPool.Erdos132ConvexK3.terminal_left_d3_partner_outer_band {d₁ d₂ d₃ xR : ℝ} (hxRClasses : xR ≤ d₁ ∧ (xR < d₁ → xR ≤ d₂) ∧ (xR < d₂ → xR ≤ d₃)) (hED : d₂ + d₃ < xR + d₂) : xR = d₁ ∨ xR = d₂

Left branch (6.12), Vs=d₂: a d₃ partner uses one of exactly the d₁ and d₂ second-center radii.

theorem LeanPool.Erdos132ConvexK3.terminal_right_d3_partner_outer_band {d₁ d₂ d₃ tR : ℝ} (hd₂d₁ : d₂ < d₁) (htRClasses : tR ≤ d₁ ∧ (tR < d₁ → tR ≤ d₂) ∧ (tR < d₂ → tR ≤ d₃)) (hED : d₁ + d₃ < tR + d₂) : tR = d₁ ∨ tR = d₂

Right branch (6.13), Vs=d₂: a d₃ partner has second-center radius d₁ or d₂ before the metric split.

theorem LeanPool.Erdos132ConvexK3.terminal_long_right_d3_partner_forces_outer_d1 {d₁ d₂ d₃ tR : ℝ} (htRClasses : tR ≤ d₁ ∧ (tR < d₁ → tR ≤ d₂)) (hlong : 2 * d₂ ≤ d₁ + d₃) (hED : d₁ + d₃ < tR + d₂) : tR = d₁

Long regime, including equality: (6.13) collapses the two right d₃ circle slots to the single d₁ radius.

theorem LeanPool.Erdos132ConvexK3.terminal_short_q_eq_d3_impossible {d₁ d₂ d₃ q : ℝ} (hshort : d₁ + d₃ < 2 * d₂) (hq : q = d₃) (hterminalED : 2 * d₂ < q + d₁) : False

The literal q=d₃ boundary is impossible in the short regime.

theorem LeanPool.Erdos132ConvexK3.terminal_short_regime_forces_q_eq_d2 {d₁ d₂ d₃ q : ℝ} (hq : q ≤ d₂) (hqClass : q = d₂ ∨ q ≤ d₃) (hshort : d₁ + d₃ < 2 * d₂) (hterminalED : 2 * d₂ < q + d₁) : q = d₂

Draft (2.15)/(6.14): in the short regime, terminal ED and the top-three gap force q=d₂; the entire q≤d₃ branch, including equality, is excluded.

theorem LeanPool.Erdos132ConvexK3.terminal_short_left_d3_partner_forces_outer_d1 {d₁ d₂ d₃ xR : ℝ} (hxRClasses : xR ≤ d₁ ∧ (xR < d₁ → xR ≤ d₂)) (hED : d₂ + d₃ < xR + d₃) : xR = d₁

Once q=d₂, ED with w collapses the two left d₃ circle slots to the single d₁ second-center radius.

theorem LeanPool.Erdos132ConvexK3.terminal_crude_seven_slot_bound {degree leftArc rightArc wSlot : ℕ} (hdegree : degree ≤ leftArc + rightArc + wSlot + 1) (hleft : leftArc ≤ 3) (hright : rightArc ≤ 2) (hw : wSlot ≤ 1) : degree ≤ 7

Crude package (6.14): 3+2+1+1=7.

theorem LeanPool.Erdos132ConvexK3.terminal_low_tip_degree_le_three {degree leftArc rightArc wSlot : ℕ} (hdegree : degree ≤ leftArc + rightArc + wSlot + 1) (hleft : leftArc ≤ 2) (hright : rightArc = 0) (hw : wSlot = 0) : degree ≤ 3

Low-tip branch: two left slots, no right branch, no w slot, and s.

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

Regime 1 package: the right branch loses one slot, so the crude seven becomes 3+1+1+1=6.

theorem LeanPool.Erdos132ConvexK3.terminal_short_no_w_degree_le_six {degree leftArc rightArc wSlot : ℕ} (hdegree : degree ≤ leftArc + rightArc + wSlot + 1) (hleft : leftArc ≤ 3) (hright : rightArc ≤ 2) (hw : wSlot = 0) : degree ≤ 6

Regime 2, w not a partner: 3+2+0+1=6.

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

Regime 2, Vw=d₃: the left package loses one slot, giving 2+2+1+1=6.

theorem LeanPool.Erdos132ConvexK3.terminal_d2_cage_metric_split_degree_le_six {degree leftArc rightArc wSlot : ℕ} {d₁ d₂ d₃ : ℝ} (hdegree : degree ≤ leftArc + rightArc + wSlot + 1) (hleft : leftArc ≤ 3) (hright : rightArc ≤ 2) (hw : wSlot ≤ 1) (hlongCollapse : 2 * d₂ ≤ d₁ + d₃ → rightArc ≤ 1) (hshortCollapse : d₁ + d₃ < 2 * d₂ → wSlot = 0 ∨ leftArc ≤ 2) : degree ≤ 6

Complete metric split of the terminal d₂ cage. Equality is included in the first branch by ≤; strict failure invokes the q=d₂/left-collapse package.