Counting transfer definition Erdos9796Counting_Cap_PartitionFromMEC

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.Cap.PartitionFromMEC; source SHA-256 cb2a5ce1101a74572ab57000424dc5f4df662f147fba1a7de73bfcf938646f93 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Cap_Structure
import Definitions.Def_Erdos9796Counting_MEC_Basic
import Definitions.Def_Erdos9796Counting_Moser_Triangle
import Definitions.Def_Erdos9796Counting_Moser_TriangleNonObtuse


/-!
# Cap partition from a circumscribed Moser triangle

This file bridges the geometric `Problem97.MEC.MoserTriangle`
(produced by the Sylvester dichotomy) to the structural
`Problem97.MoserTriangle` and from there to a `Problem97.CapTriple`
with the strengthened `arc_membership` field.

We restrict to the **circumscribed branch** of the dichotomy
(`case_split = Or.inl _`), where the three MEC-boundary vertices are
pairwise distinct.  The diameter branch (`Or.inr _`) is not handled
here; downstream consumers branch on the dichotomy.

The cap construction is the natural closed-arc filter using the
chord-separation predicate `Problem97.OnArcOpposite`:
* `C1 := A.filter (fun v => OnArcOpposite v1 v2 v3 v)`
* `C2 := A.filter (fun v => OnArcOpposite v2 v3 v1 v)`
* `C3 := A.filter (fun v => OnArcOpposite v3 v1 v2 v)`

Moser-vertex memberships fall out of algebraic identities (e.g.
`signedArea2 v1 v3 v1 = 0`) and the noncollinearity of the Moser
triangle vertices.  The "opposite apex not in own cap" clauses
(`v1 ∉ C1`, etc.) use that `signedArea2 v1 v2 v3 ≠ 0`.

## The `hAGenericCapCount` hypothesis

The closed-cap convention via `OnArcOpposite` is *algebraic* and does
not by itself imply that every non-Moser `A`-vertex lies in exactly
one cap.  Geometric counterexamples (e.g. a point strictly inside the
Moser triangle gives `0` caps; a point in a corner region gives `2`
caps) show the count is in `{0, 1, 2, 3}` over the affine plane.  For
the closed-cap-partition identity `|C1| + |C2| + |C3| = |A| + 3` to
hold downstream, we need the count to be exactly `1` on non-Moser
vertices — a *geometric* fact about A-vertices being either on the
MEC arc opposite to one of the Moser vertices, or strictly outside
exactly one chord.

We expose this as an explicit hypothesis `hAGenericCapCount`, which
downstream consumers establish via MEC + ConvexIndep + circumscribed
case structure.

## Main declarations

* Algebraic identities for `signedArea2` (`signedArea2_self_*`).
* Lemmas `onArcOpposite_of_chord_endpoint_{left,right}` — Moser
  vertex endpoints lie on their adjacent caps.
* `Problem97.signedArea2_eq_zero_of_onArcOpposite_self` — apex lies
  on its own cap only if the area degenerates.
* `Problem97.MEC.MoserTriangle.toStructural` — project the
  circumscribed branch to a structural `Problem97.MoserTriangle`.
* `Problem97.MEC.cap_partition_from_moser_circumscribed` — the main
  cap-partition existence theorem.
* `Problem97.SurplusCapPacket` — Moser triangle (carried as a
  non-obtuse circumscribed MEC triangle plus the circumscribed
  case-split) + cap triple over its structural projection +
  designation of one cap as surplus (`|Ci| > 4`).  This is the
  MEC-aware packet that downstream U1 sub-lemmas consume.
* `Problem97.SurplusCapPacket.IsM44` — predicate saying the cap
  multiset is `(m, 4, 4)` with `m ≥ 5`, and the surplus cap is the
  long one.
-/

open scoped EuclideanGeometry
open Finset

namespace Problem97

/- ### Algebraic identities for `signedArea2` -/





/- ### `OnArcOpposite` for Moser vertices -/







namespace MEC

