Counting transfer definition Erdos9796Counting_CircumscribedMECPacket

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.CircumscribedMECPacket; source SHA-256 02ff1f784964432d89d8cbd6166a30cc8417a7b0d3b72247d0f8c6a610ba54d4 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Cap_PartitionFromMEC
import Definitions.Def_Erdos9796Counting_Cap_Structure
import Definitions.Def_Erdos9796Counting_MEC_Basic
import Definitions.Def_Erdos9796Counting_MEC_Boundary
import Definitions.Def_Erdos9796Counting_Moser_Triangle
import Definitions.Def_Erdos9796Counting_Moser_TriangleNonObtuse


/-!
# Circumscribed-MEC packet for the Dumitrescu lane

This file packages the geometric data needed by the **Dumitrescu Lc1
obligation** (cap-arc Thales angle inequality) and downstream
witness-ranking arguments. It is the Dumitrescu-lane analogue of the
`SurplusCapPacket` used by U1-U7.

## Why a separate packet

The corrective math-professor analysis (2026-05-22) established that
Dumitrescu's argument does **not** require cap A-points to lie on the
MEC boundary; the actual cap condition is angle-based — every cap point
sees the cap's opposing Moser-vertex chord at angle ≥ π/2. This Thales
condition is derivable from three ingredients:

1. The chord-side predicate `OnArcOpposite` (already carried by
   `CapTriple.arc_membership`).
2. Disk-containment `dist a center ≤ radius` for every `a ∈ A`. This is
   **free** from the MEC's `enclosing` clause (every point of `A` is in
   the closed disk around the MEC center). No `ConvexIndep` hypothesis
   is needed.
3. The Thales bridge `inner_nonpos_of_cap_region_thales` from
   `CapArcInteriorPoints.lean` (commit 65e73f4): chord-side + disk-in
   ⇒ angle ≥ π/2 (in inner-product form).

The packet bundles all the geometric data so downstream Lc1 / Lc3
lemmas can consume it directly without re-deriving the disk-containment
or non-obtuse witnesses.

## Recommended pattern

`CircumscribedMECPacket` is a structural data carrier — it does **not**
extend `CapTriple` or `MoserTriangle`, and it does **not** require a
surplus-cap designation. Dumitrescu Lc1, Lc3, and the downstream
witness-ranking constructor take a `(CapTriple A M, CircumscribedMECPacket A M)`
pair. U1-U7 continue to use `SurplusCapPacket` (which already carries
the same geometric data inline via `triangleNonObtuse`).

## Main declarations

* `Problem97.CircumscribedMECPacket A M` — the data carrier (center,
  radius, three Moser-on-boundary witnesses, three non-obtuse inner
  products, disk-containment of `A`).
* `Problem97.CircumscribedMECPacket.ofNonObtuse` — discharge constructor
  from a `MEC.NonObtuseCircumscribedMoserTriangle` and circumscribed
  case-split witness. The disk-containment field comes for free from
  `MinEnclosingCircle.enclosing`.
-/

open scoped EuclideanGeometry InnerProductSpace
open Finset

namespace Problem97

/- ### `CircumscribedMECPacket`: geometric data carrier -/

/-- `CircumscribedMECPacket A M` carries the geometric data needed by
the Dumitrescu Lc1 obligation and downstream cap-arc Thales arguments:

* the MEC `center` and (positive) `radius`;
* witnesses that each Moser vertex of `M` lies on the MEC boundary
  (`‖M.vᵢ - center‖ = radius`);
* the three non-obtuse inner-product inequalities at each Moser vertex
  (`⟪vⱼ - vᵢ, vₖ - vᵢ⟫ ≥ 0`);
* disk-containment of `A` in the closed disk
  (`‖a - center‖ ≤ radius` for every `a ∈ A`).

This is the packet consumed by the cap-arc Thales lemma family and the
Dumitrescu witness-ranking constructor. It mirrors the data inline in
`SurplusCapPacket` but without the surplus-cap designation, making it
reusable for Lc1 / Lc3 in the Dumitrescu lane.

