Counting transfer definition Erdos9796Counting_CGN_CGN4g

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.CGN.CGN4g; source SHA-256 c412b95ca627805e0db3a1f0d192f80b93891249e4eb1369844d4f8206dcba79 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_CGN_CGN
import Mathlib.Data.Finset.Sort
import Mathlib.Logic.Equiv.Fin.Rotate
import Mathlib.Order.Interval.Finset.Fin


/-!
# CGN4g: ordered-cap block packaging

This file adds the closure-plan data carrier for the ordered-cap block cut out
of a global convex-boundary enumeration, together with the theorem wrappers
that are pure packaging.

The geometric producers for the block (`CGN4g1`, `CGN4g3`, `CGN4g4`) remain
separate. The declarations here are the sanctioned interfaces consumed by the
existing CGN6 / CGN7 layers.
-/

open scoped EuclideanGeometry
open scoped InnerProductSpace

namespace Problem97
namespace CGN



/-- A support cap `C` presented as a contiguous ordered block inside a global
boundary enumeration `phi`. -/
structure BoundaryCapBlock (A C : Finset ℝ²) {n m : ℕ}
    (phi : Fin n → ℝ²) (L : OrderedCap m) where
  /-- The block has at least two points, so both endpoints exist. -/
  hm : 2 ≤ m
  /-- Left endpoint of the block in the global enumeration. -/
  lo : Fin n
  /-- Right endpoint of the block in the global enumeration. -/
  hi : Fin n
  /-- The global boundary indices are ordered from `lo` to `hi`. -/
  hlohi : lo < hi
  /-- Reindex the local cap order into the global boundary order. -/
  idx : Fin m → Fin n
  /-- The local-to-global reindexing is strictly increasing. -/
  idx_strict : StrictMono idx
  /-- The first local point is the left global endpoint. -/
  idx_first : idx (firstIndex hm) = lo
  /-- The last local point is the right global endpoint. -/
  idx_last : idx (lastIndex hm) = hi
  /-- The reindexing hits exactly the closed global interval `[lo, hi]`. -/
  idx_range_exact : ∀ q : Fin n, (lo ≤ q ∧ q ≤ hi) ↔ ∃ t : Fin m, idx t = q
  /-- Local cap points are the corresponding points of the global enumeration. -/
  points_eq : ∀ t : Fin m, L.points t = phi (idx t)
  /-- The local cap image is exactly the support cap `C`. -/
  cap_image : Finset.univ.image L.points = C
  /-- The support cap lies in the ambient finite set. -/
  cap_subset_A : C ⊆ A
  /-- The global enumeration realizes the ambient finite set. -/
  phi_image : Finset.univ.image phi = A

/-- Retained ordered-cap block data.

This is the theorem-facing carrier for arguments that need both the local
ordered cap and the original global boundary block.  The older public
`CGN4g_capData_of_supportCap_oriented` wrapper exposes `OrderedCap` and
`StrictCapOrder` but forgets the `BoundaryCapBlock`; consumers that need
endpoint indices or interval transport should depend on this packet instead. -/
structure StrictCapBlockData (A C : Finset ℝ²) where
  /-- Length of the ambient global boundary enumeration. -/
  n : ℕ
  /-- Length of the retained local cap block. -/
  m : ℕ
  /-- Global boundary enumeration. -/
  phi : Fin n → ℝ²
  /-- The retained global boundary enumeration is injective. -/
  phi_injective : Function.Injective phi
  /-- The retained global boundary enumeration is counterclockwise convex. -/
  phi_ccw : EuclideanGeometry.IsCcwConvexPolygon phi
  /-- Local ordered cap cut out from the global enumeration. -/
  L : OrderedCap m
  /-- MEC packet for the local cap. -/
  Packet : MecCapPacket A L
  /-- Side hypotheses for the local cap packet. -/
  Hside : MinorCapSideHypotheses Packet
  /-- The retained local-to-global interval block. -/
  Block : BoundaryCapBlock A C phi L
  /-- The strict ordered-cap interface consumed by CGN6 / CGN7. -/
  Hord : StrictCapOrder A L

namespace StrictCapBlockData

variable {A C : Finset ℝ²}



































end StrictCapBlockData









end CGN





namespace CGN















end CGN
end Problem97