import Mathlib

/-!
# Problem 3: Two-stage stick cutting game

Lean 4 + Mathlib formalisation scaffold.

The elementary algebra relating the alternating gap to Liu's odd-position
share, and the closed-form simplification of the answer, are fully proved.
The two deep finite-combinatorial lemmas (subset-sum pairing upper bound and
binary-tree/multigraph lower bound) are stated with `sorry`.
-/

set_option autoImplicit false

namespace Problem3

/-- Alternating gap of a list already sorted in nonincreasing order. -/
def altGap : List ℝ → ℝ
  | [] => 0
  | [x] => x
  | x :: y :: xs => x - y + altGap xs

/-- Sum of entries in odd positions (positions 1,3,5,...). -/
def oddSum : List ℝ → ℝ
  | [] => 0
  | [x] => x
  | x :: _y :: xs => x + oddSum xs

/-- `sum + alternating gap = 2 × odd-position sum`. -/
theorem sum_add_altGap_eq_two_oddSum :
    ∀ xs : List ℝ, xs.sum + altGap xs = 2 * oddSum xs
  | [] => by simp [altGap, oddSum]
  | [x] => by simp [altGap, oddSum]
  | x :: y :: xs => by
      simp [altGap, oddSum, sum_add_altGap_eq_two_oddSum xs]
      ring

/-- Odd-position sum in terms of total mass and alternating gap. -/
theorem oddSum_eq_half_sum_add_gap (xs : List ℝ) :
    oddSum xs = (xs.sum + altGap xs) / 2 := by
  have h := sum_add_altGap_eq_two_oddSum xs
  linarith

/-- The small residual allowed by Xiang's subset-sum construction. -/
def delta (n : ℕ) : ℝ :=
  1 / ((2 : ℝ)^(n+1) - 1)

/-- Claimed minimax value before simplification. -/
def claimedValue (n : ℕ) : ℝ :=
  (1 + delta n) / 2

/-- Closed form of the answer. -/
theorem claimedValue_closed_form (n : ℕ) :
    claimedValue n = (2 : ℝ)^n / ((2 : ℝ)^(n+1) - 1) := by
  unfold claimedValue delta
  rw [pow_succ]
  have hden : (2 : ℝ)^n * 2 - 1 ≠ 0 := by positivity
  field_simp [hden]
  ring

/--
If all but residual mass `R` can be grouped into equal pairs, the second
player can secure one member of every pair, so the first player receives at
most `(total + R)/2`.
-/
theorem paired_mass_upper_bound
    (total residual firstShare : ℝ)
    (hbound : firstShare ≤ (total - residual) / 2 + residual) :
    firstShare ≤ (total + residual) / 2 := by
  linarith

/--
Subset-sum core of Xiang's upper bound. Among the `2^(n+1)` subset sums,
two distinct sums differ by at most `delta n`; deleting their common indices
gives disjoint subsets with nonempty symmetric difference.
-/
theorem disjoint_subset_close_sums
    (n : ℕ)
    (a : Fin (n+1) → ℝ)
    (hnonneg : ∀ i, 0 ≤ a i)
    (hsum : ∑ i, a i = 1) :
    ∃ P Q : Finset (Fin (n+1)),
      Disjoint P Q ∧
      (P ∪ Q).Nonempty ∧
      |(∑ i ∈ P, a i) - (∑ i ∈ Q, a i)| ≤ delta n := by
  sorry

/-- A finite sequence is written in nonincreasing order. -/
def IsDescending {m : ℕ} (x : Fin m → ℝ) : Prop :=
  ∀ i j, i.1 ≤ j.1 → x j ≤ x i

/--
Lower-bound combinatorial core.

The final pieces are indexed in nonincreasing order by `x`.  `origin j` records
which initial binary piece produced the final piece `j`.  The mass condition
says that the pieces of origin `i` sum to `2^i`.  If at most `n` extra cuts
were made, then `m ≤ 2n+1`, and the alternating gap is at least `1`.
-/
theorem binary_partition_altGap_lower_bound
    (n m : ℕ)
    (x : Fin m → ℝ)
    (origin : Fin m → Fin (n+1))
    (hxnonneg : ∀ j, 0 ≤ x j)
    (hxsorted : IsDescending x)
    (hm : m ≤ 2*n + 1)
    (hmass : ∀ i : Fin (n+1),
      (∑ j : Fin m, if origin j = i then x j else 0) =
        (2 : ℝ)^i.1) :
    1 ≤ altGap (List.ofFn x) := by
  sorry

/-- Once matching lower and upper bounds are available, the value is fixed. -/
theorem value_from_matching_bounds
    (n : ℕ) (v : ℝ)
    (hlower : claimedValue n ≤ v)
    (hupper : v ≤ claimedValue n) :
    v = (2 : ℝ)^n / ((2 : ℝ)^(n+1) - 1) := by
  have hv : v = claimedValue n := le_antisymm hupper hlower
  rw [hv, claimedValue_closed_form]

end Problem3
