Counting transfer definition Erdos9796Counting_MEC_ArcAngle

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.MEC.ArcAngle; source SHA-256 4d7ceebcbb8adcb5f2581ad54e00ef84ce109370fabe4fdf83c165b1fc179150 -/
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_SignedAreaOangle


/-!
# MEC arc-angle parametrization — A0 (definition + algebra)

This file introduces `Problem97.arcAngle center p : Real.Angle`, the oriented
angle in `ℝ / 2πℤ` between the canonical first basis vector
`EuclideanSpace.basisFun (Fin 2) ℝ 0` and the chord `p - center`. Geometrically
this is the angular position of `p` on a circle centered at `center`, measured
from the `+x` direction in the standard counter-clockwise orientation of `ℝ²`.

## Why `Real.Angle` rather than `ℝ`

The natural alternative — `Complex.arg : ℂ → ℝ` with range `(-π, π]` — forces a
branch cut through the negative `x`-axis. Caps in the MEC analysis routinely
straddle this cut and every monotonicity lemma would need to case-split on it.
Quotienting by `2π` (i.e. landing in `Real.Angle = ℝ / 2πℤ`) eliminates the
branch cut. Signed circular differences (`arcAngle p − arcAngle q`) are then
well-defined and compose cleanly via `Orientation.oangle` algebra.

## Cross-reference

See `docs/97-arc-angle-parametrization-plan.md` § "A0 — `arcAngle` definition +
algebra" for the four-step program (A0 + A1 + A2 + A3).

## Status — A0 + A1 + A2 + A3 (plus A3-iff)

This file establishes the full A0-A3 program plus the equality / iff forms of
A3 added by the Dumitrescu Lc1 dispatch (2026-05-22):

* `arcAngle` definition.
* Identity 1: `arcAngle_center_self` — at the apex itself the angle is `0`.
* Identity 2: `arcAngle_sub_arcAngle` — the central subtraction bridge to
  `Orientation.oangle` on the chord vectors. **Load-bearing** for downstream
  A1/A2/A3.
* Identity 3: `arcAngle_neg` — antipodal reflection adds `π`.
* A1 — `onArcOpposite_iff_oangle_sign_mul`: chord-side `OnArcOpposite vi vj vk v`
  is equivalent to the product of two `Orientation.oangle` signs being `≤ 0`.
  This is the inscribed-angle form (oangles centered at the test points `v` and
  `vi`, not at the MEC center).
* A1 — `onArcOpposite_iff_arcAngle_sign_mul`: the same iff restated as a sign
  product of arc-angle differences, by applying `arcAngle_sub_arcAngle` with the
  test point itself as the center. This is the form downstream consumers (Lc1,
  Nivasch–Pach–Pinchasi–Zerbib L6, the U-sequence geometric core) read out of A1.
* A2 — `arcAngle_chord_length` chord-length formula `dist p q = 2 r |sin(Δ/2)|`.
* A3 — `arcAngle_chord_length_strict_mono` strict monotonicity of chord length
  in arc-angle difference; analytic core `abs_sin_half_strict_mono`.
* **A3-iff** (Dumitrescu Lc1 dispatch, 2026-05-22): the equality and `<` iff
  forms `arcAngle_chord_length_eq_iff`, `arcAngle_chord_length_lt_iff`, and
  their analytic counterparts `abs_sin_half_eq_iff`, `abs_sin_half_lt_iff`.
  The equality form is the load-bearing input to the Dumitrescu witness-pair
  ranking argument: "two MEC-arc points equidistant from a third MEC-arc
  point have arc-angle differences equal in absolute value" — exactly the
  arc-symmetry-about-the-apex assertion the Lc1 diagonal-vertex argument
  needs to convert "common apex" into a positional constraint.

## Sign / argument-order convention for Identity 2

The conclusion of `arcAngle_sub_arcAngle` is

```
arcAngle center p - arcAngle center q
  = stdOrientation.oangle (q - center) (p - center)
```

i.e. with `q - center` **first** and `p - center` **second** on the right. This
matches the direct consequence of `Orientation.oangle_sub_left` and is the
mathematically correct direction. The scoping report tentatively wrote the RHS
arguments in the opposite order; that order would flip the sign relative to
this lemma. Downstream consumers (A1's `OnArcOpposite` bridge,
`signedArea2_sign_eq_oangle_sign`) read the chord endpoints out of the
right-hand `oangle`, so when composing with this lemma they should identify
`vj = q` and `vk = p` (or equivalently apply `Orientation.oangle_rev` if the
opposite arg order is desired).

## A1 — Status and approach

