A two-point base has at most two non-base apices

/- Generated theorem stub from Erdos9796Proof.P97.Dumitrescu.L6 by Stage 2 proof cut; source SHA-256 5734bd5bf1734a3ac1aec799aa89c43c6d0b026d07909ee8e7389ee71d40d90e -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Dumitrescu_L6
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Nat.Choose.Basic
open Problem97 Problem97.Dumitrescu



/-!
# Dumitrescu L6: cap good-edge quadratic bound (Corollary 9)

`Problem97.Dumitrescu.cap_good_edge_quadratic_of_ranking` and
`Problem97.Dumitrescu.cap_good_edge_quadratic` are the two forms of
Dumitrescu's Lemma 6 / Corollary 9
(Dumitrescu 2006 / Nivasch–Pach–Pinchasi–Zerbib 2013 (2012 preprint),
arXiv:1207.1266 §2 Corollary 9):

  Within a single convex-independent cap `C ⊆ A` of size `m`, the
  total **(witness-pair, non-base apex)** incidence count is `O(m²)`,
  where each cap witness pair `xy ∈ capWitnessPairs A C` contributes at
  most `2` non-base apexes (via L3) and the witness pair count itself
  is bounded by `m - 1` under a `CapWitnessRanking` (via L5) or
  unconditionally by `Nat.choose m 2` (via the trivial subset bound).

This file corresponds to the blueprint obligation
`p97-dumitrescu-l6-cap-good-edge-quadratic`.

## Composition

The proof is a clean double-count:

* **Per-pair apex bound (L3).**  For each base pair `(x, y)` with
  `x, y ∈ A`, `x ≠ y`,
  `Problem97.Dumitrescu.trivial_edge_bound_of_convexIndep` gives
  `|{a ∈ A : a ∉ {x, y} ∧ dist a x = dist a y}| ≤ 2`
  under `ConvexIndep A`.

* **Witness-pair count (L5 / unconditional).**  L5
  (`Problem97.Dumitrescu.cap_witness_uniqueness`) gives
  `|capWitnessPairs A C| ≤ C.card - 1` from a `CapWitnessRanking A C`;
  the unconditional fallback
  (`Problem97.Dumitrescu.capWitnessPairs_card_le_choose_two`) gives
  `|capWitnessPairs A C| ≤ Nat.choose C.card 2`.

* **Sum.**  Sum the per-pair bound `2` over the witness pairs.
  Multiplying gives the headline quadratic bound `O(m²)`.

The result is consumed by
`p97-dumitrescu-l8-three-cap-good-edge-count` (Corollary 10), which
sums over the three caps of a `CapTriple` and adds the
`crossCapEdges` count from L7.

## Per-pair apex Finset

The per-pair object is

```
capPairApexes A xy := A.filter (fun a => a ∉ xy ∧ ∃ r, ∀ q ∈ xy, dist a q = r)
```

which is the *unfolded* form of the L2 reindexing of
`Problem97.IsoscelesPairsAt` at base `xy`. By construction it ignores
the cap membership of the apex: a "good apex" for the chord `xy` can
sit anywhere in `A` (inside or outside `C`) as long as it is not on
the chord itself. This matches the paper's good-edge definition and
gives a strictly larger count than the cap-witness-pair count (which
requires apex `∉ C`); the L3 bound `≤ 2` applies in both settings.

## What this file does *not* assume

No `axiom` declarations. No vacuous `:= True` predicates. The two
headline theorems take a `ConvexIndep A` hypothesis (consumed by L3)
plus either a `CapWitnessRanking A C` (linear bound) or no extra
hypothesis (quadratic bound). All the heavy lifting (geometric
content of L1, witness-pair structure, ranking machinery) lives in
sibling files `DumitrescuL1.lean`, `DumitrescuL3.lean`,
`DumitrescuL5.lean`. L6 is the arithmetic composition.

## References

* Adrian Dumitrescu (2006), *On Distinct Distances from a Vertex of a Convex Polygon*, Discrete & Computational Geometry 36, 503–509. DOI: 10.1007/s00454-006-1262-y. (Original Lemma 6.)
* Gabriel Nivasch, János Pach, Rom Pinchasi, and Shira Zerbib, *The Number of Distinct Distances from a Vertex of a Convex Polygon*, Journal of Computational Geometry 4 (2013), 1–12; arXiv:1207.1266 (2012 preprint), Corollary 9.
-/

set_option linter.style.openClassical false

open scoped EuclideanGeometry
open Finset Classical




/- ### Per-pair apex filter

For a `2`-element subset `xy ⊆ A`, the *per-pair apex set* is the
collection of points `a ∈ A` with `a ∉ xy` and all points of `xy`
equidistant from `a`. Equivalently, `a` lies on the perpendicular
bisector of the chord `xy` and is not an endpoint. This is the L2
reindexing form (`Problem97.IsoscelesPairsAt` recast as a filter at a
fixed base) used for the per-pair contribution to the cap good-edge
count.

We keep the apex filter `A`-wide (not restricted to `A \ C`): the L3
bound `≤ 2` applies regardless, and the larger count subsumes both
the in-cap and out-of-cap apex contributions used downstream. -/

theorem Problem97.Dumitrescu.capPairApexes_card_le_two
    {A : Finset ℝ²} (hA : ConvexIndep A)
    {xy : Finset ℝ²} (hxy_sub : xy ⊆ A) (hxy_card : xy.card = 2) :
    (capPairApexes A xy).card ≤ 2 := by sorry