Counting transfer definition Erdos9796Counting_Moser_Triangle

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.Moser.Triangle; source SHA-256 7c78d8a21f64e82cf408a3c1b2e026298d6173838f6b91484d8386f31cf2a392 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_MEC_Basic


/-!
# Moser triangle extraction from the Sylvester dichotomy

Given a nonempty noncollinear `A : Finset ℝ²`, the Sylvester (1857)
dichotomy on the MEC (`Problem97.MEC.sylvester_dichotomy`) provides:

* **Diameter case** — two points `p, q ∈ A` on the MEC boundary pin the
  centre to their midpoint with `MEC.radius = dist p q / 2`; OR
* **Circumscribed case** — at least three points of `A` lie on the MEC
  boundary.

This file packages either case into a uniform `MoserTriangle` record
carrying *three* MEC-boundary vertices of `A`, with a `case_split` field
recording which of the two dichotomy branches produced them.

In the circumscribed case the three vertices are pairwise distinct (a
genuine inscribed triangle whose circumcircle is the MEC).  In the
diameter case the third vertex is taken to coincide with the first
(`v3 = v1`), and the `case_split` records the antipodal-pair witnesses
together with the centre/radius identifications.

This is the **structural** layer: downstream consumers
(`p97-mec-cap-partition`, `p97-u1-*`) need only the boundary-membership
data; the "obtuse-or-right" geometric content of the circumscribed case
is not formalised here (it is implicit in the variational characterisation
and not required by any open obligation as a separate lemma).

## Main declarations

* `Problem97.MEC.MoserTriangle` — three MEC-boundary points of `A` plus a
  dichotomy `case_split` witness.
* `Problem97.MEC.moser_triangle_exists` — extraction theorem: every
  nonempty noncollinear `A` yields a `MoserTriangle`.
-/

open scoped EuclideanGeometry
open Finset

namespace Problem97
namespace MEC

/-- The Moser triangle extracted from a nonempty noncollinear finite
point set `A ⊆ ℝ²`.  Three (not necessarily distinct) points of `A` lie
on the MEC boundary, with a `case_split` recording which branch of the
Sylvester (1857) dichotomy produced them:

* **Circumscribed case** (left disjunct of `case_split`): `v1, v2, v3`
  are pairwise distinct points of `A` on the MEC boundary.
* **Diameter case** (right disjunct): `v1, v2` are antipodal on the MEC
  with `v3 = v1`; the centre is `midpoint ℝ v1 v2` and the radius is
  `dist v1 v2 / 2`.

The "obtuse-or-right" geometric content of the circumscribed case is
implicit in the MEC variational characterisation and is not exposed at
this structural layer (downstream U1 consumers only need the
boundary-membership data). -/
structure MoserTriangle (A : Finset ℝ²) (hA : A.Nonempty)
    (_hncol : ¬ Collinear ℝ (A : Set ℝ²)) where
  /-- First vertex. -/
  v1 : ℝ²
  /-- Second vertex. -/
  v2 : ℝ²
  /-- Third vertex (= `v1` in the diameter case). -/
  v3 : ℝ²
  /-- `v1 ∈ A`. -/
  v1_mem : v1 ∈ A
  /-- `v2 ∈ A`. -/
  v2_mem : v2 ∈ A
  /-- `v3 ∈ A`. -/
  v3_mem : v3 ∈ A
  /-- `v1` lies on the MEC boundary. -/
  v1_boundary : dist v1 (mec A hA).center = (mec A hA).radius
  /-- `v2` lies on the MEC boundary. -/
  v2_boundary : dist v2 (mec A hA).center = (mec A hA).radius
  /-- `v3` lies on the MEC boundary. -/
  v3_boundary : dist v3 (mec A hA).center = (mec A hA).radius
  /-- Dichotomy witness:
  * left disjunct = circumscribed case (pairwise distinct);
  * right disjunct = diameter case (`v3 = v1`, antipodal `v1, v2`). -/
  case_split :
    (v1 ≠ v2 ∧ v2 ≠ v3 ∧ v1 ≠ v3)
      ∨ (v1 ≠ v2 ∧ v3 = v1
          ∧ (mec A hA).center = midpoint ℝ v1 v2
          ∧ (mec A hA).radius = dist v1 v2 / 2)



end MEC
end Problem97