The scoping report (`docs/97-arc-angle-parametrization-plan.md` §3, §5 A1)
proposed defining a 3-angle predicate `Real.Angle.btwArcNotThrough` and
formulating A1 as `OnArcOpposite vi vj vk v ↔ btwArcNotThrough …` on arc-angles
of `vj, vk, v` centered at the **MEC center**. The plan further claimed the iff
would reduce to `signedArea2_sign_eq_oangle_sign` + A0 alone, **without**
invoking the inscribed-angle theorem `Sphere.two_zsmul_oangle_eq`.

This dispatch confirms that the iff goes through with **no inscribed-angle
theorem and no cospherical / MEC-center hypothesis**, but the cleanest form does
not match the scoped predicate. The bridge
`signedArea2_sign_eq_oangle_sign` already returns an `Orientation.oangle`
*centered at the test point*, not at the MEC center. Applying A0
(`arcAngle_sub_arcAngle`) with `center := v` (and again with `center := vi`)
re-expresses each chord-vector `oangle` as a *difference* of arc-angles
centered at the test point itself. The resulting A1 statement is therefore a
sign equation on `arcAngle v · - arcAngle v ·` and `arcAngle vi · - arcAngle vi ·`,
*not* on `arcAngle center vi`, `arcAngle center vj`, `arcAngle center vk`,
`arcAngle center v` for a common `center`.

Concretely, A1 lands in two forms (a "core" oangle form, and an "arc-angle"
form by an immediate rewrite under A0):

```
onArcOpposite_iff_oangle_sign_mul :
  OnArcOpposite vi vj vk v ↔
    (stdOrientation.oangle (vj - v) (vk - v)).sign *
      (stdOrientation.oangle (vj - vi) (vk - vi)).sign ≤ 0

onArcOpposite_iff_arcAngle_sign_mul :
  OnArcOpposite vi vj vk v ↔
    (arcAngle v vk - arcAngle v vj).sign *
      (arcAngle vi vk - arcAngle vi vj).sign ≤ 0
```

Both require `vj ≠ v`, `vk ≠ v`, `vj ≠ vi`, `vk ≠ vi`. There is no MEC center,
no radius, and no cospherical hypothesis: A1 is a *purely chord-side* fact
about four points in the plane, with `arcAngle` serving as a notational
convenience for the inscribed-angle reading. Downstream consumers that want a
"common-center" form will need to fold in the inscribed-angle theorem
explicitly when they consume A1 — that step is **not** in A1's scope.

**Deviation from the scoping report.** The report's tentative
`btwArcNotThrough α β γ` 3-angle predicate is not used. After working through
the algebra, the predicate did not improve compositional clarity over the
direct sign-product form, and would have required either committing to a
common arc-center (forcing the inscribed-angle theorem) or duplicating the
sign-product statement under a wrapper. The wrapper-free form keeps A1 a one
`rw`-step composition of A0 and `signedArea2_sign_eq_oangle_sign`, with no new
predicates introduced.

## A2 — Status and approach

A2 establishes the **chord-length formula on a sphere**: for `p`, `q` both at
distance `r` from `center` (with `r > 0`), the Euclidean distance
`dist p q` equals `2 r · |sin((θ).toReal / 2)|` where
`θ = arcAngle center p - arcAngle center q`.

**Statement-shape deviation from the scoping report.** The plan (§S3, §5 A2)
proposed the canonical form

```
dist p q = 2 r · |Real.Angle.sin ((arcAngle center p - arcAngle center q) / 2)|
```

but `Real.Angle` has no `HDiv Real.Angle ℕ` instance — `θ / 2` is not
type-correct for `θ : Real.Angle`. The standard Mathlib idiom in this regime
is to lower the angle to its real representative via `Real.Angle.toReal`
(picking the unique lift in `(-π, π]`) and divide there:

```
dist p q = 2 r · |Real.sin ((arcAngle center p - arcAngle center q).toReal / 2)|
```

`|sin|` is invariant under `± 2π` shifts of its argument, so the choice of
`Real.Angle` lift does not affect the right-hand side. Downstream consumers
that prefer working entirely in `Real.Angle` can apply `Real.Angle.sin_toReal`
to convert between `Real.Angle.sin` and `Real.sin _.toReal` as needed, but the
formula on the angle quotient itself requires a packaged half-angle predicate
that Mathlib does not provide.

**Mathlib hook unavailable.** The plan flagged
`EuclideanGeometry.Sphere.dist_div_sin_oangle_div_two_eq_radius` as a possible
single-step closer, but that lemma takes three points all on the sphere
(`p₁, p₂, p₃ ∈ s`) and the angle is `oangle p₁ p₂ p₃` with the apex `p₂` *on*
the sphere — it is the *inscribed-angle* form. In A2 the apex is `center`,
which is **not** on the sphere. The lemma therefore does not apply; the proof
takes the plan's recommended polarization fallback.

