Counting transfer definition Erdos9796Counting_MEC_Boundary

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.MEC.Boundary; source SHA-256 e7d16b0637be4dd967cade4cfb9db7d4ba52c8fdb229ece7b87498ff207e21a7 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_MEC_Basic


/-!
# MEC boundary structure — Sylvester (1857) dichotomy

For any nonempty noncollinear finite point set `A ⊆ ℝ²` we prove the
classical Sylvester dichotomy on the minimum enclosing circle (MEC) of
`A`:

* **Diameter case** — two points of `A` lie diametrically opposite on
  the MEC boundary, pinning the centre to their midpoint, OR
* **Circumscribed case** — at least three points of `A` lie on the MEC
  boundary.

The naive "≥3 boundary points" statement is **false** in general:
obtuse triangles realise the diameter case (the two acute-angle vertices
form an antipodal pair on the MEC, the obtuse vertex sits strictly
inside).  The disjunction below is the correct formulation, due to
Sylvester (1857).

The argument is variational.  Define
`B(A) := { p ∈ A | dist p M.center = M.radius }`, the set of points
realising the maximum distance from the MEC centre.  Then:

* `B.card = 0` is impossible: by continuity of `radF`, every point sits
  strictly inside, so we can shrink `M.radius` keeping the centre fixed
  — contradicting minimality.
* `B.card = 1` is impossible for noncollinear `A`: perturb the centre
  toward the lone boundary point.  Strict interior distance to other
  points is preserved by continuity, so we obtain a smaller enclosing
  radius — contradicting minimality.
* `B.card = 2` forces the diameter case: the two boundary points
  `p, q` pin the centre to their midpoint (otherwise we could shift
  along the perpendicular bisector toward `midpoint p q` to shrink the
  radius — same contradiction).
* `B.card ≥ 3` is the circumscribed case by definition.

The core perturbation uses an algebraic identity: along the segment
from `c := M.center` toward a target `q*` chosen so that
`⟨p - c, q* - c⟩ = ‖q* - c‖²` for every boundary point `p ∈ B`,
the squared distance `‖p - c'(t)‖²` equals
`M.radius² + (t² - 2t) ‖q* - c‖²`, which is strictly less than
`M.radius²` for `t ∈ (0, 2)` (and `q* ≠ c`).  For interior points the
distance change is bounded by `t · ‖q* - c‖`, so picking `t` small
enough keeps them inside as well.

## Main theorem

* `Problem97.MEC.sylvester_dichotomy` — the Sylvester (1857) dichotomy
  in disjunctive form, suitable for downstream consumers branching on
  the two cases.
-/

open scoped EuclideanGeometry
open Finset

namespace Problem97
namespace MEC

/- ### Boundary set of the MEC -/

/-- The points of a nonempty finite set lying on its minimum enclosing circle. -/
noncomputable def boundary (A : Finset ℝ²) (hA : A.Nonempty) : Finset ℝ² :=
  A.filter (fun p => dist p (mec A hA).center = (mec A hA).radius)





/- ### Auxiliary helpers -/







/-- A noncollinear finite set has a strictly positive minimum enclosing radius. -/
lemma mec_radius_pos
    {A : Finset ℝ²} (hA : A.Nonempty)
    (hncol : ¬ Collinear ℝ (A : Set ℝ²)) :
    0 < (mec A hA).radius := by
  classical
  set M := mec A hA with hM_def
  rcases lt_or_eq_of_le M.radius_nn with hpos | hzero
  · exact hpos
  -- radius = 0 ⇒ all points sit at the centre ⇒ A is collinear (singleton in set form).
  exfalso
  apply hncol
  have hzero' : M.radius = 0 := hzero.symm
  -- Every p ∈ A has p = M.center.
  have hall : ∀ p ∈ A, p = M.center := by
    intro p hp
    have h_le : dist p M.center ≤ 0 := by
      have := M.enclosing p hp; linarith
    have h_zero : dist p M.center = 0 := le_antisymm h_le dist_nonneg
    exact dist_eq_zero.mp h_zero
  -- (A : Set ℝ²) ⊆ {M.center}, so A is collinear.
  refine Collinear.subset ?_ (collinear_singleton ℝ M.center)
  intro p hp; simp only [Set.mem_singleton_iff]; exact hall p hp

/- ### Boundary card lower bound: ≥ 1 -/



/- ### Sentinel computation: distance along a "shrink-toward-target" line.

We isolate the algebraic identity that underlies both the card-1 and card-2
variational arguments.  If `p, c, q* : ℝ²` satisfy
`⟨p - c, q* - c⟩ = ‖q* - c‖²`, then
`‖p - (c + t • (q* - c))‖² = ‖p - c‖² - (2t - t²) ‖q* - c‖²`.

For `card = 1` with single boundary point `p₀`, take `q* := p₀`; then
`⟨p₀ - c, p₀ - c⟩ = ‖p₀ - c‖² = M.radius² = ‖q* - c‖²` (uses `q* - c = p₀ - c`).

For `card = 2` with boundary `{p, q}`, take `q* := midpoint p q = m`; then
on the perpendicular bisector, `⟨p - c, m - c⟩ = ‖m - c‖²`.
-/





/- ### Card 1 case — impossible for noncollinear A -/



/- ### Card 2 case — diameter case -/









/- ### Main theorem -/



end MEC
end Problem97