Counting transfer definition Erdos9796Counting_Cap_Partition

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.Cap.Partition; source SHA-256 baaf503023695b8e0b1c19f8745478e6ec02a514e175bd113f5346c7d25a5e27 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.SDiff


/-!
# Cap-partition sum identity (Erdős Problem 97, Milestone 4)

Pure combinatorics extracted from the geometric setup in the universal
proof of Erdős Problem 97 (`p97-positive-defect-bridge`).

**Geometric origin.** In the universal-descent argument for Problem 97
(see `docs/97-uniform-theorem-closure-plan.md`), a convex counterexample
`P` to the 4-equidistant property carries three "caps" `C₁, C₂, C₃` cut
out by closed chains between three selected Moser vertices.  Each Moser vertex lies on exactly two opposite caps and
every other vertex on exactly one of the three chains, so

  `|C₁| + |C₂| + |C₃| = n + 3`

where `n = |P|`.

The geometry only enters via the membership pattern.  Once you fix it,
the identity is a pure counting lemma:

* a finset `S` (the vertex set),
* a 3-element subset `M ⊆ S` (the Moser vertices),
* three subsets `C₁, C₂, C₃ ⊆ S` such that every Moser vertex hits
  exactly two of them and every non-Moser vertex hits exactly one,

then `|C₁| + |C₂| + |C₃| = |S| + 3`.

Both pieces of data ("Moser vertex ⇒ in exactly two caps" and
"non-Moser ⇒ in exactly one cap") are packaged in a structure
`CapPartition` so the geometric obligation can hand the combinatorics
a single bundled object.

This is `p97-cap-sum-identity` (Milestone 4 sub-step 2 of 4).  It is
independent of the geometric existence proofs and provable from the
structural setup alone.
-/

open Finset

namespace Problem97

/-- Combinatorial cap-partition data for a finset `S` over a 3-element
Moser subset `M ⊆ S`: three caps `C₁, C₂, C₃ ⊆ S` with every Moser
vertex in exactly two caps and every non-Moser vertex in exactly one. -/
structure CapPartition {α : Type*} [DecidableEq α]
    (S : Finset α) (M : Finset α) where
  /-- First cap. -/
  C1 : Finset α
  /-- Second cap. -/
  C2 : Finset α
  /-- Third cap. -/
  C3 : Finset α
  /-- The Moser set has exactly three vertices. -/
  M_card : M.card = 3
  /-- The Moser set is a subset of the ambient finset. -/
  M_sub : M ⊆ S
  /-- The first cap is contained in the ambient finset. -/
  C1_sub : C1 ⊆ S
  /-- The second cap is contained in the ambient finset. -/
  C2_sub : C2 ⊆ S
  /-- The third cap is contained in the ambient finset. -/
  C3_sub : C3 ⊆ S
  /-- Every Moser vertex belongs to exactly two of the three caps. -/
  moser_in_two : ∀ v ∈ M,
    (if v ∈ C1 then 1 else 0)
      + (if v ∈ C2 then 1 else 0)
      + (if v ∈ C3 then 1 else 0) = 2
  /-- Every non-Moser vertex in the ambient finset belongs to exactly one cap. -/
  nonmoser_in_one : ∀ v ∈ S, v ∉ M →
    (if v ∈ C1 then 1 else 0)
      + (if v ∈ C2 then 1 else 0)
      + (if v ∈ C3 then 1 else 0) = 1



end Problem97