Counting transfer definition Erdos9796Counting_CGN_CGN

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.CGN.CGN; source SHA-256 9f1ccd7df30637d7fbdf412fb40177dedb5193c45ec2993df86f137cbd34ffb7 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Fin


/-!
# CGN7: indexed cap-side witness matching scaffold

This file records the CGN7-local indexed witness relation requested by the
updated counterexample-card-ge-nine prose.  The geometry that produces the
one-sided injectivity hypotheses lives in the CGN6 lemmas; this module only
packages the ordered-cap interface and the partial-matching counting shell.
-/

open scoped EuclideanGeometry
open scoped InnerProductSpace
open Finset

namespace Problem97
namespace CGN

/-- A duplicate-free ordered cap list, represented as an indexed map
`Fin m → ℝ²` together with injectivity.  This is the Lean stand-in for the
cap order `L = [p₁, ..., p_m]`. -/
structure OrderedCap (m : ℕ) where
  points : Fin m → ℝ²
  injective : Function.Injective points

namespace OrderedCap

variable {m : ℕ}

/-- Apply an injective point map to an ordered cap. -/
def map (L : OrderedCap m) (T : ℝ² → ℝ²) (hT : Function.Injective T) :
    OrderedCap m where
  points := fun i => T (L.points i)
  injective := by
    intro i j hij
    apply L.injective
    exact hT hij



end OrderedCap

/-- Transport data for a Euclidean similarity `T`.  The normalization theorem
records only the facts used downstream: distance scaling, distance equality,
convex-hull transport, and the oriented signed-area factor. -/
structure SimilarityTransportData (T : ℝ² → ℝ²) where
  /-- Positive similarity scale. -/
  scale : ℝ
  /-- The similarity scale is positive. -/
  scale_pos : 0 < scale
  /-- Distances are scaled by `scale`. -/
  dist_image : ∀ a b : ℝ², dist (T a) (T b) = scale * dist a b
  /-- Equality of two distances is preserved and reflected by `T`. -/
  dist_eq_iff : ∀ a b c : ℝ²,
      dist (T a) (T b) = dist (T a) (T c) ↔ dist a b = dist a c
  /-- Convex-hull membership is transported along `T`. -/
  convexHull_mem_iff : ∀ {S : Set ℝ²} {a : ℝ²},
      T a ∈ convexHull ℝ (T '' S) ↔ a ∈ convexHull ℝ S
  /-- Orientation sign recorded for half-plane tests. -/
  orientation : ℝ
  /-- The orientation sign is its own inverse. -/
  orientation_sq : orientation ^ 2 = 1
  /-- Oriented signed-area tests are transported by `T`. -/
  halfplane_sign : ∀ a b c : ℝ²,
      signedArea2 (T a) (T b) (T c) =
        orientation * (scale ^ 2) * signedArea2 a b c

/-- The first endpoint index `0`, packaged as a `Fin m` from the lower-bound
certificate `2 ≤ m`. -/
def firstIndex {m : ℕ} (hm : 2 ≤ m) : Fin m :=
  ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hm⟩

/-- The last endpoint index `m - 1`, packaged as a `Fin m` from the lower-bound
certificate `2 ≤ m`. -/
def lastIndex {m : ℕ} (hm : 2 ≤ m) : Fin m :=
  ⟨m - 1, by
    have hm1 : 0 < m := lt_of_lt_of_le (by decide : 0 < 2) hm
    exact Nat.sub_lt hm1 (by decide : 0 < (1 : ℕ))
  ⟩







/-- The MEC packet for one ordered cap `L`.  The fields match the updated
closure-plan interface exactly. -/
structure MecCapPacket (A : Finset ℝ²) {m : ℕ} (L : OrderedCap m) where
  /-- The cap has at least two points, so both endpoints exist. -/
  hm : 2 ≤ m
  /-- MEC center. -/
  center : ℝ²
  /-- MEC radius. -/
  radius : ℝ
  /-- The radius is nonnegative. -/
  radius_nonneg : 0 ≤ radius
  /-- Every cap vertex lies in `A`. -/
  mem_A : ∀ t : Fin m, L.points t ∈ A
  /-- Every cap vertex lies in the MEC disk. -/
  disk_mem : ∀ t : Fin m, dist (L.points t) center ≤ radius
  /-- First endpoint lies on the MEC circle. -/
  first_on_circle : dist (L.points (firstIndex hm)) center = radius
  /-- Last endpoint lies on the MEC circle. -/
  last_on_circle : dist (L.points (lastIndex hm)) center = radius