The packet is **structurally independent** of `CapTriple`: a `CapTriple A M`
plus a `CircumscribedMECPacket A M` over the same Moser triangle `M` is
the standard input to Dumitrescu Lc1. -/
structure CircumscribedMECPacket (A : Finset ℝ²) (M : MoserTriangle A) where
  /-- MEC center. -/
  center : ℝ²
  /-- MEC radius. -/
  radius : ℝ
  /-- The radius is strictly positive. -/
  radius_pos : 0 < radius
  /-- Moser vertex 1 lies on the MEC boundary. -/
  moser_on_boundary_1 : ‖M.v1 - center‖ = radius
  /-- Moser vertex 2 lies on the MEC boundary. -/
  moser_on_boundary_2 : ‖M.v2 - center‖ = radius
  /-- Moser vertex 3 lies on the MEC boundary. -/
  moser_on_boundary_3 : ‖M.v3 - center‖ = radius
  /-- Non-obtuse at `v1`: angle at `v1` subtending the chord `v2 v3` is
  at most `π/2`. -/
  inner_at_v1 : 0 ≤ ⟪M.v2 - M.v1, M.v3 - M.v1⟫_ℝ
  /-- Non-obtuse at `v2`: angle at `v2` subtending the chord `v3 v1` is
  at most `π/2`. -/
  inner_at_v2 : 0 ≤ ⟪M.v3 - M.v2, M.v1 - M.v2⟫_ℝ
  /-- Non-obtuse at `v3`: angle at `v3` subtending the chord `v1 v2` is
  at most `π/2`. -/
  inner_at_v3 : 0 ≤ ⟪M.v1 - M.v3, M.v2 - M.v3⟫_ℝ
  /-- Every point of `A` lies in the closed disk centered at `center`
  with radius `radius`. -/
  disk_contains_A : ∀ a ∈ A, ‖a - center‖ ≤ radius





namespace MoserTriangle

variable {A : Finset ℝ²}





end MoserTriangle

namespace CircumscribedMECPacket

variable {A : Finset ℝ²}





/-- **Discharge constructor.** Given a non-obtuse circumscribed Moser
triangle and a circumscribed case-split witness, the structural
projection's `CircumscribedMECPacket` is fully determined by the MEC
data: center, radius, boundary witnesses, non-obtuse witnesses, and
disk-containment all flow from the `MEC.NonObtuseCircumscribedMoserTriangle`
data plus `MinEnclosingCircle.enclosing`.

The `disk_contains_A` field is free from the MEC's defining property
(`enclosing : ∀ p ∈ A, dist p center ≤ radius`). No `ConvexIndep`
hypothesis is needed. -/
noncomputable def ofNonObtuse
    {hA : A.Nonempty} {hncol : ¬ Collinear ℝ (A : Set ℝ²)}
    (MT : MEC.NonObtuseCircumscribedMoserTriangle A hA hncol)
    (hCirc : ∃ h12 h23 h13,
      MT.toMoserTriangle.case_split = Or.inl ⟨h12, h23, h13⟩) :
    CircumscribedMECPacket A (MT.toMoserTriangle.toStructural hCirc) where
  center := (MEC.mec A hA).center
  radius := (MEC.mec A hA).radius
  radius_pos := MEC.mec_radius_pos hA hncol
  moser_on_boundary_1 := by
    rw [← dist_eq_norm]
    exact MT.toMoserTriangle.v1_boundary
  moser_on_boundary_2 := by
    rw [← dist_eq_norm]
    exact MT.toMoserTriangle.v2_boundary
  moser_on_boundary_3 := by
    rw [← dist_eq_norm]
    exact MT.toMoserTriangle.v3_boundary
  inner_at_v1 := MT.inner_at_v1
  inner_at_v2 := MT.inner_at_v2
  inner_at_v3 := MT.inner_at_v3
  disk_contains_A := by
    intro a ha
    rw [← dist_eq_norm]
    exact (MEC.mec A hA).enclosing a ha

end CircumscribedMECPacket

end Problem97