**Proof sketch (polarization).** Let `u := p - center`, `v := q - center`, so
`‖u‖ = ‖v‖ = r`. Then

```
dist(p,q)² = ‖u - v‖²
           = ‖u‖² − 2⟪u, v⟫ + ‖v‖²        (norm_sub_sq_real)
           = 2r² − 2⟪u, v⟫
           = 2r² (1 − cos(oangle u v))    (inner_eq_norm_mul_norm_mul_cos_oangle)
           = 2r² (1 − cos(arcAngle p − arcAngle q))   (A0 + cos is even)
           = 4r² sin²((arcAngle p − arcAngle q).toReal / 2)   (half-angle)
           = (2r · |sin(…)|)²
```

The two sides are non-negative; squaring is injective on `[0, ∞)`
(`pow_left_inj₀`), so taking square roots closes the goal. Total proof ≈ 50
lines of straight-line algebra, no new axioms, no sorry. The cosine step needs
that `cos` on `Real.Angle` is symmetric (`Real.Angle.cos_neg`), which absorbs
the `oangle (q-center) (p-center)` vs `oangle (p-center) (q-center)` swap that
arises from A0's argument order.

The theorem `arcAngle_chord_length` is the headline export. Downstream
consumers (Lc1, Nivasch–Pach–Pinchasi–Zerbib L6, A3 monotonicity) read `dist p q` in terms of
`arcAngle` differences out of this lemma.

## A3 — Status and approach

A3 is the **strict monotonicity** of chord length in arc-angle difference. With
A2 in hand, the chord-length form reduces to the underlying analytic fact:

```
|θ₁.toReal| < |θ₂.toReal|  →  |sin(θ₁.toReal / 2)| < |sin(θ₂.toReal / 2)|
```

(for `θ₁, θ₂ : Real.Angle`). This file states both:

* `abs_sin_half_strict_mono` — the pure analytic statement above, decoupled
  from any geometric content. Useful in its own right (and reusable for any
  half-angle monotonicity argument on `Real.Angle`).
* `arcAngle_chord_length_strict_mono` — the chord-length form on a sphere: for
  `p, q₁, q₂` at distance `r > 0` from `center`, if the absolute arc-angle
  differences are strictly ordered (with `q₁` "closer" in arc angle), then the
  chord lengths are strictly ordered the same way.

**Proof key.** `Real.Angle.toReal` lands in `(-π, π]`, so the half `θ.toReal /
2` lands in `(-π/2, π/2]`. Inside this interval `|sin x| = sin |x|` (via
`Real.abs_sin_eq_sin_abs_of_abs_le_pi`), and `sin` is strictly monotone on
`[-π/2, π/2]` (via `Real.sin_lt_sin_of_lt_of_le_pi_div_two`). Combining these
gives strict monotonicity of `|sin(x/2)|` in `|x|` for `x ∈ (-π, π]`.

**Why we lift to `toReal`.** The scoping report (§5 A3) flagged risk
"`Real.Angle` arithmetic on the additive quotient". The cleanest avoidance is
to do all real-line monotonicity arguments after passing through
`Real.Angle.toReal`, exactly as in A2. No quotient arithmetic appears in the
A3 proofs — every step is on `ℝ` with `toReal` bounds supplied by
`Real.Angle.neg_pi_lt_toReal` and `Real.Angle.toReal_le_pi`.

**Deviation from the scoping report.** The report tentatively named the
analytic lemma `abs_sin_half_strict_mono` and the chord form
`arcAngle_chord_length_strict_mono`; both are retained. The hypothesis form is
`|θ₁.toReal| < |θ₂.toReal|` (rather than the report's symbolic
`0 ≤ |θ₁.toReal| < |θ₂.toReal| ≤ π`): the lower `0 ≤` is redundant (every
`abs` is non-negative) and the upper `≤ π` is automatic for any
`Real.Angle.toReal` value, so neither is a hypothesis. -/

open scoped EuclideanGeometry Real

namespace Problem97

/-- **arcAngle.** The angular position of `p` on a circle centered at `center`,
measured from the canonical first basis vector of `ℝ²` in the standard
counter-clockwise orientation. Returns a value in `Real.Angle = ℝ / 2πℤ` to
sidestep the `Complex.arg` branch cut.

At the apex itself (`p = center`) the chord vector is `0` and the convention
`Orientation.oangle _ 0 = 0` gives `arcAngle center center = 0`. See
`arcAngle_center_self`. -/
noncomputable def arcAngle (center p : ℝ²) : Real.Angle :=
  stdOrientation.oangle (EuclideanSpace.basisFun (Fin 2) ℝ 0) (p - center)









