Metric/sign dichotomy

The normalized algebraic kernel for draft Section 5 and Lean-plan step 10. The proof uses only the four cross-color metric parameters, so its conclusion applies uniformly to all four cross-color pairs. The two boundary radicals are retained as exact kernel inequalities.

theorem LeanPool.Erdos132ConvexK3.first_hard_constant_pos : 0 < (3 * √3 - 5) / 4

First exact boundary constant in the short-sign regime.

theorem LeanPool.Erdos132ConvexK3.second_hard_constant_gt_nine_eighths : 9 / 8 < (4 * √3 + √39) / 8

Second exact boundary constant in the long-sign regime.

theorem LeanPool.Erdos132ConvexK3.metric_failure_numerator_lt_majorant {β γ : ℝ} (hγ : 0 < γ) (hfailure : 1 + γ < 2 * β) : 1 + 2 * γ ^ 2 - 3 * β ^ 2 < (1 - β) * (3 - 5 * β)

Failure of the desired metric inequality gives the strict numerator comparison used by all three beta ranges.

theorem LeanPool.Erdos132ConvexK3.amgm_two_r_add_p_gt_one {r p β : ℝ} (hr : 0 < r) (hβlo : 1 / 2 < β) (hβhi : β < 3 / 5) (hβsq : β ^ 2 = 1 - 4 * r * p) : 1 < 2 * r + p

AM-GM in polynomial form. In the first beta range the single identity β²=1-4rp already forces 2r+p>1.

theorem LeanPool.Erdos132ConvexK3.range_one_exact_radical_bound {β : ℝ} (hβlo : 1 / 2 < β) (hβhi : β < 3 / 5) : (3 - 5 * β) / (1 + β) < √3 / 2 - β

Exact rationalized inequality behind beta range 1/2<β<3/5.

theorem LeanPool.Erdos132ConvexK3.metric_dichotomy_range_one {r p β γ h k δ : ℝ} (hr : 0 < r) (hrhi : r ≤ 1 / 2) (hp : 0 < p) (hβlo : 1 / 2 < β) (hβhi : β < 3 / 5) (hβsq : β ^ 2 = 1 - 4 * r * p) (hγ : 0 < γ) (hfailure : 1 + γ < 2 * β) (hh : 0 < h) (hhsq : h ^ 2 = 1 - r ^ 2) (hksq : k ^ 2 = 1 - (r + p) ^ 2) (hδ : 0 < δ) (hδdef : δ = h - k) : (1 + 2 * γ ^ 2 - 3 * β ^ 2) / (4 * δ) < h - β

Beta range 1 (1/2<β<3/5). The AM-GM consequence makes δ>p/2; the exact first radical constant then closes the sign inequality.

theorem LeanPool.Erdos132ConvexK3.metric_dichotomy_range_two {r p β γ h δ : ℝ} (hr : 0 < r) (hp : 0 < p) (hβsq : β ^ 2 = 1 - 4 * r * p) (hγ : 0 < γ) (hfailure : 1 + γ < 2 * β) (hβlo : 3 / 5 ≤ β) (hβh : β ≤ h) (hδ : 0 < δ) : (1 + 2 * γ ^ 2 - 3 * β ^ 2) / (4 * δ) < h - β

Beta range 2 (3/5≤β≤h). Here the majorant is nonpositive, so its strict numerator bound immediately has the required sign.

theorem LeanPool.Erdos132ConvexK3.metric_dichotomy_range_three {r p β γ h k δ : ℝ} (hr : 0 < r) (hrhi : r ≤ 1 / 2) (hp : 0 < p) (hβsq : β ^ 2 = 1 - 4 * r * p) (hγ : 0 < γ) (hfailure : 1 + γ < 2 * β) (hh : 0 < h) (hhsq : h ^ 2 = 1 - r ^ 2) (hk : 0 < k) (hksq : k ^ 2 = 1 - (r + p) ^ 2) (hδ : 0 < δ) (hδdef : δ = h - k) (hβh : h < β) : (1 + 2 * γ ^ 2 - 3 * β ^ 2) / (4 * δ) < h - β

Beta range 3 (h<β). The identity β²-h²=r(r-4p) gives p<r/4. The exact second radical constant proves δ<p; the remaining ratio estimate then reverses the negative majorant with room to spare.

theorem LeanPool.Erdos132ConvexK3.metric_sign_dichotomy {r p β γ h k δ : ℝ} (hr : 0 < r) (hrhi : r ≤ 1 / 2) (hp : 0 < p) (hβsq : β ^ 2 = 1 - 4 * r * p) (hγ : 0 < γ) (hh : 0 < h) (hhsq : h ^ 2 = 1 - r ^ 2) (hk : 0 < k) (hksq : k ^ 2 = 1 - (r + p) ^ 2) (hδ : 0 < δ) (hδdef : δ = h - k) : 2 * β ≤ 1 + γ ∨ (1 + 2 * γ ^ 2 - 3 * β ^ 2) / (4 * δ) < h - β

Metric/sign dichotomy for one arbitrary full two-rung normalization. Equality belongs to the length branch; only strict failure enters the three beta regimes. Since no earlier cross-color hypothesis occurs, this one theorem applies unchanged to all four AA, AB, BA, and BB branches from draft (4.2).

theorem LeanPool.Erdos132ConvexK3.metric_equality_routes_long {d₁ d₂ d₃ : ℝ} (heq : d₁ + d₃ = 2 * d₂) : 2 * d₂ ≤ d₁ + d₃

The equality boundary belongs to the non-strict long regime.

theorem LeanPool.Erdos132ConvexK3.metric_equality_forces_long_second_center {d₁ d₂ d₃ q : ℝ} (heq : d₁ + d₃ = 2 * d₂) (hED : d₁ + d₃ < q + d₂) : d₂ < q

The exact equality boundary is assigned to the long/counting regime: strict edge-diagonal separation then forces the second center beyond d₂.