/-- The side hypotheses for a MEC cap packet.  This keeps the chord
orientation fixed for the normalization theorem. -/
structure MinorCapSideHypotheses {m : ℕ} {A : Finset ℝ²} {L : OrderedCap m}
    (P : MecCapPacket A L) where
  /-- The cap lies on the nonnegative side of the endpoint chord. -/
  cap_side_nonneg :
    ∀ t : Fin m,
      0 ≤ signedArea2 (L.points (firstIndex P.hm)) (L.points (lastIndex P.hm)) (L.points t)
  /-- The MEC center lies on the nonpositive side of the endpoint chord. -/
  center_side_nonpos :
    signedArea2 (L.points (firstIndex P.hm)) (L.points (lastIndex P.hm)) P.center ≤ 0

/-- The strict ordered-cap hypotheses used by the normalization theorem. -/
structure StrictCapOrder (A : Finset ℝ²) {m : ℕ} (L : OrderedCap m) where
  /-- The cap has at least two points, so the two endpoints exist. -/
  hm : 2 ≤ m
  /-- Consecutive turns are nonpositive. -/
  consecutive_turn_nonpos :
    ∀ t : ℕ, ∀ ht : t + 2 < m,
      signedArea2 (L.points ⟨t, by
          exact lt_trans (Nat.lt_add_of_pos_right (by decide : 0 < (2 : ℕ))) ht⟩)
        (L.points ⟨t + 1, by
          exact lt_trans
            (Nat.succ_lt_succ (Nat.lt_add_of_pos_right (by decide : 0 < (1 : ℕ))))
            ht⟩)
        (L.points ⟨t + 2, by
          exact ht⟩) ≤ 0
  /-- Strict chord-projection order along the endpoint chord. -/
  chord_projection_strict :
    ∀ {i j : Fin m}, i < j →
      inner ℝ (L.points j - L.points i)
        (L.points (lastIndex hm) - L.points (firstIndex hm)) > 0
  /-- Positive-side subchord points are exactly the indexed cap vertices in between. -/
  subchord_open_side_iff_A :
    ∀ {r s : Fin m}, r < s → ∀ {x : ℝ²}, x ∈ A →
      (0 < signedArea2 (L.points r) (L.points s) x ↔
        ∃ j : Fin m, r < j ∧ j < s ∧ L.points j = x)

/-- Canonical CGN7 witness relation, oriented from the earlier endpoint `r`
to the later endpoint `s`.  It records the ordered split `r < j < s` and the
equal-distance witness condition at the cap vertex `L[j]`. -/
def WitnessesCapEdgeAt {m : ℕ} (L : OrderedCap m) (j r s : Fin m) : Prop :=
  r < j ∧ j < s ∧ dist (L.points j) (L.points r) = dist (L.points j) (L.points s)

/-- Finset of witnessed ordered pairs at index `j`. -/
noncomputable def WitnessedPairsAt {m : ℕ} (L : OrderedCap m) (j : Fin m) :
    Finset (Fin m × Fin m) := by
  classical
  exact Finset.univ.filter (fun p => WitnessesCapEdgeAt L j p.1 p.2)











/-- Oriented index pairs for cap edges. -/
def CapIndexPairs (m : ℕ) : Finset (Fin m × Fin m) :=
  Finset.univ.filter fun p => p.1 < p.2



/-- The unordered base pair determined by two oriented cap indices. -/
noncomputable def edgeAt {m : ℕ} (L : OrderedCap m) (r s : Fin m) : Finset ℝ² :=
  {L.points r, L.points s}





/-- A witness is simply an indexed cap-side witness. -/
def HasCapWitness {m : ℕ} (L : OrderedCap m) (r s : Fin m) : Prop :=
  ∃ j : Fin m, WitnessesCapEdgeAt L j r s

/-- The negation of a cap witness. -/
def NoCapWitness {m : ℕ} (L : OrderedCap m) (r s : Fin m) : Prop :=
  ¬ HasCapWitness L r s





-- The next two CGN7c theorems depend on the missing CGN6e indexed-witness
-- bridge.  Stop here rather than inventing that geometry.

end CGN
end Problem97