/- ### A1 — `OnArcOpposite` ↔ sign-product bridge

`OnArcOpposite vi vj vk v` is the algebraic chord-separation predicate
`signedArea2 v vj vk * signedArea2 vi vj vk ≤ 0` (closed-cap convention).
Geometrically this says `v` and `vi` are on opposite (closed) sides of the
chord `vj`—`vk`.

Pushing the sign through `signedArea2_sign_eq_oangle_sign` (twice) rewrites
each `signedArea2` as the sign of an oriented angle on the two chord vectors,
centered at the corresponding test point. A further `rw` with
`arcAngle_sub_arcAngle` (taking the test point itself as the arc-angle
center) restates the bridge as a sign equation on differences of arc-angles
centered at the test points.

No MEC center, radius, or cospherical hypothesis is used — A1 is a purely
chord-side fact about four points in the plane. See the "A1 — Status and
approach" section in this file's module docstring for why this differs from
the scoping report's tentative 3-angle predicate. -/





/- ### A2 — chord-length formula on a sphere

For `p`, `q` both at distance `r > 0` from `center`, the Euclidean distance
`dist p q` equals `2 r |sin(θ/2)|` where `θ = arcAngle center p - arcAngle
center q`. See the "A2 — Status and approach" section in this file's module
docstring for the proof sketch (polarization) and for why the right-hand-side
half-angle is taken on `θ.toReal` rather than directly on `θ : Real.Angle`. -/



/- ### A3 — strict monotonicity of chord length in arc-angle difference

The chord-length formula A2 reads `dist p q = 2 r |sin(θ.toReal / 2)|` with
`θ = arcAngle center p - arcAngle center q`. To prove strict monotonicity of
the chord length in the arc-angle difference, the central analytic fact is

```
|θ₁.toReal| < |θ₂.toReal|  →  |sin(θ₁.toReal / 2)| < |sin(θ₂.toReal / 2)|
```

We package this as `abs_sin_half_strict_mono` (independent of geometry) and
then derive `arcAngle_chord_length_strict_mono` as a one-`rw` corollary using
A2. See the "A3 — Status and approach" section in this file's module
docstring for the proof key. -/





/- ### A3-iff — equality and `<` iff forms of strict monotonicity

The strict-monotonicity A3 (`arcAngle_chord_length_strict_mono`) is one
direction of an iff. For the Dumitrescu Lc1 witness-pair argument we also
need the **equality** direction: two MEC-arc points equidistant from a fixed
third MEC-arc point have arc-angle differences equal in absolute value
(arc-symmetry about the apex). With the analytic core
`abs_sin_half_eq_iff` in hand both directions of the chord-length comparison
collapse to comparisons on `|θ.toReal|`.

The four lemmas in this block come in two layers:

* **Analytic layer** — `abs_sin_half_eq_iff`, `abs_sin_half_lt_iff`. Pure
  half-angle sine facts on `Real.Angle.toReal`, decoupled from geometry. The
  equality form uses `Real.injOn_sin` on `[-π/2, π/2]`; the strict form is
  the iff lift of `abs_sin_half_strict_mono`.
* **Geometric layer** — `arcAngle_chord_length_eq_iff`,
  `arcAngle_chord_length_lt_iff`. Chord-length forms on a sphere, obtained
  by composing A2 (`arcAngle_chord_length`) with the analytic layer.

Together with `arcAngle_chord_length_strict_mono` (the `→` direction of
`_lt_iff`), the chord-length forms give a clean trichotomy: under
`p, q₁, q₂` all at distance `r` from `center`, the chord-length comparison
between `dist p q₁` and `dist p q₂` matches the comparison between
`|(arcAngle center p - arcAngle center q₁).toReal|` and
`|(arcAngle center p - arcAngle center q₂).toReal|` in all three cases
(`<`, `=`, `>`).

**Use in Dumitrescu Lc1.** The `CapWitnessRanking` constructor needs to
exhibit an injection from `capWitnessPairs A C` into a Finset of size
`|C| - 1`. Each witness pair `xy = {x, y} ⊆ C` carries an apex `a ∈ A \ C`
with `dist a x = dist a y`. Under the MEC-arc-membership hypothesis (cap
points all lie on the MEC, apex on or inside the MEC), the equality form
gives `|(arcAngle center a - arcAngle center x).toReal|
   = |(arcAngle center a - arcAngle center y).toReal|`, i.e. `x` and `y`
are arc-symmetric about the diameter through `a`. This is the geometric
input to the diagonal-vertex injection that realizes the `|C| - 1` bound. -/









end Problem97