Documentation

LeanPool.Erdos132ConvexK3.Penultimate

Forced penultimate coordinates #

Algebraic kernel for draft Section 5 and Lean-plan step 9. The two circle systems force the penultimate points to be mirror images; no symmetry is assumed. The previously implicit P5-4 height constraint is named and used explicitly in every distance-subtraction identity.

source
theorem LeanPool.Erdos132ConvexK3.forced_penultimate_mirror {c A B W R K_w K_r : ℝ} (hc : 0 < c) (hwA : W ^ 2 + K_w ^ 2 = A) (hwB : (W - 2 * c) ^ 2 + K_w ^ 2 = B) (hrB : R ^ 2 + K_r ^ 2 = B) (hrA : (R - 2 * c) ^ 2 + K_r ^ 2 = A) (hKw : 0 < K_w) (hKr : 0 < K_r) :
W + R = 2 * c ∧ K_w = K_r ∧ A - B = 4 * c * (W - c)

The two penultimate circle systems force W+R=2c, equal positive ordinates, and the horizontal class difference.

source
theorem LeanPool.Erdos132ConvexK3.forced_penultimate_coordinates {c A B W R K_w K_r : ℝ} (hc : 0 < c) (hBA : B < A) (hwA : W ^ 2 + K_w ^ 2 = A) (hwB : (W - 2 * c) ^ 2 + K_w ^ 2 = B) (hrB : R ^ 2 + K_r ^ 2 = B) (hrA : (R - 2 * c) ^ 2 + K_r ^ 2 = A) (hKw : 0 < K_w) (hKr : 0 < K_r) :
∃ (d : ℝ) (K : ℝ), 0 < d ∧ W = c + d ∧ R = c - d ∧ K_w = K ∧ K_r = K ∧ A - B = 4 * c * d

Canonical mirror-coordinate form with d>0 when A>B.

source
theorem LeanPool.Erdos132ConvexK3.forced_penultimate_height_constraint {c d H K Δ : ℝ} (hradius : (c + d) ^ 2 + K ^ 2 = c ^ 2 + H ^ 2) (hΔ : Δ = H - K) :
2 * c * d + d ^ 2 = Δ * (H + K)

P5-4, displayed. Equality of the two diameter radii forces 2cd+d² = Δ(H+K) when Δ=H-K.

source
theorem LeanPool.Erdos132ConvexK3.forced_penultimate_height_constraint_reparam {c d H Δ : ℝ} (hradius : (c + d) ^ 2 + (H - Δ) ^ 2 = c ^ 2 + H ^ 2) :
2 * c * d + d ^ 2 = Δ * (H + (H - Δ))

The exact P5-4 constraint in the draft parameterization K=H-Δ.

source
theorem LeanPool.Erdos132ConvexK3.left_penultimate_distance_difference {c d H Δ X Y : ℝ} (hconstraint : 2 * c * d + d ^ 2 = Δ * (H + (H - Δ))) :
sqDist (X, Y) (c + d, H - Δ) - sqDist (X, Y) (c, H) = -2 * d * X + 2 * Δ * Y

Left penultimate subtraction identity, with P5-4 explicit.

source
theorem LeanPool.Erdos132ConvexK3.right_penultimate_distance_difference {c d H Δ X Y : ℝ} (hconstraint : 2 * c * d + d ^ 2 = Δ * (H + (H - Δ))) :
sqDist (X, Y) (c - d, H - Δ) - sqDist (X, Y) (c, H) = -2 * d * (2 * c - X) + 2 * Δ * Y

Right penultimate subtraction identity, with P5-4 explicit.

source
noncomputable def LeanPool.Erdos132ConvexK3.penultimateReflectionOrdinate (c d H Δ : ℝ) :
ℝ

Ordinate of the nontrivial reflection of (2c,0) across the line through (c,H) and (c+d,H-Δ).

Equations
Instances For
    source
    theorem LeanPool.Erdos132ConvexK3.penultimate_reflection_ordinate_pos {c d H Δ : ℝ} (hd : 0 < d) (hconvex : c * Δ < H * d) :
    0 < penultimateReflectionOrdinate c d H Δ

    The convexity sign Hd>cΔ puts the reflected intersection strictly above the lower chord.

    source
    theorem LeanPool.Erdos132ConvexK3.penultimate_nontrivial_intersection_ordinate {c d H Δ X Y : ℝ} (hd : 0 < d) (hcircleS : sqDist (X, Y) (c, H) = sqDist (2 * c, 0) (c, H)) (hcircleW : sqDist (X, Y) (c + d, H - Δ) = sqDist (2 * c, 0) (c + d, H - Δ)) (hneq : (X, Y) ≠ (2 * c, 0)) :
    Y = penultimateReflectionOrdinate c d H Δ

    The two circle equations have the known intersection (2c,0); every other intersection has exactly the reflected ordinate from attempt 9.

    source
    theorem LeanPool.Erdos132ConvexK3.penultimate_nontrivial_intersection_above {c d H Δ X Y : ℝ} (hd : 0 < d) (hconvex : c * Δ < H * d) (hcircleS : sqDist (X, Y) (c, H) = sqDist (2 * c, 0) (c, H)) (hcircleW : sqDist (X, Y) (c + d, H - Δ) = sqDist (2 * c, 0) (c + d, H - Δ)) (hneq : (X, Y) ≠ (2 * c, 0)) :
    0 < Y

    With the polygon-order sign Hd>cΔ, the nontrivial circle intersection is above the lower chord; the known intersection is (2c,0).

    source
    theorem LeanPool.Erdos132ConvexK3.top_three_value_split {F A B C : ℝ} (hbound : F ≤ A ∧ (F < A → F ≤ B) ∧ (F < B → F ≤ C)) :
    F = A ∨ F = B ∨ F ≤ C

    A local top-three bound has exactly the shared-tip split used in the proof: top class A, second class B, or at most C.

    source
    theorem LeanPool.Erdos132ConvexK3.case_three_existential_partition_bound {degreeP degreeQ pToS sToX qToS sToQ : ℕ} (hPpartition : degreeP ≤ pToS + sToX + 2) (hpToS : pToS ≤ 2) (hsToX : sToX ≤ 2) (hQpartition : degreeQ ≤ qToS + sToQ + 1) (hqToS : qToS ≤ 2) (hsToQ : sToQ ≤ 2) :
    degreeP ≤ 6 ∧ degreeQ ≤ 5 ∧ ∃ (degree : ℕ), (degree = degreeP ∨ degree = degreeQ) ∧ degree ≤ 6

    P5-2, existential form. The left-adjacent lower vertex uses the partition arc(P,s) + arc(s,x) + {s,x}; its mirror uses arc(Q,s) + arc(s,Q) + {s}. The hypotheses expose those two different partitions instead of quantifying one universal partition over both points.