Counting transfer definition Erdos9796Counting_CGN_CGN6

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.CGN.CGN6; source SHA-256 87eeea2860c10b6c484c3d7aec9f295605a553c9956e5cc04bbc649402bc9c30 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_CGN_CGN
import Mathlib.Analysis.Convex.Hull
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Orthonormal
import Mathlib.Analysis.InnerProductSpace.TwoDim
import Mathlib.Geometry.Euclidean.PerpBisector
import Mathlib.Order.Interval.Finset.Fin


/-!
# CGN6: normalized minor-cap chain model

This file starts the CGN6 layer named in the updated counterexample-card-ge-nine
prose. It records the normalized minor-cap chain data the prose uses for the
CGN6b slope-product argument: ordered coordinates, endpoint normalization, the
unit-disk bound, and the adjacent-slope bookkeeping.

The actual geometric construction of this model from a concrete MEC cap packet
is still separate. This file only provides the data interface the subsequent
CGN6b / CGN6c proofs will consume.
-/

open scoped EuclideanGeometry
open scoped InnerProductSpace
open scoped BigOperators

namespace Problem97
namespace CGN

/-- Convert a natural index into a `Fin m` index. -/
def finIndex (m : ℕ) (n : ℕ) (hn : n < m) : Fin m :=
  ⟨n, hn⟩

/-- The slope of the secant line through two indexed points in a normalized
minor-cap chain. The intended use always supplies `i < j`, so the denominator
is positive. -/
noncomputable def slopeAt {m : ℕ} (X Y : Fin m → ℝ)
    (i j : ℕ) (hi : i < m) (hj : j < m) : ℝ :=
  (Y (finIndex m j hj) - Y (finIndex m i hi))
    / (X (finIndex m j hj) - X (finIndex m i hi))

/-- Reconstruct the `ℝ²`-point from its coordinates. -/
noncomputable def point {m : ℕ} (X Y : Fin m → ℝ) (t : Fin m) : ℝ² :=
  (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 => if i = 0 then X t else Y t)

/-- Construct a vector in `ℝ²` from its two coordinates. -/
noncomputable def vec2 (x y : ℝ) : ℝ² :=
  EuclideanSpace.single 0 x + EuclideanSpace.single 1 y

/-- The left adjacent secant slope `slope(t, t+1)` in natural indexing. -/
noncomputable def adjacentSlope {m : ℕ} (X Y : Fin m → ℝ)
    (t : ℕ) (h : t + 1 < m) : ℝ :=
  slopeAt X Y t (t + 1) (by omega) h

/-- The right adjacent secant slope `slope(t+1, t+2)` in natural indexing. -/
noncomputable def nextAdjacentSlope {m : ℕ} (X Y : Fin m → ℝ)
    (t : ℕ) (h : t + 2 < m) : ℝ :=
  slopeAt X Y (t + 1) (t + 2) (by omega) (by omega)

/-- Totalized `X` coordinate on natural indices. Outside the valid range, this
returns `0` so that interval sums can be written on `ℕ`. -/
noncomputable def xCoord {m : ℕ} (X : Fin m → ℝ) (n : ℕ) : ℝ :=
  if h : n < m then X (finIndex m n h) else 0

/-- Totalized `Y` coordinate on natural indices. Outside the valid range, this
returns `0` so that interval sums can be written on `ℕ`. -/
noncomputable def yCoord {m : ℕ} (Y : Fin m → ℝ) (n : ℕ) : ℝ :=
  if h : n < m then Y (finIndex m n h) else 0

/-- Totalized adjacent slope on natural indices. Outside the valid range, this
returns `0` so that interval sums can be written on `ℕ`. -/
noncomputable def adjSlopeNat {m : ℕ} (X Y : Fin m → ℝ) (t : ℕ) : ℝ :=
  if h : t + 1 < m then slopeAt X Y t (t + 1) (by omega) h else 0

/-- Internal normalized minor-cap chain coordinates. The cap points are indexed
in order and carry separate `X` / `Y` coordinates. The fields match the prose
package:

* `X_0 = -1`, `X_(m-1) = 1`
* `Y_0 = Y_(m-1) = 0`
* strict `X`-monotonicity
* all points lie in the unit disk
* adjacent secant slopes are weakly decreasing

The coordinate core is the boundary object for CGN6b; it is stronger than
`OrderedCap` because it remembers the geometric normalization data. -/
structure MinorCapChainCoords (m : ℕ) where
  /-- The cap has at least two points, so the two endpoints exist. -/
  hm : 2 ≤ m
  /-- `X`-coordinates of the normalized cap chain. -/
  X : Fin m → ℝ
  /-- `Y`-coordinates of the normalized cap chain. -/
  Y : Fin m → ℝ
  /-- Strict increase of the `X` coordinates. -/
  x_strict : ∀ {i j : Fin m}, i < j → X i < X j
  /-- Left endpoint normalization. -/
  X_first : X (finIndex m 0 (by omega)) = -1
  /-- Right endpoint normalization. -/
  X_last : X (finIndex m (m - 1) (by omega)) = 1
  /-- Left endpoint lies on the diameter. -/
  Y_first : Y (finIndex m 0 (by omega)) = 0
  /-- Right endpoint lies on the diameter. -/
  Y_last : Y (finIndex m (m - 1) (by omega)) = 0
  /-- Every point lies in the closed upper half-plane. -/
  y_nonneg : ∀ t : Fin m, 0 ≤ Y t
  /-- Every point lies in the closed unit disk. -/
  unit_disk : ∀ t : Fin m, X t ^ 2 + Y t ^ 2 ≤ 1
  /-- Adjacent secant slopes `d_t = slope(t, t+1)` are weakly decreasing. -/
  adjacent_slopes_decreasing :
    ∀ t : ℕ, ∀ h : t + 2 < m,
      adjacentSlope X Y t (by omega) ≥ nextAdjacentSlope X Y t h

/-- The public normalized model attached to an ordered cap `L`.  It stores the
coordinate core plus the point-coordinate coherence field used by the CGN6c /
CGN6e transport steps. -/
structure MinorCapChainModel {m : ℕ} (L : OrderedCap m) where
  /-- Normalized coordinates of the cap chain. -/
  coords : MinorCapChainCoords m
  /-- The cap points are exactly the normalized coordinates. -/
  points_eq : ∀ t : Fin m, L.points t = point coords.X coords.Y t

/- ### CGN6norm scaffold

The prose normalization theorem uses an explicit coordinate frame
centered at the chord midpoint and aligned with the chord / inward
normal directions.  The full packet-to-frame bridge is still separate;
this helper records the coordinate map in the exact algebraic form used
by the prose.
-/

/-- Explicit chord-frame coordinate map used by the CGN6 normalization.

The intended instantiation is the midpoint/rotation/reflection/scaling
map from the prose proof: the `scale` parameter is `2 / ‖q_m - q_1‖`
and the two direction vectors are the normalized chord and inward normal
vectors. -/
noncomputable def chordFrame (M e n : ℝ²) (scale : ℝ) : ℝ² → ℝ² :=
  fun z =>
    (EuclideanSpace.equiv (Fin 2) ℝ).symm (fun i : Fin 2 =>
      if i = 0 then scale * ⟪z - M, e⟫_ℝ else scale * ⟪z - M, n⟫_ℝ)





























-- The normalization proof is large enough to need a higher elaboration budget.








































end CGN
end Problem97