import Erdos1135.Terras.Parity.Word

/-!
# Terras/Everett Branch Contraction

This module packages the local descent consequence of the cleared affine normal form for an
accelerated parity branch.
-/

namespace Erdos1135
namespace Terras

theorem branch_descends_of_contracting {k n : ℕ} {w : ParityWord k}
    (hprefix : parityPrefix k n = w)
    (_hcontract : 3 ^ numOdd w < 2 ^ k)
    (hconst : branchConst w < ((2 ^ k : ℤ) - ((3 : ℤ) ^ numOdd w)) * (n : ℤ)) :
    accelerated^[k] n < n := by
  have hmul_lt :
      (2 ^ k : ℤ) * (accelerated^[k] n : ℤ) < (2 ^ k : ℤ) * (n : ℤ) := by
    calc
      (2 ^ k : ℤ) * (accelerated^[k] n : ℤ)
          = ((3 : ℤ) ^ numOdd w) * (n : ℤ) + branchConst w :=
            affine_normal_form w hprefix
      _ < ((3 : ℤ) ^ numOdd w) * (n : ℤ) +
            (((2 ^ k : ℤ) - ((3 : ℤ) ^ numOdd w)) * (n : ℤ)) := by
            nlinarith [hconst]
      _ = (2 ^ k : ℤ) * (n : ℤ) := by
            ring
  have hpow_pos_int : (0 : ℤ) < (2 ^ k : ℤ) := by
    positivity
  have hint : (accelerated^[k] n : ℤ) < (n : ℤ) := by
    nlinarith [hmul_lt, hpow_pos_int]
  exact_mod_cast hint

def branchThreshold {k : ℕ} (w : ParityWord k) : ℕ :=
  Int.natAbs (branchConst w) + 1

def branchThresholdMax (k : ℕ) : ℕ :=
  Finset.univ.sup (fun w : ParityWord k => branchThreshold w)

theorem branchThreshold_le_branchThresholdMax {k : ℕ} (w : ParityWord k) :
    branchThreshold w ≤ branchThresholdMax k := by
  classical
  unfold branchThresholdMax
  exact Finset.le_sup (s := (Finset.univ : Finset (ParityWord k)))
    (f := fun w => branchThreshold w) (by simp)

theorem descends_of_contracting_of_branchThreshold_le {k n : ℕ} {w : ParityWord k}
    (hcontract : 3 ^ numOdd w < 2 ^ k)
    (hn : branchThreshold w ≤ n)
    (hprefix : parityPrefix k n = w) :
    accelerated^[k] n < n := by
  apply branch_descends_of_contracting hprefix hcontract
  let B : ℤ := (2 ^ k : ℤ) - ((3 : ℤ) ^ numOdd w)
  have hcoef_pos : (0 : ℤ) < B := by
    dsimp [B]
    have hcast : ((3 : ℤ) ^ numOdd w) < (2 : ℤ) ^ k := by
      exact_mod_cast hcontract
    omega
  have hcoef_ge_one : (1 : ℤ) ≤ B := by omega
  have hc_le_abs : branchConst w ≤ (Int.natAbs (branchConst w) : ℤ) := by
    simpa [Int.natCast_natAbs] using le_abs_self (branchConst w)
  have habs_lt_n_nat : Int.natAbs (branchConst w) < n := by
    unfold branchThreshold at hn
    omega
  have habs_lt_n : (Int.natAbs (branchConst w) : ℤ) < (n : ℤ) := by
    exact_mod_cast habs_lt_n_nat
  have hc_lt_n : branchConst w < (n : ℤ) := lt_of_le_of_lt hc_le_abs habs_lt_n
  have hn_nonneg : (0 : ℤ) ≤ n := by positivity
  have hn_le_Bn : (n : ℤ) ≤ B * (n : ℤ) := by nlinarith
  exact lt_of_lt_of_le hc_lt_n hn_le_Bn

theorem exists_large_descends_of_contracting {k : ℕ} (w : ParityWord k)
    (hcontract : 3 ^ numOdd w < 2 ^ k) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → parityPrefix k n = w → accelerated^[k] n < n := by
  exact ⟨branchThreshold w, fun n hn hprefix =>
    descends_of_contracting_of_branchThreshold_le hcontract hn hprefix⟩

theorem descends_of_contracting_of_branchThresholdMax_le {k n : ℕ} {w : ParityWord k}
    (hcontract : 3 ^ numOdd w < 2 ^ k)
    (hn : branchThresholdMax k ≤ n)
    (hprefix : parityPrefix k n = w) :
    accelerated^[k] n < n :=
  descends_of_contracting_of_branchThreshold_le hcontract
    ((branchThreshold_le_branchThresholdMax w).trans hn) hprefix

end Terras
end Erdos1135