/- ### Bridge: circumscribed `MEC.MoserTriangle` → structural `MoserTriangle` -/

/-- Project a circumscribed `Problem97.MEC.MoserTriangle` to a
structural `Problem97.MoserTriangle` (pairwise-distinct).  The
hypothesis `hCircumscribed` selects the left disjunct of `case_split`,
which carries the three pairwise-distinctness witnesses. -/
def MoserTriangle.toStructural
    {A : Finset ℝ²} {hA : A.Nonempty} {hncol : ¬ Collinear ℝ (A : Set ℝ²)}
    (MT : Problem97.MEC.MoserTriangle A hA hncol)
    (hCircumscribed : ∃ h12 h23 h13,
      MT.case_split = Or.inl ⟨h12, h23, h13⟩) :
    Problem97.MoserTriangle A :=
  { v1 := MT.v1
    v2 := MT.v2
    v3 := MT.v3
    v1_mem := MT.v1_mem
    v2_mem := MT.v2_mem
    v3_mem := MT.v3_mem
    v12_ne := by
      obtain ⟨h12, _, _, _⟩ := hCircumscribed
      exact h12
    v13_ne := by
      obtain ⟨_, _, h13, _⟩ := hCircumscribed
      exact h13
    v23_ne := by
      obtain ⟨_, h23, _, _⟩ := hCircumscribed
      exact h23 }

/- ### Cap-partition existence theorem -/



end MEC

/- ### Surplus cap: cap of size `> 4` (MEC-aware packet) -/

/-- A `SurplusCapPacket` on `A` is the data of

* a non-obtuse circumscribed Moser triangle on `A`
  (`triangleNonObtuse : MEC.NonObtuseCircumscribedMoserTriangle A hA hncol`),
* a witness `hCirc` selecting the circumscribed branch of the underlying
  dichotomy (so the structural projection has pairwise-distinct
  vertices),
* a cap triple over the *structural projection* of that triangle,
* and a *designation* of one cap as surplus (`|Ci| > 4`).

The MEC promotion data is carried directly inside the packet so that
downstream U1 sub-lemmas can immediately apply
`cap_arc_midpoint_inequality_v{1,2,3}` (which take exactly these
parameters).

We use the cap index `0, 1, 2` for `C1, C2, C3` respectively to make
the "which cap" data uniform; cap selectors below let downstream code
project to the surplus cap and the two opposite caps. -/
structure SurplusCapPacket (A : Finset ℝ²) where
  /-- `A` is nonempty (needed for the MEC). -/
  hA : A.Nonempty
  /-- `A` is not collinear (needed for the MEC dichotomy). -/
  hncol : ¬ Collinear ℝ (A : Set ℝ²)
  /-- The chosen MEC-promoted Moser triangle with all three vertex
  angles non-obtuse. -/
  triangleNonObtuse : MEC.NonObtuseCircumscribedMoserTriangle A hA hncol
  /-- The triangle is in the circumscribed branch of the dichotomy
  (three pairwise-distinct MEC-boundary vertices). -/
  hCirc : ∃ h12 h23 h13,
    triangleNonObtuse.toMoserTriangle.case_split = Or.inl ⟨h12, h23, h13⟩
  /-- The associated cap triple over the structural projection. -/
  partition :
    CapTriple A (triangleNonObtuse.toMoserTriangle.toStructural hCirc)
  /-- Index of the surplus cap (`0`, `1`, or `2`). -/
  surplusIdx : Fin 3
  /-- The surplus cap has more than `4` vertices. -/
  surplus : (4 : ℕ) <
    (match surplusIdx with
      | ⟨0, _⟩ => partition.C1
      | ⟨1, _⟩ => partition.C2
      | _      => partition.C3).card

namespace SurplusCapPacket

variable {A : Finset ℝ²}













end SurplusCapPacket



/- ### `(m, 4, 4)` regime predicate -/







namespace SurplusCapPacket



























end SurplusCapPacket

end Problem97