import Mathlib open Finset abbrev putnam_2025_a5_solution : (n : ℕ) → Set (Fin n → ℤˣ) := fun n => {s | ∀ (i : Fin n), (h : i.val + 1 < n) → s ⟨i.val + 1, h⟩ = -s i} abbrev f (n : ℕ) (s : Fin n → ℤˣ) : ℕ := Finset.card {σ : Equiv.Perm (Fin (n + 1)) | ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))} noncomputable def F (n : ℕ) (s : Fin n → ℤˣ) (k : Fin (n + 1)) : ℕ := Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k} noncomputable def U (m : ℕ) (x : Fin m → ℕ) : Fin (m + 1) → ℕ := fun k => ∑ j : Fin m, if j.val < k.val then x j else 0 noncomputable def D (m : ℕ) (x : Fin m → ℕ) : Fin (m + 1) → ℕ := fun k => ∑ j : Fin m, if k.val ≤ j.val then x j else 0 def isAlternating (n : ℕ) (s : Fin n → ℤˣ) : Prop := ∀ (i : Fin n), (h : i.val + 1 < n) → s ⟨i.val + 1, h⟩ = -s i noncomputable def altSeqPlus (m : ℕ) : Fin m → ℤˣ := fun i => if (m - 1 - i.val) % 2 = 0 then 1 else -1 noncomputable def altSeqMinus (m : ℕ) : Fin m → ℤˣ := fun i => if (m - 1 - i.val) % 2 = 0 then -1 else 1 lemma f_eq_sum_F (n : ℕ) (s : Fin n → ℤˣ) : f n s = ∑ k : Fin (n + 1), F n s k := by classical unfold f F set S : Finset (Equiv.Perm (Fin (n + 1))) := Finset.univ.filter (fun σ => ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) set last : Equiv.Perm (Fin (n + 1)) → Fin (n + 1) := fun σ => σ ⟨n, Nat.lt_succ_self n⟩ have h := Finset.card_eq_sum_card_fiberwise (ι := Equiv.Perm (Fin (n + 1))) (M := Fin (n + 1)) (f := last) (s := S) (t := Finset.univ) (fun _ _ => Finset.mem_univ _) rw [h] apply Finset.sum_congr rfl intro k _ congr 1 ext σ simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_setOf_eq, S, last, and_comm] lemma penult_lt_of_last_sign_pos (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = 1) (σ : Equiv.Perm (Fin (n + 1))) (hvalid : ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) (k : Fin (n + 1)) (hσn : σ ⟨n, Nat.lt_succ_self n⟩ = k) : σ ⟨n - 1, by omega⟩ < k := by have hconstr := hvalid ⟨n - 1, by omega⟩ simp only [Fin.succ_mk, Fin.castSucc_mk] at hconstr have hn' : n - 1 + 1 = n := by omega simp only [hn'] at hconstr rw [hlast] at hconstr simp only [Units.val_one, one_mul] at hconstr rw [← hσn] have : (σ ⟨n - 1, by omega⟩ : ℤ) < (σ ⟨n, Nat.lt_succ_self n⟩ : ℤ) := by omega have hnat : (σ ⟨n - 1, by omega⟩).val < (σ ⟨n, Nat.lt_succ_self n⟩).val := by simp only [Fin.val_fin_lt] at this ⊢; omega exact hnat lemma perm_ne_last_at_earlier_pos (n : ℕ) (k : Fin (n + 1)) (σ : Equiv.Perm (Fin (n + 1))) (hσn : σ ⟨n, Nat.lt_succ_self n⟩ = k) (i : Fin n) : σ i.castSucc ≠ k := by intro hcontra have : σ i.castSucc = σ ⟨n, Nat.lt_succ_self n⟩ := by rw [hcontra, hσn] have hinj := σ.injective this simp only [Fin.castSucc_mk, Fin.ext_iff, Fin.coe_castSucc] at hinj have : i.val < n := i.isLt omega def compressK {n : ℕ} (k : Fin (n+1)) (i : Fin (n+1)) (h : i ≠ k) : Fin n := if hlt : i < k then i.castPred (Fin.ne_last_of_lt hlt) else i.pred (by intro hi0; rw [hi0] at h hlt; exact h (Fin.le_zero_iff.mp (not_lt.mp hlt)).symm) lemma succAbove_compressK {n : ℕ} (k : Fin (n+1)) (i : Fin (n+1)) (h : i ≠ k) : k.succAbove (compressK k i h) = i := by simp only [compressK]; split_ifs with hlt · exact Fin.succAbove_castPred_of_lt k i hlt · exact Fin.succAbove_pred_of_lt k i (lt_of_le_of_ne (not_lt.mp hlt) (Ne.symm h)) lemma compressK_succAbove {n : ℕ} (k : Fin (n+1)) (i : Fin n) : compressK k (k.succAbove i) (Fin.succAbove_ne k i) = i := by simp only [compressK] rcases k.castSucc_lt_or_lt_succ i with hcase | hcase · have h1 : k.succAbove i = i.castSucc := Fin.succAbove_of_castSucc_lt k i hcase simp only [h1, hcase, dite_true, Fin.castPred_castSucc] · have h1 : k.succAbove i = i.succ := Fin.succAbove_of_lt_succ k i hcase have h2 : ¬i.succ < k := not_lt.mpr (le_of_lt hcase) simp only [h1, h2, dite_false, Fin.pred_succ] lemma compressK_of_lt {n : ℕ} (k : Fin (n+1)) (i : Fin (n+1)) (h : i ≠ k) (hlt : i < k) : (compressK k i h).val = i.val := by simp only [compressK, hlt, dite_true, Fin.coe_castPred] lemma compressK_of_gt {n : ℕ} (k : Fin (n+1)) (i : Fin (n+1)) (h : i ≠ k) (hgt : k < i) : (compressK k i h).val = i.val - 1 := by simp only [compressK, not_lt.mpr (le_of_lt hgt), dite_false, Fin.coe_pred] lemma perm_inv_succAbove_lt {n : ℕ} (k : Fin (n+1)) (σ : Equiv.Perm (Fin (n+1))) (hσk : σ ⟨n, Nat.lt_succ_self n⟩ = k) (j : Fin n) : (σ.symm (k.succAbove j)).val < n := by by_cases h : (σ.symm (k.succAbove j)).val < n · exact h · exfalso push_neg at h have hbound := (σ.symm (k.succAbove j)).isLt have heq : (σ.symm (k.succAbove j)).val = n := by omega have hfinEq : σ.symm (k.succAbove j) = ⟨n, Nat.lt_succ_self n⟩ := Fin.ext heq have happly := σ.apply_symm_apply (k.succAbove j) rw [hfinEq, hσk] at happly exact Fin.succAbove_ne k j happly.symm noncomputable def compressPerm {n : ℕ} (k : Fin (n+1)) (σ : Equiv.Perm (Fin (n+1))) (hσk : σ ⟨n, Nat.lt_succ_self n⟩ = k) : Equiv.Perm (Fin n) where toFun i := compressK k (σ i.castSucc) (perm_ne_last_at_earlier_pos n k σ hσk i) invFun j := ⟨(σ.symm (k.succAbove j)).val, perm_inv_succAbove_lt k σ hσk j⟩ left_inv i := by simp only have h1 := succAbove_compressK k (σ i.castSucc) (perm_ne_last_at_earlier_pos n k σ hσk i) have h2 := σ.symm_apply_apply i.castSucc ext simp only [Fin.coe_castSucc] calc (σ.symm (k.succAbove (compressK k (σ i.castSucc) _))).val = (σ.symm (σ i.castSucc)).val := by simp only [h1] _ = i.castSucc.val := by simp only [h2] _ = i.val := rfl right_inv j := by simp only let preimg : Fin n := ⟨(σ.symm (k.succAbove j)).val, perm_inv_succAbove_lt k σ hσk j⟩ have hcast : preimg.castSucc = σ.symm (k.succAbove j) := Fin.ext rfl have hσpreimg : σ preimg.castSucc = k.succAbove j := by rw [hcast]; exact σ.apply_symm_apply (k.succAbove j) have step1 : compressK k (σ preimg.castSucc) (perm_ne_last_at_earlier_pos n k σ hσk preimg) = compressK k (k.succAbove j) (Fin.succAbove_ne k j) := by simp only [hσpreimg] rw [step1, compressK_succAbove] noncomputable def expandPerm {n : ℕ} (k : Fin (n+1)) (τ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n+1)) where toFun i := if h : i = ⟨n, Nat.lt_succ_self n⟩ then k else k.succAbove (τ ⟨i.val, by have hi := i.isLt have hne : i.val ≠ n := fun heq => h (Fin.ext heq) omega⟩) invFun j := if h : j = k then ⟨n, Nat.lt_succ_self n⟩ else (τ.symm (compressK k j h)).castSucc left_inv i := by dsimp only split_ifs with hi hk hk · exact hi.symm · exfalso; exact hk rfl · exfalso have hcontra : k.succAbove (τ ⟨i.val, by have hi' := i.isLt have hne : i.val ≠ n := fun heq => hi (Fin.ext heq) omega⟩) = k := hk exact Fin.succAbove_ne k _ hcontra · rw [compressK_succAbove] ext rw [Fin.coe_castSucc, Fin.val_mk] have hsymm := τ.symm_apply_apply ⟨i.val, by have hi' := i.isLt have hne : i.val ≠ n := fun heq => hi (Fin.ext heq) omega⟩ simp only [Fin.ext_iff, Fin.val_mk] at hsymm exact hsymm right_inv j := by dsimp only split_ifs with hj hi hi · exact hj.symm · exfalso; exact hi rfl · exfalso have hcast_eq : ((τ.symm (compressK k j hj)).castSucc) = ⟨n, Nat.lt_succ_self n⟩ := hi have hval_eq : (τ.symm (compressK k j hj)).val = n := by simp only [Fin.ext_iff, Fin.coe_castSucc] at hcast_eq exact hcast_eq have hbound := (τ.symm (compressK k j hj)).isLt omega · have hval_lt : (τ.symm (compressK k j hj)).val < n := (τ.symm (compressK k j hj)).isLt have hfin_eq : (⟨(τ.symm (compressK k j hj)).castSucc.val, by rw [Fin.coe_castSucc]; exact hval_lt⟩ : Fin n) = τ.symm (compressK k j hj) := by ext; simp [Fin.coe_castSucc] rw [hfin_eq, τ.apply_symm_apply, succAbove_compressK] lemma expandPerm_at_n {n : ℕ} (k : Fin (n+1)) (τ : Equiv.Perm (Fin n)) : (expandPerm k τ) ⟨n, Nat.lt_succ_self n⟩ = k := by show (expandPerm k τ).toFun ⟨n, Nat.lt_succ_self n⟩ = k simp only [expandPerm, dite_eq_ite, ite_true, dite_true] lemma compressPerm_expandPerm {n : ℕ} (k : Fin (n+1)) (τ : Equiv.Perm (Fin n)) : compressPerm k (expandPerm k τ) (expandPerm_at_n k τ) = τ := by apply Equiv.ext intro i have hi : i.castSucc ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro heq simp only [Fin.ext_iff, Fin.coe_castSucc] at heq exact absurd heq (Nat.ne_of_lt i.isLt) have hlt : i.castSucc.val < n := by simp_all [Fin.coe_castSucc] have hne : (expandPerm k τ) i.castSucc ≠ k := by have h := perm_ne_last_at_earlier_pos n k (expandPerm k τ) (expandPerm_at_n k τ) i exact h show compressK k ((expandPerm k τ) i.castSucc) hne = τ i have hexpand : (expandPerm k τ) i.castSucc = k.succAbove (τ ⟨i.castSucc.val, hlt⟩) := by show (expandPerm k τ).toFun i.castSucc = _ simp only [expandPerm, hi, dite_false] have hval_eq : (⟨i.castSucc.val, hlt⟩ : Fin n) = i := by ext; simp [Fin.coe_castSucc] have hrewr : k.succAbove (τ ⟨i.castSucc.val, hlt⟩) = k.succAbove (τ i) := by rw [hval_eq] have hexpand' : (expandPerm k τ) i.castSucc = k.succAbove (τ i) := by rw [hexpand, hrewr] have hne2 : k.succAbove (τ i) ≠ k := Fin.succAbove_ne k (τ i) calc compressK k ((expandPerm k τ) i.castSucc) hne = compressK k (k.succAbove (τ i)) hne2 := by simp only [hexpand'] _ = τ i := compressK_succAbove k (τ i) lemma expandPerm_compressPerm {n : ℕ} (k : Fin (n+1)) (σ : Equiv.Perm (Fin (n+1))) (hσk : σ ⟨n, Nat.lt_succ_self n⟩ = k) : expandPerm k (compressPerm k σ hσk) = σ := by apply Equiv.ext intro i show (expandPerm k (compressPerm k σ hσk)).toFun i = σ i by_cases hi : i = ⟨n, Nat.lt_succ_self n⟩ · subst hi simp only [expandPerm, dite_true] exact hσk.symm · have hval_lt : i.val < n := by have := i.isLt have hne : i.val ≠ n := fun heq => hi (Fin.ext heq) omega simp only [expandPerm, hi, dite_false] have heq : (⟨i.val, hval_lt⟩ : Fin n).castSucc = i := Fin.ext rfl have hσne : σ (⟨i.val, hval_lt⟩ : Fin n).castSucc ≠ k := perm_ne_last_at_earlier_pos n k σ hσk ⟨i.val, hval_lt⟩ calc k.succAbove ((compressPerm k σ hσk) ⟨i.val, hval_lt⟩) = k.succAbove (compressK k (σ (⟨i.val, hval_lt⟩ : Fin n).castSucc) hσne) := rfl _ = σ (⟨i.val, hval_lt⟩ : Fin n).castSucc := succAbove_compressK k (σ (⟨i.val, hval_lt⟩ : Fin n).castSucc) hσne _ = σ i := by rw [heq] lemma compressK_strictMono {n : ℕ} (k : Fin (n+1)) (a b : Fin (n+1)) (ha : a ≠ k) (hb : b ≠ k) (hab : a < b) : compressK k a ha < compressK k b hb := by rcases lt_trichotomy a k with halt | heq | hagt · rcases lt_trichotomy b k with hblt | hbeq | hbgt · rw [Fin.lt_iff_val_lt_val, compressK_of_lt k a ha halt, compressK_of_lt k b hb hblt] exact hab · exact absurd hbeq hb · rw [Fin.lt_iff_val_lt_val, compressK_of_lt k a ha halt, compressK_of_gt k b hb hbgt] have hk_lt_b : k.val < b.val := hbgt have ha_lt_k : a.val < k.val := halt omega · exact absurd heq ha · have hbgt : k < b := lt_trans hagt hab rw [Fin.lt_iff_val_lt_val, compressK_of_gt k a ha hagt, compressK_of_gt k b hb hbgt] have ha_pos : k.val < a.val := hagt have hb_pos : k.val < b.val := hbgt have hab_val : a.val < b.val := hab omega lemma sign_constraint_preserved_compress {n : ℕ} (s : Fin n → ℤˣ) (k : Fin (n+1)) (σ : Equiv.Perm (Fin (n+1))) (hσk : σ ⟨n, Nat.lt_succ_self n⟩ = k) (hvalid : ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) (i : Fin (n - 1)) (hn : 1 ≤ n) : 0 < (s ⟨i.val, by omega⟩ : ℤ) * (((compressPerm k σ hσk) ⟨i.val + 1, by omega⟩ : ℤ) - ((compressPerm k σ hσk) ⟨i.val, by omega⟩ : ℤ)) := by have hi_lt_n : i.val < n := by have := i.isLt; omega have hi_succ_lt_n : i.val + 1 < n := by have := i.isLt; omega have horiginal := hvalid ⟨i.val, hi_lt_n⟩ let idx0 : Fin (n+1) := ⟨i.val, by omega⟩ let idx1 : Fin (n+1) := ⟨i.val + 1, by omega⟩ have hidx0_cast : idx0 = (⟨i.val, hi_lt_n⟩ : Fin n).castSucc := rfl have hidx1_succ : idx1 = (⟨i.val, hi_lt_n⟩ : Fin n).succ := by ext; simp [Fin.succ, idx1] have hσ0_ne : σ idx0 ≠ k := perm_ne_last_at_earlier_pos n k σ hσk ⟨i.val, hi_lt_n⟩ have hσ1_ne : σ idx1 ≠ k := by have : idx1 = (⟨i.val + 1, hi_succ_lt_n⟩ : Fin n).castSucc := rfl exact perm_ne_last_at_earlier_pos n k σ hσk ⟨i.val + 1, hi_succ_lt_n⟩ have hcomp0 : (compressPerm k σ hσk) ⟨i.val, by omega⟩ = compressK k (σ idx0) hσ0_ne := by show (compressPerm k σ hσk).toFun ⟨i.val, by omega⟩ = _ simp only [compressPerm, idx0] congr 1 have hcomp1 : (compressPerm k σ hσk) ⟨i.val + 1, by omega⟩ = compressK k (σ idx1) hσ1_ne := by show (compressPerm k σ hσk).toFun ⟨i.val + 1, by omega⟩ = _ simp only [compressPerm, idx1] congr 1 rw [hcomp0, hcomp1] have hidx0_eq : idx0 = (⟨i.val, hi_lt_n⟩ : Fin n).castSucc := by ext; simp [idx0, Fin.coe_castSucc] have hidx1_eq : idx1 = (⟨i.val, hi_lt_n⟩ : Fin n).succ := by ext; simp [idx1, Fin.val_succ] have horiginal' : 0 < (s ⟨i.val, hi_lt_n⟩ : ℤ) * ((σ idx1 : ℤ) - (σ idx0 : ℤ)) := by simp only [hidx0_eq, hidx1_eq]; exact horiginal rcases Int.units_eq_one_or (s ⟨i.val, hi_lt_n⟩) with hs | hs · simp only [hs, Units.val_one, one_mul] at horiginal' ⊢ have hσ_lt : σ idx0 < σ idx1 := by have h := Int.sub_pos.mp horiginal' rw [Fin.lt_iff_val_lt_val] omega have hcomp_lt := compressK_strictMono k (σ idx0) (σ idx1) hσ0_ne hσ1_ne hσ_lt have hcomp_lt' := Fin.lt_iff_val_lt_val.mp hcomp_lt omega · simp only [hs, Units.val_neg, Units.val_one] at horiginal' ⊢ have hσ_lt : σ idx1 < σ idx0 := by have h : (σ idx1 : ℤ) - (σ idx0 : ℤ) < 0 := by linarith rw [Fin.lt_iff_val_lt_val] omega have hcomp_lt := compressK_strictMono k (σ idx1) (σ idx0) hσ1_ne hσ0_ne hσ_lt have hcomp_lt' := Fin.lt_iff_val_lt_val.mp hcomp_lt linarith lemma sign_constraint_preserved_expand {n : ℕ} (s : Fin n → ℤˣ) (k : Fin (n+1)) (τ : Equiv.Perm (Fin n)) (hn : 1 ≤ n) (hvalid : ∀ i : Fin (n - 1), 0 < (s ⟨i.val, by omega⟩ : ℤ) * ((τ ⟨i.val + 1, by omega⟩ : ℤ) - (τ ⟨i.val, by omega⟩ : ℤ))) (i : Fin (n - 1)) : 0 < (s ⟨i.val, by omega⟩ : ℤ) * (((expandPerm k τ) ⟨i.val + 1, by omega⟩ : ℤ) - ((expandPerm k τ) ⟨i.val, by omega⟩ : ℤ)) := by have hi_lt_n : i.val < n := by have := i.isLt; omega have hi_succ_lt_n : i.val + 1 < n := by have := i.isLt; omega have horiginal := hvalid i let idx0 : Fin (n+1) := ⟨i.val, by omega⟩ let idx1 : Fin (n+1) := ⟨i.val + 1, by omega⟩ have hne0 : idx0 ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro h; simp only [Fin.ext_iff, Fin.val_mk] at h exact Nat.ne_of_lt hi_lt_n h have hne1 : idx1 ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro h; simp only [Fin.ext_iff, Fin.val_mk] at h exact Nat.ne_of_lt hi_succ_lt_n h have hexp0 : (expandPerm k τ) idx0 = k.succAbove (τ ⟨i.val, hi_lt_n⟩) := by show (expandPerm k τ).toFun idx0 = _ simp only [expandPerm, hne0, dite_false] congr 1 have hexp1 : (expandPerm k τ) idx1 = k.succAbove (τ ⟨i.val + 1, hi_succ_lt_n⟩) := by show (expandPerm k τ).toFun idx1 = _ simp only [expandPerm, hne1, dite_false] congr 1 rw [hexp0, hexp1] have horiginal' : 0 < (s ⟨i.val, hi_lt_n⟩ : ℤ) * ((τ ⟨i.val + 1, hi_succ_lt_n⟩ : ℤ) - (τ ⟨i.val, hi_lt_n⟩ : ℤ)) := horiginal rcases Int.units_eq_one_or (s ⟨i.val, hi_lt_n⟩) with hs | hs · simp only [hs, Units.val_one, one_mul] at horiginal' ⊢ have hτ_lt : τ ⟨i.val, hi_lt_n⟩ < τ ⟨i.val + 1, hi_succ_lt_n⟩ := by have h := Int.sub_pos.mp horiginal' rw [Fin.lt_iff_val_lt_val] omega have hsucc_lt := (Fin.succAbove_lt_succAbove_iff (p := k)).mpr hτ_lt have hsucc_lt' := Fin.lt_iff_val_lt_val.mp hsucc_lt omega · simp only [hs, Units.val_neg, Units.val_one] at horiginal' ⊢ have hτ_lt : τ ⟨i.val + 1, hi_succ_lt_n⟩ < τ ⟨i.val, hi_lt_n⟩ := by have h : (τ ⟨i.val + 1, hi_succ_lt_n⟩ : ℤ) - (τ ⟨i.val, hi_lt_n⟩ : ℤ) < 0 := by linarith rw [Fin.lt_iff_val_lt_val] omega have hsucc_lt := (Fin.succAbove_lt_succAbove_iff (p := k)).mpr hτ_lt have hsucc_lt' := Fin.lt_iff_val_lt_val.mp hsucc_lt linarith lemma last_constraint_expand {n : ℕ} (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = 1) (k : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) (j : Fin n) (hj : j.val < k.val) (hτlast : τ ⟨n - 1, by omega⟩ = j) : 0 < (s ⟨n - 1, by omega⟩ : ℤ) * (((expandPerm k τ) ⟨n, Nat.lt_succ_self n⟩ : ℤ) - ((expandPerm k τ) ⟨n - 1, by omega⟩ : ℤ)) := by have h1 : (expandPerm k τ) ⟨n, Nat.lt_succ_self n⟩ = k := expandPerm_at_n k τ have hne : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro heq; simp only [Fin.ext_iff] at heq; omega have h2 : (expandPerm k τ) ⟨n - 1, by omega⟩ = k.succAbove (τ ⟨n - 1, by omega⟩) := by show (expandPerm k τ).toFun ⟨n - 1, by omega⟩ = _ simp only [expandPerm, hne, dite_false] have hj_cast : j.castSucc < k := by simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc] exact hj have h3 : k.succAbove j = j.castSucc := Fin.succAbove_of_castSucc_lt k j hj_cast rw [hτlast, h3] at h2 simp only [hlast, h1, h2, Units.val_one, one_mul, Fin.coe_castSucc] have hk_bound := k.isLt have hj_bound := j.isLt omega lemma fiber_card_eq (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = 1) (k : Fin (n + 1)) (j : Fin n) (hj : j.val < k.val) : Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩} = F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ := by classical unfold F have hn_eq : n - 1 + 1 = n := by omega set Source := {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩}.toFinset set s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ set j' : Fin ((n - 1) + 1) := ⟨j.val, by have := j.isLt; omega⟩ have heq : (n - 1) + 1 = n := hn_eq let finCast : Fin ((n - 1) + 1) ≃ Fin n := (Fin.castOrderIso heq).toEquiv let castPermTo : Equiv.Perm (Fin n) → Equiv.Perm (Fin ((n - 1) + 1)) := fun τ => Equiv.permCongr finCast.symm τ let castPermFrom : Equiv.Perm (Fin ((n - 1) + 1)) → Equiv.Perm (Fin n) := fun τ => Equiv.permCongr finCast τ let fwd : Equiv.Perm (Fin (n + 1)) → Equiv.Perm (Fin ((n - 1) + 1)) := fun σ => if h : σ ⟨n, Nat.lt_succ_self n⟩ = k then castPermTo (compressPerm k σ h) else 1 let bwd : Equiv.Perm (Fin ((n - 1) + 1)) → Equiv.Perm (Fin (n + 1)) := fun τ => expandPerm k (castPermFrom τ) apply Finset.card_nbij' fwd bwd · intro σ hσ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hσ ⊢ obtain ⟨hvalid, hσk, hσj⟩ := hσ simp only [fwd, hσk, dite_true] constructor · intro i have hconstr := sign_constraint_preserved_compress s k σ hσk hvalid i hn simp only [castPermTo, Equiv.permCongr_apply, Equiv.symm_symm] have h1 : finCast i.succ = ⟨i.val + 1, by omega⟩ := by ext; simp [finCast, Fin.succ] have h2 : finCast i.castSucc = ⟨i.val, by omega⟩ := by ext; simp [finCast, Fin.castSucc] rw [h1, h2] convert hconstr using 2 · simp only [castPermTo, Equiv.permCongr_apply, Equiv.symm_symm] have hcomp_last : (compressPerm k σ hσk) ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩ := by show (compressPerm k σ hσk).toFun ⟨n - 1, by omega⟩ = _ simp only [compressPerm] have hσ_ne : σ (⟨n - 1, by omega⟩ : Fin n).castSucc ≠ k := perm_ne_last_at_earlier_pos n k σ hσk ⟨n - 1, by omega⟩ have hσ_cast : (⟨n - 1, by omega⟩ : Fin n).castSucc = ⟨n - 1, by omega⟩ := rfl have hσ_val : σ ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩ := hσj rw [hσ_cast] at hσ_ne have hj_lt_k : (⟨j.val, by omega⟩ : Fin (n + 1)) < k := by simp only [Fin.lt_iff_val_lt_val, Fin.val_mk]; exact hj have hcompress : compressK k ⟨j.val, by omega⟩ (Fin.ne_of_lt hj_lt_k) = ⟨j.val, by omega⟩ := by ext; rw [compressK_of_lt]; exact hj have hcomp_eq : compressK k (σ (⟨n - 1, by omega⟩ : Fin n).castSucc) hσ_ne = compressK k ⟨j.val, by omega⟩ (Fin.ne_of_lt hj_lt_k) := by have heq : σ (⟨n - 1, by omega⟩ : Fin n).castSucc = ⟨j.val, by omega⟩ := by rw [hσ_cast]; exact hσ_val simp only [heq, compressK] rw [hcomp_eq, hcompress] have hcast_eq : finCast ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hcomp_last] simp only [j', Fin.ext_iff, finCast] simp · intro τ hτ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hτ ⊢ obtain ⟨hvalid, hτlast⟩ := hτ simp only [bwd] let τ' : Equiv.Perm (Fin n) := castPermFrom τ refine ⟨?_, expandPerm_at_n k τ', ?_⟩ · intro i have hi_lt : i.val < n := i.isLt by_cases hi_last : i.val < n - 1 · have hvalid' : ∀ i' : Fin (n - 1), 0 < (s ⟨i'.val, by omega⟩ : ℤ) * ((τ' ⟨i'.val + 1, by omega⟩ : ℤ) - (τ' ⟨i'.val, by omega⟩ : ℤ)) := by intro i' have hi'_constr := hvalid i' simp only [s', castPermFrom, τ', Equiv.permCongr_apply] at hi'_constr ⊢ have hcast_succ : finCast.symm ⟨i'.val + 1, by omega⟩ = i'.succ := by ext; simp [finCast, Fin.succ] have hcast_castSucc : finCast.symm ⟨i'.val, by omega⟩ = i'.castSucc := by ext; simp [finCast, Fin.castSucc] rw [hcast_succ, hcast_castSucc] convert hi'_constr using 2 have hexpand := sign_constraint_preserved_expand s k τ' hn hvalid' ⟨i.val, hi_last⟩ convert hexpand using 2 · have hi_eq : i.val = n - 1 := by omega have hi_fin_eq : i = ⟨n - 1, by omega⟩ := Fin.ext hi_eq rw [hi_fin_eq] simp only [Fin.succ_mk, Fin.castSucc_mk] have hn' : n - 1 + 1 = n := by omega simp only [hn'] have hτ'_last : τ' ⟨n - 1, by omega⟩ = j := by simp only [τ', castPermFrom, Equiv.permCongr_apply] have hcast_eq : finCast.symm ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hτlast] simp only [j', finCast, Fin.ext_iff]; rfl exact last_constraint_expand hn s hlast k τ' j hj hτ'_last · show (expandPerm k τ') ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩ simp only [expandPerm] have hne : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro h; simp only [Fin.ext_iff] at h; omega have hτ'_last : τ' ⟨n - 1, by omega⟩ = j := by simp only [τ', castPermFrom, Equiv.permCongr_apply] have hcast_eq : finCast.symm ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hτlast] simp only [j', finCast, Fin.ext_iff]; rfl have hj_cast : j.castSucc < k := by simp [Fin.lt_iff_val_lt_val]; exact hj have hsuccAbove : k.succAbove j = j.castSucc := Fin.succAbove_of_castSucc_lt k j hj_cast have hne_val : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by simp only [ne_eq, Fin.ext_iff, Fin.val_mk]; omega simp only [Equiv.coe_fn_mk, hne_val, ↓reduceDIte, hτ'_last, hsuccAbove] rfl · intro σ hσ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hσ obtain ⟨hvalid, hσk, hσj⟩ := hσ simp only [fwd, bwd, hσk, dite_true] have hcast_inv : castPermFrom (castPermTo (compressPerm k σ hσk)) = compressPerm k σ hσk := by simp only [castPermFrom, castPermTo] ext x simp only [Equiv.permCongr_apply, Equiv.symm_symm] simp [finCast] rw [hcast_inv] exact expandPerm_compressPerm k σ hσk · intro τ hτ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hτ simp only [fwd, bwd] let τ' : Equiv.Perm (Fin n) := castPermFrom τ have hexpand_k : (expandPerm k τ') ⟨n, Nat.lt_succ_self n⟩ = k := expandPerm_at_n k τ' rw [dif_pos hexpand_k] have hcomp_expand : compressPerm k (expandPerm k τ') hexpand_k = τ' := compressPerm_expandPerm k τ' rw [hcomp_expand] simp only [castPermTo, castPermFrom, τ'] ext x simp only [Equiv.permCongr_apply, Equiv.symm_symm] simp [finCast] lemma F_recurrence_plus (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = 1) : ∀ k : Fin (n + 1), F n s k = U n (fun j : Fin n => F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k := by intro k classical unfold F U let s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ let S : Finset (Equiv.Perm (Fin (n + 1))) := Finset.univ.filter fun σ => (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k have hLHS : Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k} = S.card := by rfl rw [hLHS] let proj : Equiv.Perm (Fin (n + 1)) → Fin (n + 1) := fun σ => σ ⟨n - 1, by omega⟩ have h_partition : S.card = ∑ j : Fin (n + 1), (S.filter (fun σ => proj σ = j)).card := by rw [← Finset.card_eq_sum_card_fiberwise (f := proj) (t := Finset.univ)] intro _ _ exact Finset.mem_univ _ rw [h_partition] have h_fiber_empty : ∀ j : Fin (n + 1), ¬(j.val < k.val) → (S.filter (fun σ => proj σ = j)).card = 0 := by intro j hjk rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] intro σ hσ simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hσ obtain ⟨hvalid, hσk⟩ := hσ intro hproj have hpenult := penult_lt_of_last_sign_pos n hn s hlast σ hvalid k hσk simp only [proj] at hproj rw [hproj] at hpenult omega have h_last_empty : (S.filter (fun σ => proj σ = ⟨n, Nat.lt_succ_self n⟩)).card = 0 := by apply h_fiber_empty have hk_bound := k.isLt simp only [Fin.val_mk] omega have h_sum_split : ∑ j : Fin (n + 1), (S.filter (fun σ => proj σ = j)).card = ∑ j : Fin n, (S.filter (fun σ => proj σ = j.castSucc)).card + (S.filter (fun σ => proj σ = Fin.last n)).card := Fin.sum_univ_castSucc _ rw [h_sum_split] have h_fin_last : Fin.last n = ⟨n, Nat.lt_succ_self n⟩ := rfl rw [h_fin_last, h_last_empty, add_zero] apply Finset.sum_congr rfl intro j _ by_cases hjk : j.val < k.val · simp only [hjk, ↓reduceIte] have hfiber_eq : (S.filter (fun σ => proj σ = j.castSucc)).card = Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩} := by congr 1 ext σ simp only [S, Finset.mem_filter, Finset.mem_univ, true_and, proj, Set.mem_setOf_eq, Fin.castSucc_mk, Fin.ext_iff, Fin.val_mk] constructor · intro ⟨⟨hvalid, hσk⟩, hproj⟩ exact ⟨hvalid, hσk, hproj⟩ · intro ⟨hvalid, hσk, hσj⟩ exact ⟨⟨hvalid, hσk⟩, hσj⟩ rw [hfiber_eq] exact fiber_card_eq n hn s hlast k j hjk · simp only [hjk, ↓reduceIte] have hcast : j.castSucc.val = j.val := Fin.coe_castSucc j have : ¬(j.castSucc.val < k.val) := by rw [hcast]; exact hjk exact h_fiber_empty j.castSucc this lemma penult_gt_of_last_sign_neg (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = -1) (σ : Equiv.Perm (Fin (n + 1))) (hvalid : ∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) (k : Fin (n + 1)) (hσn : σ ⟨n, Nat.lt_succ_self n⟩ = k) : k < σ ⟨n - 1, by omega⟩ := by have hconstr := hvalid ⟨n - 1, by omega⟩ simp only [Fin.succ_mk, Fin.castSucc_mk] at hconstr have hn' : n - 1 + 1 = n := by omega simp only [hn'] at hconstr rw [hlast] at hconstr simp only [Units.val_neg, Units.val_one, neg_one_mul] at hconstr rw [← hσn] have : (σ ⟨n, Nat.lt_succ_self n⟩ : ℤ) < (σ ⟨n - 1, by omega⟩ : ℤ) := by omega have hnat : (σ ⟨n, Nat.lt_succ_self n⟩).val < (σ ⟨n - 1, by omega⟩).val := by simp only [Fin.val_fin_lt] at this ⊢; omega exact hnat lemma last_constraint_expand_neg {n : ℕ} (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = -1) (k : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) (j : Fin n) (hj : k.val ≤ j.val) (hτlast : τ ⟨n - 1, by omega⟩ = j) : 0 < (s ⟨n - 1, by omega⟩ : ℤ) * (((expandPerm k τ) ⟨n, Nat.lt_succ_self n⟩ : ℤ) - ((expandPerm k τ) ⟨n - 1, by omega⟩ : ℤ)) := by have h1 : (expandPerm k τ) ⟨n, Nat.lt_succ_self n⟩ = k := expandPerm_at_n k τ have hne : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro heq; simp only [Fin.ext_iff] at heq; omega have h2 : (expandPerm k τ) ⟨n - 1, by omega⟩ = k.succAbove (τ ⟨n - 1, by omega⟩) := by show (expandPerm k τ).toFun ⟨n - 1, by omega⟩ = _ simp only [expandPerm, hne, dite_false] have hj_cast : ¬(j.castSucc < k) := by simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, not_lt] exact hj have h3 : k.succAbove j = j.succ := Fin.succAbove_of_le_castSucc k j (not_lt.mp hj_cast) rw [hτlast, h3] at h2 simp only [hlast, h1, h2, Units.val_neg, Units.val_one, neg_one_mul, Fin.val_succ] have hk_bound := k.isLt have hj_bound := j.isLt omega lemma fiber_card_eq_minus (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = -1) (k : Fin (n + 1)) (j : Fin n) (hj : k.val ≤ j.val) : Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val + 1, by omega⟩} = F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ := by classical unfold F have hn_eq : n - 1 + 1 = n := by omega set Source := {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val + 1, by omega⟩}.toFinset set s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ set j' : Fin ((n - 1) + 1) := ⟨j.val, by have := j.isLt; omega⟩ have heq : (n - 1) + 1 = n := hn_eq let finCast : Fin ((n - 1) + 1) ≃ Fin n := (Fin.castOrderIso heq).toEquiv let castPermTo : Equiv.Perm (Fin n) → Equiv.Perm (Fin ((n - 1) + 1)) := fun τ => Equiv.permCongr finCast.symm τ let castPermFrom : Equiv.Perm (Fin ((n - 1) + 1)) → Equiv.Perm (Fin n) := fun τ => Equiv.permCongr finCast τ let fwd : Equiv.Perm (Fin (n + 1)) → Equiv.Perm (Fin ((n - 1) + 1)) := fun σ => if h : σ ⟨n, Nat.lt_succ_self n⟩ = k then castPermTo (compressPerm k σ h) else 1 let bwd : Equiv.Perm (Fin ((n - 1) + 1)) → Equiv.Perm (Fin (n + 1)) := fun τ => expandPerm k (castPermFrom τ) apply Finset.card_nbij' fwd bwd · intro σ hσ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hσ ⊢ obtain ⟨hvalid, hσk, hσj⟩ := hσ simp only [fwd, hσk, dite_true] constructor · intro i have hconstr := sign_constraint_preserved_compress s k σ hσk hvalid i hn simp only [castPermTo, Equiv.permCongr_apply, Equiv.symm_symm] have h1 : finCast i.succ = ⟨i.val + 1, by omega⟩ := by ext; simp [finCast, Fin.succ] have h2 : finCast i.castSucc = ⟨i.val, by omega⟩ := by ext; simp [finCast, Fin.castSucc] rw [h1, h2] convert hconstr using 2 · simp only [castPermTo, Equiv.permCongr_apply, Equiv.symm_symm] have hcomp_last : (compressPerm k σ hσk) ⟨n - 1, by omega⟩ = ⟨j.val, by omega⟩ := by show (compressPerm k σ hσk).toFun ⟨n - 1, by omega⟩ = _ simp only [compressPerm] have hσ_ne : σ (⟨n - 1, by omega⟩ : Fin n).castSucc ≠ k := perm_ne_last_at_earlier_pos n k σ hσk ⟨n - 1, by omega⟩ have hσ_cast : (⟨n - 1, by omega⟩ : Fin n).castSucc = ⟨n - 1, by omega⟩ := rfl have hσ_val : σ ⟨n - 1, by omega⟩ = ⟨j.val + 1, by omega⟩ := hσj rw [hσ_cast] at hσ_ne have hj_gt_k : k < (⟨j.val + 1, by omega⟩ : Fin (n + 1)) := by simp only [Fin.lt_iff_val_lt_val, Fin.val_mk] omega have hcompress : compressK k ⟨j.val + 1, by omega⟩ (Fin.ne_of_gt hj_gt_k) = ⟨j.val, by omega⟩ := by ext rw [compressK_of_gt] · simp · exact hj_gt_k have hcomp_eq : compressK k (σ (⟨n - 1, by omega⟩ : Fin n).castSucc) hσ_ne = compressK k ⟨j.val + 1, by omega⟩ (Fin.ne_of_gt hj_gt_k) := by have heq' : σ (⟨n - 1, by omega⟩ : Fin n).castSucc = ⟨j.val + 1, by omega⟩ := by rw [hσ_cast]; exact hσ_val simp only [heq', compressK] rw [hcomp_eq, hcompress] have hcast_eq : finCast ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hcomp_last] simp only [j', Fin.ext_iff, finCast] simp · intro τ hτ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hτ ⊢ obtain ⟨hvalid, hτlast⟩ := hτ simp only [bwd] let τ' : Equiv.Perm (Fin n) := castPermFrom τ refine ⟨?_, expandPerm_at_n k τ', ?_⟩ · intro i have hi_lt : i.val < n := i.isLt by_cases hi_last : i.val < n - 1 · have hvalid' : ∀ i' : Fin (n - 1), 0 < (s ⟨i'.val, by omega⟩ : ℤ) * ((τ' ⟨i'.val + 1, by omega⟩ : ℤ) - (τ' ⟨i'.val, by omega⟩ : ℤ)) := by intro i' have hi'_constr := hvalid i' simp only [s', castPermFrom, τ', Equiv.permCongr_apply] at hi'_constr ⊢ have hcast_succ : finCast.symm ⟨i'.val + 1, by omega⟩ = i'.succ := by ext; simp [finCast, Fin.succ] have hcast_castSucc : finCast.symm ⟨i'.val, by omega⟩ = i'.castSucc := by ext; simp [finCast, Fin.castSucc] rw [hcast_succ, hcast_castSucc] convert hi'_constr using 2 have hexpand := sign_constraint_preserved_expand s k τ' hn hvalid' ⟨i.val, hi_last⟩ convert hexpand using 2 · have hi_eq : i.val = n - 1 := by omega have hi_fin_eq : i = ⟨n - 1, by omega⟩ := Fin.ext hi_eq rw [hi_fin_eq] simp only [Fin.succ_mk, Fin.castSucc_mk] have hn' : n - 1 + 1 = n := by omega simp only [hn'] have hτ'_last : τ' ⟨n - 1, by omega⟩ = j := by simp only [τ', castPermFrom, Equiv.permCongr_apply] have hcast_eq : finCast.symm ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hτlast] simp only [j', finCast, Fin.ext_iff]; rfl exact last_constraint_expand_neg hn s hlast k τ' j hj hτ'_last · show (expandPerm k τ') ⟨n - 1, by omega⟩ = ⟨j.val + 1, by omega⟩ simp only [expandPerm] have hne : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by intro h; simp only [Fin.ext_iff] at h; omega have hτ'_last : τ' ⟨n - 1, by omega⟩ = j := by simp only [τ', castPermFrom, Equiv.permCongr_apply] have hcast_eq : finCast.symm ⟨n - 1, by omega⟩ = ⟨n - 1, by omega⟩ := by ext; simp [finCast] rw [hcast_eq, hτlast] simp only [j', finCast, Fin.ext_iff]; rfl have hj_cast : ¬(j.castSucc < k) := by simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc, not_lt] exact hj have hsuccAbove : k.succAbove j = j.succ := Fin.succAbove_of_le_castSucc k j (not_lt.mp hj_cast) have hne_val : (⟨n - 1, by omega⟩ : Fin (n + 1)) ≠ ⟨n, Nat.lt_succ_self n⟩ := by simp only [ne_eq, Fin.ext_iff, Fin.val_mk]; omega simp only [Equiv.coe_fn_mk, hne_val, ↓reduceDIte, hτ'_last, hsuccAbove] rfl · intro σ hσ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hσ obtain ⟨hvalid, hσk, hσj⟩ := hσ simp only [fwd, bwd, hσk, dite_true] have hcast_inv : castPermFrom (castPermTo (compressPerm k σ hσk)) = compressPerm k σ hσk := by simp only [castPermFrom, castPermTo] ext x simp only [Equiv.permCongr_apply, Equiv.symm_symm] simp [finCast] rw [hcast_inv] exact expandPerm_compressPerm k σ hσk · intro τ hτ simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and] at hτ simp only [fwd, bwd] let τ' : Equiv.Perm (Fin n) := castPermFrom τ have hexpand_k : (expandPerm k τ') ⟨n, Nat.lt_succ_self n⟩ = k := expandPerm_at_n k τ' rw [dif_pos hexpand_k] have hcomp_expand : compressPerm k (expandPerm k τ') hexpand_k = τ' := compressPerm_expandPerm k τ' rw [hcomp_expand] simp only [castPermTo, castPermFrom, τ'] ext x simp only [Equiv.permCongr_apply, Equiv.symm_symm] simp [finCast] lemma F_recurrence_minus (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hlast : s ⟨n - 1, by omega⟩ = -1) : ∀ k : Fin (n + 1), F n s k = D n (fun j : Fin n => F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k := by intro k classical unfold F D let s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ let S : Finset (Equiv.Perm (Fin (n + 1))) := Finset.univ.filter fun σ => (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k have hLHS : Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k} = S.card := by rfl rw [hLHS] let proj : Equiv.Perm (Fin (n + 1)) → Fin (n + 1) := fun σ => σ ⟨n - 1, by omega⟩ have h_partition : S.card = ∑ j : Fin (n + 1), (S.filter (fun σ => proj σ = j)).card := by rw [← Finset.card_eq_sum_card_fiberwise (f := proj) (t := Finset.univ)] intro _ _; exact Finset.mem_univ _ rw [h_partition] have h_fiber_empty : ∀ j : Fin (n + 1), j.val ≤ k.val → (S.filter (fun σ => proj σ = j)).card = 0 := by intro j hjk rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] intro σ hσ simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hσ obtain ⟨hvalid, hσk⟩ := hσ intro hproj have hpenult := penult_gt_of_last_sign_neg n hn s hlast σ hvalid k hσk simp only [proj] at hproj rw [hproj] at hpenult omega have h_fiber_bij : ∀ m : Fin (n + 1), k.val < m.val → m.val ≤ n → (S.filter (fun σ => proj σ = m)).card = F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ := by intro m hm_gt_k hm_le_n have hj_lt : m.val - 1 < n := by omega let j : Fin n := ⟨m.val - 1, hj_lt⟩ have hj_val : j.val = m.val - 1 := rfl have hj_ge_k : k.val ≤ j.val := by simp only [hj_val]; omega have hjp1_lt : j.val + 1 < n + 1 := by simp only [hj_val]; omega have hm_val_eq : m.val = j.val + 1 := by simp only [hj_val]; omega have hm_eq : m = ⟨j.val + 1, hjp1_lt⟩ := Fin.ext hm_val_eq have h_eq_fiber : (S.filter (fun σ => proj σ = m)).card = Finset.card {σ : Equiv.Perm (Fin (n + 1)) | (∀ i : Fin n, 0 < (s i : ℤ) * ((σ i.succ : ℤ) - (σ i.castSucc : ℤ))) ∧ σ ⟨n, Nat.lt_succ_self n⟩ = k ∧ σ ⟨n - 1, by omega⟩ = ⟨j.val + 1, by rw [hj_val]; omega⟩} := by congr 1 ext σ simp only [S, Finset.mem_filter, Finset.mem_univ, true_and, proj, Set.mem_setOf_eq] constructor · intro ⟨⟨hvalid, hσk⟩, hproj⟩ refine ⟨hvalid, hσk, ?_⟩ simp only [hproj, hm_eq] · intro ⟨hvalid, hσk, hσj⟩ refine ⟨⟨hvalid, hσk⟩, ?_⟩ simp only [hm_eq, hσj] rw [h_eq_fiber] exact fiber_card_eq_minus n hn s hlast k j hj_ge_k by_cases hk_last : k.val = n · have hS_empty : S.card = 0 := by rw [Finset.card_eq_zero] ext σ simp only [S, Finset.mem_filter, Finset.mem_univ, true_and, Finset.notMem_empty, iff_false] intro ⟨hvalid, hσk⟩ have hpenult := penult_gt_of_last_sign_neg n hn s hlast σ hvalid k hσk have hbound := (σ ⟨n - 1, by omega⟩).isLt omega have hLHS_zero : ∑ j : Fin (n + 1), (S.filter (fun σ => proj σ = j)).card = 0 := by apply Finset.sum_eq_zero intro m _ by_cases hmk : m.val ≤ k.val · exact h_fiber_empty m hmk · have := m.isLt omega rw [hLHS_zero] symm apply Finset.sum_eq_zero intro j _ split_ifs with hjk · have := j.isLt omega · rfl have hk_lt_n : k.val < n := by have := k.isLt; omega have h_sum_decomp : ∑ m : Fin (n + 1), (S.filter (fun σ => proj σ = m)).card = ∑ m : Fin (n + 1), if k.val < m.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ else 0 := by apply Finset.sum_congr rfl intro m _ by_cases hm_le : m.val ≤ k.val · simp only [not_lt.mpr hm_le, ite_false] exact h_fiber_empty m hm_le · have hm_gt : k.val < m.val := by omega simp only [hm_gt, ite_true] exact h_fiber_bij m hm_gt (Nat.lt_succ_iff.mp m.isLt) rw [h_sum_decomp] symm have h_rhs_split : ∑ m : Fin (n + 1), (if k.val < m.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ else 0) = ∑ m : Fin n, (if k.val < m.castSucc.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.castSucc.val - 1, by omega⟩ else 0) + (if k.val < (Fin.last n).val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨(Fin.last n).val - 1, by omega⟩ else 0) := by exact Fin.sum_univ_castSucc _ rw [h_rhs_split] have h_last_term : (if k.val < (Fin.last n).val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨(Fin.last n).val - 1, by omega⟩ else 0) = F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨n - 1, by omega⟩ := by simp only [Fin.val_last, hk_lt_n, ite_true] rw [h_last_term] have h_lhs_eq : ∑ j : Fin n, (if k.val ≤ j.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by omega⟩ else 0) = ∑ j ∈ Finset.filter (fun j : Fin n => k.val ≤ j.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by omega⟩ := by rw [Finset.sum_filter] have h_rhs_sum_eq : ∑ m : Fin n, (if k.val < m.castSucc.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.castSucc.val - 1, by omega⟩ else 0) = ∑ m ∈ Finset.filter (fun m : Fin n => k.val < m.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ := by simp only [Fin.coe_castSucc] rw [Finset.sum_filter] have h_bij : ∑ j ∈ Finset.filter (fun j : Fin n => k.val ≤ j.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by omega⟩ = ∑ m ∈ Finset.filter (fun m : Fin n => k.val < m.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ + F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨n - 1, by omega⟩ := by by_cases hn_pos : 0 < n · have hk_in : (⟨n - 1, by omega⟩ : Fin n) ∈ Finset.filter (fun j : Fin n => k.val ≤ j.val) Finset.univ := by simp only [Finset.mem_filter, Finset.mem_univ, true_and] omega rw [← Finset.add_sum_erase _ _ hk_in, add_comm] congr 1 refine Finset.sum_bij' (fun j hj => ⟨j.val + 1, ?hj_bound⟩) (fun m hm => ⟨m.val - 1, ?hm_bound⟩) ?hi ?hji ?left_inv ?right_inv ?heq case hj_bound => simp only [Finset.mem_erase, Finset.mem_filter, Finset.mem_univ, true_and, ne_eq, Fin.ext_iff] at hj have := j.isLt omega case hm_bound => simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm omega case hi => intro j hj simp only [Finset.mem_erase, Finset.mem_filter, Finset.mem_univ, true_and, ne_eq, Fin.ext_iff] at hj ⊢ omega case hji => intro m hm simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm simp only [Finset.mem_erase, Finset.mem_filter, Finset.mem_univ, true_and, ne_eq, Fin.ext_iff] omega case left_inv => intro j hj ext simp only [Fin.val_mk] simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hj omega case right_inv => intro m hm simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hm ext simp only [Fin.val_mk] omega case heq => intro j hj simp only [Finset.mem_erase, Finset.mem_filter, Finset.mem_univ, true_and, ne_eq, Fin.ext_iff] at hj simp only [Fin.val_mk, Nat.add_sub_cancel] · omega calc ∑ j : Fin n, (if k.val ≤ j.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by omega⟩ else 0) = ∑ j ∈ Finset.filter (fun j : Fin n => k.val ≤ j.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by omega⟩ := h_lhs_eq _ = ∑ m ∈ Finset.filter (fun m : Fin n => k.val < m.val) Finset.univ, F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.val - 1, by omega⟩ + F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨n - 1, by omega⟩ := h_bij _ = ∑ m : Fin n, (if k.val < m.castSucc.val then F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨m.castSucc.val - 1, by omega⟩ else 0) + F (n - 1) (fun i => s ⟨i.val, by omega⟩) ⟨n - 1, by omega⟩ := by rw [h_rhs_sum_eq] lemma U_mono (m : ℕ) (x y : Fin m → ℕ) (hle : ∀ j, x j ≤ y j) : ∀ k, U m x k ≤ U m y k := by intro k unfold U apply Finset.sum_le_sum intro j _ split_ifs with h · exact hle j · rfl lemma D_mono (m : ℕ) (x y : Fin m → ℕ) (hle : ∀ j, x j ≤ y j) : ∀ k, D m x k ≤ D m y k := by intro k unfold D apply Finset.sum_le_sum intro j _ split_ifs with h · exact hle j · rfl lemma F_neg_symm (n : ℕ) (s : Fin n → ℤˣ) (k : Fin (n + 1)) : F n (fun i => -s i) k = F n s ⟨n - k.val, by omega⟩ := by unfold F let bij : Equiv.Perm (Fin (n + 1)) → Equiv.Perm (Fin (n + 1)) := fun σ => σ.trans Fin.revPerm have rev_val_int : ∀ x : Fin (n+1), (x.rev : ℤ) = n - (x : ℤ) := by intro x; have := Fin.rev_add_cast x; omega apply Finset.card_nbij' bij bij · intro σ hσ simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_setOf_eq] at hσ ⊢ constructor · intro i have h1 := hσ.1 i simp only [bij, Equiv.trans_apply, Fin.revPerm_apply, rev_val_int] simp only [Units.val_neg] at h1 linarith · simp only [bij, Equiv.trans_apply, Fin.revPerm_apply] rw [hσ.2] ext; simp only [Fin.val_rev]; omega · intro τ hτ simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_setOf_eq] at hτ ⊢ constructor · intro i have h1 := hτ.1 i simp only [bij, Equiv.trans_apply, Fin.revPerm_apply, rev_val_int, Units.val_neg] linarith · simp only [bij, Equiv.trans_apply, Fin.revPerm_apply] rw [hτ.2] ext; simp only [Fin.val_rev]; omega · intro σ _ simp only [bij, Equiv.trans_assoc] have h : Fin.revPerm.trans Fin.revPerm = Equiv.refl (Fin (n+1)) := by ext x; simp [Fin.revPerm, Fin.rev_rev] simp [h] · intro τ _ simp only [bij, Equiv.trans_assoc] have h : Fin.revPerm.trans Fin.revPerm = Equiv.refl (Fin (n+1)) := by ext x; simp [Fin.revPerm, Fin.rev_rev] simp [h] lemma altSeqMinus_eq_neg_altSeqPlus (m : ℕ) : altSeqMinus m = fun i => -altSeqPlus m i := by funext i unfold altSeqMinus altSeqPlus split_ifs with h <;> rfl lemma sub_sub_cancel_of_lt {k j : ℕ} (h : j < k) : k - 1 - (k - 1 - j) = j := by omega /-! ## Proof sketch for tails_dominate_heads_U The goal is: ∑_{j < k} a(j) ≤ ∑_{j < k} b(j) where b(j) = a(m-1-j). **Approach 1 (term-by-term, doesn't work directly):** Term-by-term comparison a(j) vs a(m-1-j) only holds when j ≤ m-1-j, i.e., j < m/2. For j ≥ m/2, the inequality reverses. So sum_le_sum fails. **Approach 2 (reindexing, correct):** Rewrite RHS as: ∑_{j < k} a(m-1-j) = ∑_{i=m-k}^{m-1} a(i) (last k terms). For each j ∈ {0,...,k-1}, compare a(j) with a(m-k+j): - Since m-k ≥ 0 (k ≤ m), we have j ≤ m-k+j - So a(j) ≤ a(m-k+j) by nondecreasing Sum: ∑_{j=0}^{k-1} a(j) ≤ ∑_{j=0}^{k-1} a(m-k+j) = ∑_{i=m-k}^{m-1} a(i) The RHS equals ∑_{j < k} b(j) via index substitution i = m-1-j. Key Mathlib theorems: Finset.sum_le_sum, sum reindexing via Finset.sum_bij or similar. -/ lemma tails_dominate_heads_U (m : ℕ) (a : Fin m → ℕ) (ha_nondec : ∀ i j : Fin m, i ≤ j → a i ≤ a j) (b : Fin m → ℕ) (hb_rev : ∀ i : Fin m, b i = a ⟨m - 1 - i.val, by omega⟩) : ∀ k : Fin (m + 1), U m a k ≤ U m b k := by intro k unfold U conv_rhs => arg 2; ext j; rw [hb_rev] simp only [← Finset.sum_filter] have hkm : k.val ≤ m := Nat.lt_succ_iff.mp k.isLt rcases m with _ | m' · simp by_cases hk0 : k.val = 0 · simp [hk0] have hk_pos : 0 < k.val := Nat.pos_of_ne_zero hk0 have hkm' : k.val ≤ m' + 1 := hkm have goal_rhs_eq : (∑ j ∈ Finset.filter (fun j : Fin (m' + 1) => j.val < k.val) Finset.univ, a ⟨m' + 1 - 1 - j.val, by have := j.isLt; omega⟩) = (∑ j ∈ Finset.filter (fun j : Fin (m' + 1) => j.val < k.val) Finset.univ, a ⟨m' - j.val, by have := j.isLt; omega⟩) := by apply Finset.sum_congr rfl intro j hj congr 1 rw [goal_rhs_eq] let S := Finset.filter (fun j : Fin (m' + 1) => j.val < k.val) Finset.univ have rhs_eq : (∑ j ∈ S, a ⟨m' - j.val, by have := j.isLt; omega⟩) = (∑ i ∈ S, a ⟨m' - (k.val - 1 - i.val), by have := i.isLt; omega⟩) := by let f : ∀ j ∈ S, Fin (m' + 1) := fun j hj => ⟨k.val - 1 - j.val, by simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hj; omega⟩ let g : ∀ i ∈ S, Fin (m' + 1) := fun i hi => ⟨k.val - 1 - i.val, by simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hi; omega⟩ refine Finset.sum_bij' f g ?_ ?_ ?_ ?_ ?_ · intro j hj simp only [f, S, Finset.mem_filter, Finset.mem_univ, true_and, Fin.val_mk] at hj ⊢ omega · intro i hi simp only [g, S, Finset.mem_filter, Finset.mem_univ, true_and, Fin.val_mk] at hi ⊢ omega · intro j hj simp only [f, g, S, Finset.mem_filter, Finset.mem_univ, true_and] at hj simp only [f, g, Fin.val_mk] ext simp only [Fin.val_mk] exact sub_sub_cancel_of_lt hj · intro i hi simp only [f, g, S, Finset.mem_filter, Finset.mem_univ, true_and] at hi simp only [f, g, Fin.val_mk] ext simp only [Fin.val_mk] exact sub_sub_cancel_of_lt hi · intro j hj simp only [f, S, Finset.mem_filter, Finset.mem_univ, true_and] at hj simp only [f] congr 2 rw [sub_sub_cancel_of_lt hj] rw [rhs_eq] apply Finset.sum_le_sum intro i hi simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hi apply ha_nondec simp only [Fin.le_def, Fin.val_mk] omega /-! ## Proof sketch for tails_dominate_heads_D The goal is: D b k ≤ D a k, i.e., ∑_{j ≥ k} b(j) ≤ ∑_{j ≥ k} a(j) Since b is the reverse of a: - D b k = ∑_{j ≥ k} b(j) = ∑_{j ≥ k} a(m-1-j) = ∑_{i ≤ m-1-k} a(i) = first (m-k) terms - D a k = ∑_{j ≥ k} a(j) = last (m-k) terms So we need: first (m-k) terms ≤ last (m-k) terms. This is the same inequality as tails_dominate_heads_U with k' = m-k. -/ lemma tails_dominate_heads_D (m : ℕ) (a : Fin m → ℕ) (ha_nondec : ∀ i j : Fin m, i ≤ j → a i ≤ a j) (b : Fin m → ℕ) (hb_rev : ∀ i : Fin m, b i = a ⟨m - 1 - i.val, by omega⟩) : ∀ k : Fin (m + 1), D m b k ≤ D m a k := by intro k unfold D conv_lhs => arg 2; ext j; rw [hb_rev] simp only [← Finset.sum_filter] have hkm : k.val ≤ m := Nat.lt_succ_iff.mp k.isLt rcases m with _ | m' · simp by_cases hkmax : k.val = m' + 1 · simp only [hkmax, Finset.filter_true_of_mem, Finset.filter_false_of_mem] have hempty : Finset.filter (fun j : Fin (m' + 1) => m' + 1 ≤ j.val) Finset.univ = ∅ := by ext x simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.notMem_empty, iff_false] have := x.isLt omega simp [hempty] have hk_lt : k.val < m' + 1 := by omega have hkm' : k.val ≤ m' := by omega have goal_lhs_eq : (∑ j ∈ Finset.filter (fun j : Fin (m' + 1) => k.val ≤ j.val) Finset.univ, a ⟨m' + 1 - 1 - j.val, by have := j.isLt; omega⟩) = (∑ j ∈ Finset.filter (fun j : Fin (m' + 1) => k.val ≤ j.val) Finset.univ, a ⟨m' - j.val, by have := j.isLt; omega⟩) := by apply Finset.sum_congr rfl intro j hj congr 1 rw [goal_lhs_eq] let S := Finset.filter (fun j : Fin (m' + 1) => k.val ≤ j.val) Finset.univ have lhs_eq : (∑ j ∈ S, a ⟨m' - j.val, by have := j.isLt; omega⟩) = (∑ i ∈ S, a ⟨m' - (m' + k.val - i.val), by have := i.isLt; omega⟩) := by let f : ∀ j ∈ S, Fin (m' + 1) := fun j hj => ⟨m' + k.val - j.val, by simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hj; omega⟩ let g : ∀ i ∈ S, Fin (m' + 1) := fun i hi => ⟨m' + k.val - i.val, by simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hi; omega⟩ refine Finset.sum_bij' f g ?_ ?_ ?_ ?_ ?_ · intro j hj simp only [f, S, Finset.mem_filter, Finset.mem_univ, true_and, Fin.val_mk] at hj ⊢ omega · intro i hi simp only [g, S, Finset.mem_filter, Finset.mem_univ, true_and, Fin.val_mk] at hi ⊢ omega · intro j hj simp only [f, g, S, Finset.mem_filter, Finset.mem_univ, true_and] at hj simp only [f, g, Fin.val_mk] ext simp only [Fin.val_mk] omega · intro i hi simp only [f, g, S, Finset.mem_filter, Finset.mem_univ, true_and] at hi simp only [f, g, Fin.val_mk] ext simp only [Fin.val_mk] omega · intro j hj simp only [f, S, Finset.mem_filter, Finset.mem_univ, true_and] at hj simp only [f] congr 2 omega rw [lhs_eq] apply Finset.sum_le_sum intro i hi simp only [S, Finset.mem_filter, Finset.mem_univ, true_and] at hi apply ha_nondec simp only [Fin.le_def, Fin.val_mk] omega noncomputable def alpha (m : ℕ) : Fin (m + 1) → ℕ := F m (altSeqPlus m) noncomputable def beta (m : ℕ) : Fin (m + 1) → ℕ := F m (altSeqMinus m) lemma beta_eq_alpha_rev (m : ℕ) (k : Fin (m + 1)) : beta m k = alpha m ⟨m - k.val, by omega⟩ := by unfold beta alpha rw [altSeqMinus_eq_neg_altSeqPlus] exact F_neg_symm m (altSeqPlus m) k lemma altSeqPlus_last' (m : ℕ) (hm : 1 ≤ m) : altSeqPlus m ⟨m - 1, by omega⟩ = 1 := by unfold altSeqPlus simp only [Nat.sub_self, Nat.zero_mod, ↓reduceIte] lemma U_nondecreasing (n : ℕ) (x : Fin n → ℕ) : ∀ i j : Fin (n + 1), i ≤ j → U n x i ≤ U n x j := by intro i j hij unfold U apply Finset.sum_le_sum intro k _ split_ifs with h1 h2 · exact Nat.le_refl _ · omega · exact Nat.zero_le _ · exact Nat.le_refl _ lemma alpha_nondecreasing (m : ℕ) (hm : 1 ≤ m) : ∀ i j : Fin (m + 1), i ≤ j → alpha m i ≤ alpha m j := by intro i j hij unfold alpha have hlast : altSeqPlus m ⟨m - 1, by omega⟩ = 1 := altSeqPlus_last' m hm rw [F_recurrence_plus m hm (altSeqPlus m) hlast i] rw [F_recurrence_plus m hm (altSeqPlus m) hlast j] exact U_nondecreasing m _ i j hij lemma altSeqPlus_prefix_eq_altSeqMinus (m : ℕ) (hm : 1 ≤ m) (i : Fin (m - 1)) : altSeqPlus m ⟨i.val, by omega⟩ = altSeqMinus (m - 1) i := by unfold altSeqPlus altSeqMinus simp only have hi : i.val < m - 1 := i.isLt have h_parity : (m - 1 - i.val) % 2 ≠ (m - 1 - 1 - i.val) % 2 := by omega split_ifs with h1 h2 h2 <;> try rfl · exfalso; omega · exfalso; omega lemma altSeqMinus_prefix_eq_altSeqPlus (m : ℕ) (hm : 1 ≤ m) (i : Fin (m - 1)) : altSeqMinus m ⟨i.val, by omega⟩ = altSeqPlus (m - 1) i := by unfold altSeqPlus altSeqMinus simp only have hi : i.val < m - 1 := i.isLt have h_parity : (m - 1 - i.val) % 2 ≠ (m - 1 - 1 - i.val) % 2 := by omega split_ifs with h1 h2 h2 <;> try rfl · exfalso; omega · exfalso; omega lemma altSeqMinus_last' (m : ℕ) (hm : 1 ≤ m) : altSeqMinus m ⟨m - 1, by omega⟩ = -1 := by unfold altSeqMinus simp only [Nat.sub_self, Nat.zero_mod, ↓reduceIte] lemma domination_combined (m : ℕ) (hm : 1 ≤ m) : (∀ s : Fin m → ℤˣ, s ⟨m - 1, by omega⟩ = 1 → ∀ k : Fin (m + 1), F m s k ≤ alpha m k) ∧ (∀ s : Fin m → ℤˣ, s ⟨m - 1, by omega⟩ = -1 → ∀ k : Fin (m + 1), F m s k ≤ beta m k) := by induction m using Nat.strong_induction_on with | _ m ih => obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩ constructor · intro s hlast k by_cases hm'_zero : m' = 0 · subst hm'_zero have hs_eq : s = altSeqPlus 1 := by ext i fin_cases i simp only [Nat.zero_add, Nat.reduceAdd, Nat.zero_lt_one] at hlast have h0 : s ⟨0, by omega⟩ = 1 := hlast simp only [h0] unfold altSeqPlus simp simp only [Nat.zero_add, hs_eq] unfold alpha rfl · have hm'_pos : 1 ≤ m' := by omega have hm_pos : 1 ≤ m' + 1 := by omega have hrec := F_recurrence_plus (m' + 1) hm_pos s hlast k rw [hrec] have hlast_alt : altSeqPlus (m' + 1) ⟨m' + 1 - 1, by omega⟩ = 1 := altSeqPlus_last' (m' + 1) hm_pos have hrec_alt := F_recurrence_plus (m' + 1) hm_pos (altSeqPlus (m' + 1)) hlast_alt k unfold alpha rw [hrec_alt] set s' : Fin m' → ℤˣ := fun i => s ⟨i.val, by omega⟩ with hs'_def have ih_m' := ih m' (by omega : m' < m' + 1) hm'_pos have h_alpha_nondec : ∀ i j : Fin (m' + 1), i ≤ j → alpha m' i ≤ alpha m' j := alpha_nondecreasing m' hm'_pos have h_beta_rev : ∀ i : Fin (m' + 1), beta m' i = alpha m' ⟨m' - i.val, by omega⟩ := fun i => beta_eq_alpha_rev m' i have h_tails : ∀ kk : Fin (m' + 2), U (m' + 1) (alpha m') kk ≤ U (m' + 1) (beta m') kk := tails_dominate_heads_U (m' + 1) (alpha m') h_alpha_nondec (beta m') h_beta_rev have h_lhs_eq : U (m' + 1) (fun j => F (m' + 1 - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k = U (m' + 1) (F m' s') k := rfl have h_rhs_eq : U (m' + 1) (fun j => F (m' + 1 - 1) (fun i => altSeqPlus (m' + 1) ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k = U (m' + 1) (beta m') k := by unfold beta congr 1 funext j congr 1 funext i have h := altSeqPlus_prefix_eq_altSeqMinus (m' + 1) hm_pos i simp only [Nat.add_sub_cancel] at h exact h rw [h_lhs_eq, h_rhs_eq] have hsign : s' ⟨m' - 1, by omega⟩ = 1 ∨ s' ⟨m' - 1, by omega⟩ = -1 := Int.units_eq_one_or _ rcases hsign with hs'_pos | hs'_neg · have h_dom : ∀ j : Fin (m' + 1), F m' s' j ≤ alpha m' j := ih_m'.1 s' hs'_pos have h_U1 : U (m' + 1) (F m' s') k ≤ U (m' + 1) (alpha m') k := U_mono (m' + 1) (F m' s') (alpha m') h_dom k exact Nat.le_trans h_U1 (h_tails k) · have h_dom : ∀ j : Fin (m' + 1), F m' s' j ≤ beta m' j := ih_m'.2 s' hs'_neg exact U_mono (m' + 1) (F m' s') (beta m') h_dom k · intro s hlast k by_cases hm'_zero : m' = 0 · subst hm'_zero have hs_eq : s = altSeqMinus 1 := by ext i fin_cases i simp only [Nat.zero_add, Nat.reduceAdd, Nat.zero_lt_one] at hlast have h0 : s ⟨0, by omega⟩ = -1 := hlast simp only [h0] unfold altSeqMinus simp simp only [Nat.zero_add, hs_eq] unfold beta rfl · have hm'_pos : 1 ≤ m' := by omega have hm_pos : 1 ≤ m' + 1 := by omega have hrec := F_recurrence_minus (m' + 1) hm_pos s hlast k rw [hrec] have hlast_alt : altSeqMinus (m' + 1) ⟨m' + 1 - 1, by omega⟩ = -1 := altSeqMinus_last' (m' + 1) hm_pos have hrec_alt := F_recurrence_minus (m' + 1) hm_pos (altSeqMinus (m' + 1)) hlast_alt k unfold beta rw [hrec_alt] set s' : Fin m' → ℤˣ := fun i => s ⟨i.val, by omega⟩ with hs'_def have ih_m' := ih m' (by omega : m' < m' + 1) hm'_pos have h_alpha_nondec : ∀ i j : Fin (m' + 1), i ≤ j → alpha m' i ≤ alpha m' j := alpha_nondecreasing m' hm'_pos have h_beta_rev : ∀ i : Fin (m' + 1), beta m' i = alpha m' ⟨m' - i.val, by omega⟩ := fun i => beta_eq_alpha_rev m' i have h_tails : ∀ kk : Fin (m' + 2), D (m' + 1) (beta m') kk ≤ D (m' + 1) (alpha m') kk := tails_dominate_heads_D (m' + 1) (alpha m') h_alpha_nondec (beta m') h_beta_rev have h_lhs_eq : D (m' + 1) (fun j => F (m' + 1 - 1) (fun i => s ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k = D (m' + 1) (F m' s') k := rfl have h_rhs_eq : D (m' + 1) (fun j => F (m' + 1 - 1) (fun i => altSeqMinus (m' + 1) ⟨i.val, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) k = D (m' + 1) (alpha m') k := by unfold alpha congr 1 funext j congr 1 funext i have h := altSeqMinus_prefix_eq_altSeqPlus (m' + 1) hm_pos i simp only [Nat.add_sub_cancel] at h exact h rw [h_lhs_eq, h_rhs_eq] have hsign : s' ⟨m' - 1, by omega⟩ = 1 ∨ s' ⟨m' - 1, by omega⟩ = -1 := Int.units_eq_one_or _ rcases hsign with hs'_pos | hs'_neg · have h_dom : ∀ j : Fin (m' + 1), F m' s' j ≤ alpha m' j := ih_m'.1 s' hs'_pos exact D_mono (m' + 1) (F m' s') (alpha m') h_dom k · have h_dom : ∀ j : Fin (m' + 1), F m' s' j ≤ beta m' j := ih_m'.2 s' hs'_neg have h_D1 : D (m' + 1) (F m' s') k ≤ D (m' + 1) (beta m') k := D_mono (m' + 1) (F m' s') (beta m') h_dom k exact Nat.le_trans h_D1 (h_tails k) lemma domination_plus (m : ℕ) (hm : 1 ≤ m) (s : Fin m → ℤˣ) (hlast : s ⟨m - 1, by omega⟩ = 1) : ∀ k : Fin (m + 1), F m s k ≤ alpha m k := (domination_combined m hm).1 s hlast lemma domination_minus (m : ℕ) (hm : 1 ≤ m) (s : Fin m → ℤˣ) (hlast : s ⟨m - 1, by omega⟩ = -1) : ∀ k : Fin (m + 1), F m s k ≤ beta m k := (domination_combined m hm).2 s hlast lemma f_altPlus_eq_f_altMinus (n : ℕ) : f n (altSeqPlus n) = f n (altSeqMinus n) := by rw [f_eq_sum_F n (altSeqPlus n), f_eq_sum_F n (altSeqMinus n)] conv_rhs => arg 2 ext k rw [altSeqMinus_eq_neg_altSeqPlus] conv_rhs => arg 2 ext k rw [F_neg_symm n (altSeqPlus n) k] symm apply Finset.sum_equiv Fin.revPerm · simp · intro k _ congr 1 ext simp [Fin.rev] lemma f_le_f_alt (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) : f n s ≤ f n (altSeqPlus n) := by have hlast := Int.units_eq_one_or (s ⟨n - 1, by omega⟩) rcases hlast with hpos | hneg · rw [f_eq_sum_F n s, f_eq_sum_F n (altSeqPlus n)] apply Finset.sum_le_sum intro k _ have h := domination_plus n hn s hpos k unfold alpha at h exact h · rw [f_eq_sum_F n s, f_altPlus_eq_f_altMinus n, f_eq_sum_F n (altSeqMinus n)] apply Finset.sum_le_sum intro k _ have h := domination_minus n hn s hneg k unfold beta at h exact h lemma alpha_last_pos (m : ℕ) (hm : 1 ≤ m) : 0 < alpha m ⟨m, by omega⟩ := by induction m with | zero => omega | succ m' ih => cases Nat.lt_or_ge m' 1 with | inl hm'_lt => have hm'_eq : m' = 0 := by omega subst hm'_eq unfold alpha F apply Finset.one_le_card.mpr use Equiv.refl (Fin 2) simp only [Finset.mem_filter, Finset.mem_univ, true_and, Set.mem_setOf_eq] constructor · intro i fin_cases i unfold altSeqPlus simp only [Nat.zero_add, Nat.reduceAdd, Nat.sub_self, Nat.zero_mod, ↓reduceIte, Units.val_one, one_mul, Equiv.Perm.coe_one, id_eq, Fin.succ, Fin.castSucc] norm_num · rfl | inr hm'_ge => have hm'_pos : 1 ≤ m' := hm'_ge have hlast : altSeqPlus (m' + 1) ⟨m' + 1 - 1, by omega⟩ = 1 := altSeqPlus_last' (m' + 1) (by omega) have hrec := F_recurrence_plus (m' + 1) (by omega : 1 ≤ m' + 1) (altSeqPlus (m' + 1)) hlast ⟨m' + 1, by omega⟩ unfold alpha rw [hrec] unfold U simp only [Nat.add_lt_add_iff_right, Fin.val_mk, Nat.lt_add_one_iff, Nat.le_refl, ↓reduceIte] have h_prefix : (fun i : Fin m' => altSeqPlus (m' + 1) ⟨i.val, by omega⟩) = altSeqMinus m' := by funext i exact altSeqPlus_prefix_eq_altSeqMinus (m' + 1) (by omega) i have h_beta_pos : 0 < beta m' ⟨0, by omega⟩ := by rw [beta_eq_alpha_rev m' ⟨0, by omega⟩] simp only [Nat.sub_zero] exact ih hm'_pos unfold beta at h_beta_pos have h_term_pos : 0 < F m' (fun i => altSeqPlus (m' + 1) ⟨↑i, by omega⟩) ⟨0, by omega⟩ := by have heq : (fun i : Fin m' => altSeqPlus (m' + 1) ⟨↑i, by omega⟩) = altSeqMinus m' := h_prefix rw [heq] exact h_beta_pos apply Nat.lt_of_lt_of_le h_term_pos have h_sum_eq : ∑ x : Fin (m' + 1), (if ↑x ≤ m' then F (m' + 1 - 1) (fun i => altSeqPlus (m' + 1) ⟨↑i, by omega⟩) ⟨↑x, by omega⟩ else 0) = ∑ x : Fin (m' + 1), F m' (fun i => altSeqPlus (m' + 1) ⟨↑i, by omega⟩) ⟨↑x, by omega⟩ := by congr 1 funext j have hj : (j : ℕ) ≤ m' := Nat.lt_succ_iff.mp j.isLt simp only [hj, ↓reduceIte, Nat.add_sub_cancel] rfl rw [h_sum_eq] have h0_mem : (0 : Fin (m' + 1)) ∈ Finset.univ := Finset.mem_univ _ apply Finset.single_le_sum (fun k _ => Nat.zero_le _) h0_mem lemma eq_implies_alt : ∀ (n : ℕ), 1 ≤ n → ∀ (s : Fin n → ℤˣ), f n s = f n (altSeqPlus n) → isAlternating n s := by intro n induction n using Nat.strong_induction_on with | _ n ih => intro hn s heq by_cases hn1 : n = 1 · subst hn1 intro i hi exfalso have : i.val = 0 := Fin.val_eq_zero i omega have hn2 : 2 ≤ n := by omega rcases Int.units_eq_one_or (s ⟨n - 1, by omega⟩) with hlast_pos | hlast_neg · have hdom := domination_plus n hn s hlast_pos have hsum_eq : ∑ k : Fin (n + 1), F n s k = ∑ k : Fin (n + 1), alpha n k := by rw [← f_eq_sum_F n s, heq, f_eq_sum_F] unfold alpha rfl have hF_eq : ∀ k : Fin (n + 1), F n s k = alpha n k := by have := Finset.sum_eq_sum_iff_of_le (s := Finset.univ) (f := F n s) (g := alpha n) (fun k _ => hdom k) rw [hsum_eq] at this intro k exact this.mp rfl k (Finset.mem_univ k) have hn_pos : 1 ≤ n := hn have hrec_s := F_recurrence_plus n hn_pos s hlast_pos have hlast_alt := altSeqPlus_last' n hn_pos have hrec_alt := F_recurrence_plus n hn_pos (altSeqPlus n) hlast_alt set s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ with hs'_def by_cases hn1' : n - 1 = 0 · omega have hn1_pos : 1 ≤ n - 1 := by omega rcases Int.units_eq_one_or (s' ⟨n - 1 - 1, by omega⟩) with hs'_pos | hs'_neg · exfalso have hdom_s' := domination_plus (n-1) hn1_pos s' hs'_pos have h_alpha_0 : alpha (n - 1) ⟨0, by omega⟩ = 0 := by unfold alpha have h_alt_last := altSeqPlus_last' (n - 1) hn1_pos rw [F_recurrence_plus (n - 1) hn1_pos (altSeqPlus (n - 1)) h_alt_last] unfold U simp only [Fin.val_zero, Nat.not_lt_zero, ↓reduceIte, Finset.sum_const_zero] have h_beta_0 : beta (n - 1) ⟨0, by omega⟩ = alpha (n - 1) ⟨n - 1, by omega⟩ := by rw [beta_eq_alpha_rev] simp only [Fin.val_zero, Nat.sub_zero] have h_Fs_0 : F n s ⟨0, by omega⟩ = 0 := by rw [hrec_s] unfold U simp only [Fin.val_zero, Nat.not_lt_zero, ↓reduceIte, Finset.sum_const_zero] have h_eq_0 := hF_eq ⟨0, by omega⟩ have h_alpha_n_0 : alpha n ⟨0, by omega⟩ = 0 := by unfold alpha rw [hrec_alt] unfold U simp only [Fin.val_zero, Nat.not_lt_zero, ↓reduceIte, Finset.sum_const_zero] have h_eq_1 := hF_eq ⟨1, by omega⟩ rw [hrec_s] at h_eq_1 unfold U at h_eq_1 have h_lhs_eq_0 : (∑ j : Fin n, if j.val < 1 then F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨0, by omega⟩ := by rw [Finset.sum_eq_single (⟨0, by omega⟩ : Fin n)] · simp · intro b _ hb simp only [ite_eq_right_iff] intro hlt exfalso have hb0 : b.val = 0 := by omega apply hb ext exact hb0 · intro hne exfalso apply hne exact Finset.mem_univ _ rw [h_lhs_eq_0] at h_eq_1 have h_alpha_1 : alpha n ⟨1, by omega⟩ = beta (n - 1) ⟨0, by omega⟩ := by unfold alpha rw [hrec_alt] unfold U simp only [Fin.val_one, Nat.lt_one_iff, Fin.val_eq_zero] rw [Finset.sum_eq_single (⟨0, by omega⟩ : Fin n)] · simp only [↓reduceIte] unfold beta congr 1 funext i have h := altSeqPlus_prefix_eq_altSeqMinus n hn_pos i simp only [Nat.sub_one_add_one_eq_of_pos (by omega : 0 < n)] at h exact h · intro b _ hb simp only [ite_eq_right_iff] intro heq exfalso; apply hb; ext; simp [heq] · intro hne exfalso; apply hne; exact Finset.mem_univ _ rw [h_alpha_1] at h_eq_1 rw [h_beta_0] at h_eq_1 have h_dom_s'_0 := hdom_s' ⟨0, by omega⟩ rw [h_alpha_0] at h_dom_s'_0 have h_Fs'_0 : F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨0, by omega⟩ = 0 := Nat.le_zero.mp h_dom_s'_0 rw [h_Fs'_0] at h_eq_1 have h_alpha_pos : 0 < alpha (n - 1) ⟨n - 1, by omega⟩ := alpha_last_pos (n - 1) (by omega) omega · have hsum_s' : f (n - 1) s' = f (n - 1) (altSeqPlus (n - 1)) := by rw [f_eq_sum_F (n - 1) s', f_eq_sum_F (n - 1) (altSeqPlus (n - 1))] have h_eq_n := hF_eq ⟨n, by omega⟩ rw [hrec_s] at h_eq_n unfold U at h_eq_n simp only [Fin.val_natCast, Nat.mod_self, Nat.lt_irrefl, not_false_eq_true] at h_eq_n have h_lhs : (∑ j : Fin n, if j.val < n then F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = ∑ j : Fin n, F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ := by apply Finset.sum_congr rfl intro j _ have hj : j.val < n := j.isLt simp only [hj, ↓reduceIte] rw [h_lhs] at h_eq_n have h_alpha_n_eq : alpha n ⟨n, by omega⟩ = ∑ j : Fin n, beta (n - 1) ⟨j.val, by have := j.isLt; omega⟩ := by unfold alpha rw [hrec_alt] unfold U apply Finset.sum_congr rfl intro j _ have hj : j.val < n := j.isLt simp only [hj, ↓reduceIte] congr 1 funext i exact altSeqPlus_prefix_eq_altSeqMinus n hn_pos i rw [h_alpha_n_eq] at h_eq_n have h1 : (∑ j : Fin n, F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) = f (n - 1) s' := by rw [f_eq_sum_F (n - 1) s'] apply Finset.sum_nbij' (fun j : Fin n => ⟨j.val, by have := j.isLt; omega⟩) (fun k : Fin ((n - 1) + 1) => ⟨k.val, by have := k.isLt; omega⟩) · intro j _; simp · intro k _; simp · intro j _; ext; simp · intro k _; ext; simp · intro j _; rfl have h2 : (∑ j : Fin n, beta (n - 1) ⟨j.val, by have := j.isLt; omega⟩) = f (n - 1) (altSeqMinus (n - 1)) := by rw [f_eq_sum_F (n - 1) (altSeqMinus (n - 1))] unfold beta apply Finset.sum_nbij' (fun j : Fin n => ⟨j.val, by have := j.isLt; omega⟩) (fun k : Fin ((n - 1) + 1) => ⟨k.val, by have := k.isLt; omega⟩) · intro j _; simp · intro k _; simp · intro j _; ext; simp · intro k _; ext; simp · intro j _; rfl rw [h1, h2] at h_eq_n rw [← f_eq_sum_F (n - 1) s', ← f_eq_sum_F (n - 1) (altSeqPlus (n - 1))] rw [h_eq_n, f_altPlus_eq_f_altMinus] have hs'_alt : isAlternating (n - 1) s' := ih (n - 1) (by omega) hn1_pos s' hsum_s' intro i hi by_cases hi' : i.val + 1 < n - 1 · have h := hs'_alt ⟨i.val, by omega⟩ hi' simp only [hs'_def] at h convert h using 2 · have hi_eq : i.val = n - 2 := by omega have hs_n2 : s ⟨n - 2, by omega⟩ = -1 := by have : s' ⟨n - 1 - 1, by omega⟩ = -1 := hs'_neg simp only [hs'_def] at this have heq : (n - 2 : ℕ) = n - 1 - 1 := by omega simp only [heq] exact this have hs_n1 : s ⟨n - 1, by omega⟩ = 1 := hlast_pos have h : s ⟨i.val + 1, hi⟩ = -s i := by have h1 : s ⟨i.val + 1, hi⟩ = s ⟨n - 1, by omega⟩ := by congr 1 ext simp only [hi_eq] omega have h2 : (i : Fin n) = ⟨n - 2, by omega⟩ := by ext exact hi_eq rw [h1, hs_n1, h2, hs_n2] simp exact h · have hdom := domination_minus n hn s hlast_neg have hsum_eq : ∑ k : Fin (n + 1), F n s k = ∑ k : Fin (n + 1), beta n k := by rw [← f_eq_sum_F n s, heq, f_altPlus_eq_f_altMinus, f_eq_sum_F] unfold beta rfl have hF_eq : ∀ k : Fin (n + 1), F n s k = beta n k := by have := Finset.sum_eq_sum_iff_of_le (s := Finset.univ) (f := F n s) (g := beta n) (fun k _ => hdom k) rw [hsum_eq] at this intro k exact this.mp rfl k (Finset.mem_univ k) have hn_pos : 1 ≤ n := hn have hrec_s := F_recurrence_minus n hn_pos s hlast_neg have hlast_alt := altSeqMinus_last' n hn_pos have hrec_alt := F_recurrence_minus n hn_pos (altSeqMinus n) hlast_alt set s' : Fin (n - 1) → ℤˣ := fun i => s ⟨i.val, by omega⟩ with hs'_def by_cases hn1' : n - 1 = 0 · omega have hn1_pos : 1 ≤ n - 1 := by omega rcases Int.units_eq_one_or (s' ⟨n - 1 - 1, by omega⟩) with hs'_pos | hs'_neg · have hsum_s' : f (n - 1) s' = f (n - 1) (altSeqPlus (n - 1)) := by rw [f_eq_sum_F (n - 1) s', f_eq_sum_F (n - 1) (altSeqPlus (n - 1))] have h_eq_n := hF_eq ⟨n, by omega⟩ rw [hrec_s] at h_eq_n unfold D at h_eq_n have h_lhs : (∑ j : Fin n, if n ≤ j.val then F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = 0 := by apply Finset.sum_eq_zero intro j _ have hj : j.val < n := j.isLt simp only [Nat.not_le_of_lt hj, ↓reduceIte] have h_eq_0 := hF_eq ⟨0, by omega⟩ rw [hrec_s] at h_eq_0 unfold D at h_eq_0 have h_lhs' : (∑ j : Fin n, if 0 ≤ j.val then F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = ∑ j : Fin n, F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ := by apply Finset.sum_congr rfl intro j _ simp only [Nat.zero_le, ↓reduceIte] rw [h_lhs'] at h_eq_0 have h_beta_0_eq : beta n ⟨0, by omega⟩ = ∑ j : Fin n, alpha (n - 1) ⟨j.val, by have := j.isLt; omega⟩ := by unfold beta rw [hrec_alt] unfold D apply Finset.sum_congr rfl intro j _ simp only [Nat.zero_le, ↓reduceIte] congr 1 funext i exact altSeqMinus_prefix_eq_altSeqPlus n hn_pos i rw [h_beta_0_eq] at h_eq_0 have h1 : (∑ j : Fin n, F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩) = f (n - 1) s' := by rw [f_eq_sum_F (n - 1) s'] apply Finset.sum_nbij' (fun j : Fin n => ⟨j.val, by have := j.isLt; omega⟩) (fun k : Fin ((n - 1) + 1) => ⟨k.val, by have := k.isLt; omega⟩) · intro j _; simp · intro k _; simp · intro j _; ext; simp · intro k _; ext; simp · intro j _; rfl have h2 : (∑ j : Fin n, alpha (n - 1) ⟨j.val, by have := j.isLt; omega⟩) = f (n - 1) (altSeqPlus (n - 1)) := by rw [f_eq_sum_F (n - 1) (altSeqPlus (n - 1))] unfold alpha apply Finset.sum_nbij' (fun j : Fin n => ⟨j.val, by have := j.isLt; omega⟩) (fun k : Fin ((n - 1) + 1) => ⟨k.val, by have := k.isLt; omega⟩) · intro j _; simp · intro k _; simp · intro j _; ext; simp · intro k _; ext; simp · intro j _; rfl rw [h1, h2] at h_eq_0 rw [← f_eq_sum_F (n - 1) s', ← f_eq_sum_F (n - 1) (altSeqPlus (n - 1))] exact h_eq_0 have hs'_alt : isAlternating (n - 1) s' := ih (n - 1) (by omega) hn1_pos s' hsum_s' intro i hi by_cases hi' : i.val + 1 < n - 1 · have h := hs'_alt ⟨i.val, by omega⟩ hi' simp only [hs'_def] at h convert h using 2 · have hi_eq : i.val = n - 2 := by omega have hs_n2 : s ⟨n - 2, by omega⟩ = 1 := by have : s' ⟨n - 1 - 1, by omega⟩ = 1 := hs'_pos simp only [hs'_def] at this have heq : (n - 2 : ℕ) = n - 1 - 1 := by omega simp only [heq] exact this have hs_n1 : s ⟨n - 1, by omega⟩ = -1 := hlast_neg have h : s ⟨i.val + 1, hi⟩ = -s i := by have h1 : s ⟨i.val + 1, hi⟩ = s ⟨n - 1, by omega⟩ := by congr 1; ext simp only [hi_eq] omega have h2 : (i : Fin n) = ⟨n - 2, by omega⟩ := by ext; exact hi_eq rw [h1, hs_n1, h2, hs_n2] exact h · exfalso have hdom_s' := domination_minus (n-1) hn1_pos s' hs'_neg have h_beta_last : beta (n - 1) ⟨n - 1, by omega⟩ = alpha (n - 1) ⟨0, by omega⟩ := by rw [beta_eq_alpha_rev] congr 1; simp have h_alpha_0 : alpha (n - 1) ⟨0, by omega⟩ = 0 := by unfold alpha have h_alt_last := altSeqPlus_last' (n - 1) hn1_pos rw [F_recurrence_plus (n - 1) hn1_pos (altSeqPlus (n - 1)) h_alt_last] unfold U simp only [Fin.val_zero, Nat.not_lt_zero, ↓reduceIte, Finset.sum_const_zero] have h_dom_s'_last := hdom_s' ⟨n - 1, by omega⟩ rw [h_beta_last, h_alpha_0] at h_dom_s'_last have h_Fs'_last : F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨n - 1, by omega⟩ = 0 := Nat.le_zero.mp h_dom_s'_last have h_eq_nm1 := hF_eq ⟨n - 1, by omega⟩ rw [hrec_s] at h_eq_nm1 unfold D at h_eq_nm1 have h_lhs_nm1 : (∑ j : Fin n, if (n - 1) ≤ j.val then F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = F (n - 1) (fun i => s ⟨↑i, by omega⟩) ⟨n - 1, by omega⟩ := by rw [Finset.sum_eq_single (⟨n - 1, by omega⟩ : Fin n)] · simp · intro b _ hb simp only [ite_eq_right_iff] intro hle exfalso have hb' : b.val < n := b.isLt have hne : b.val ≠ n - 1 := by intro heq; apply hb; ext; exact heq omega · intro hne; exfalso; apply hne; exact Finset.mem_univ _ rw [h_lhs_nm1] at h_eq_nm1 have h_beta_nm1 : beta n ⟨n - 1, by omega⟩ = alpha (n - 1) ⟨n - 1, by omega⟩ := by unfold beta rw [hrec_alt] unfold D have h : (∑ j : Fin n, if (n - 1) ≤ j.val then F (n - 1) (fun i => altSeqMinus n ⟨↑i, by omega⟩) ⟨j.val, by have := j.isLt; omega⟩ else 0) = F (n - 1) (fun i => altSeqMinus n ⟨↑i, by omega⟩) ⟨n - 1, by omega⟩ := by rw [Finset.sum_eq_single (⟨n - 1, by omega⟩ : Fin n)] · simp · intro b _ hb simp only [ite_eq_right_iff] intro hle exfalso have hb' : b.val < n := b.isLt have hne : b.val ≠ n - 1 := by intro heq; apply hb; ext; exact heq omega · intro hne; exfalso; apply hne; exact Finset.mem_univ _ rw [h] unfold alpha congr 1 funext i exact altSeqMinus_prefix_eq_altSeqPlus n hn_pos i rw [h_beta_nm1] at h_eq_nm1 rw [h_Fs'_last] at h_eq_nm1 have h_alpha_pos : 0 < alpha (n - 1) ⟨n - 1, by omega⟩ := alpha_last_pos (n - 1) (by omega) omega lemma f_strict_lt_of_not_alt (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hnotalt : ¬ isAlternating n s) : f n s < f n (altSeqPlus n) := by have hle := f_le_f_alt n hn s by_contra h_not_lt push_neg at h_not_lt have heq : f n s = f n (altSeqPlus n) := Nat.le_antisymm hle h_not_lt have halt := eq_implies_alt n hn s heq exact hnotalt halt lemma alt_in_solution (n : ℕ) : altSeqPlus n ∈ putnam_2025_a5_solution n ∧ altSeqMinus n ∈ putnam_2025_a5_solution n := by simp only [Set.mem_setOf_eq] constructor · intro i h simp only [altSeqPlus] have hi : i.val + 1 < n := h split_ifs with h1 h2 <;> first | rfl | (exfalso; omega) · intro i h simp only [altSeqMinus] have hi : i.val + 1 < n := h split_ifs with h1 h2 <;> first | rfl | (exfalso; omega) lemma solution_eq_alternating (n : ℕ) : putnam_2025_a5_solution n = {s | isAlternating n s} := by rfl lemma alt_eq_of_last_eq (n : ℕ) (hn : 1 ≤ n) (s t : Fin n → ℤˣ) (hs : isAlternating n s) (ht : isAlternating n t) (hlast : s ⟨n - 1, by omega⟩ = t ⟨n - 1, by omega⟩) : s = t := by funext ⟨i, hi⟩ have hind : ∀ d : ℕ, ∀ j : ℕ, (hj : j < n) → n - 1 - j = d → s ⟨j, hj⟩ = t ⟨j, hj⟩ := by intro d induction d using Nat.strong_induction_on with | _ d ih => intro j hj hd by_cases hj_last : j = n - 1 · subst hj_last convert hlast using 2 · have hj' : j + 1 < n := by omega have hd' : n - 1 - (j + 1) < d := by omega have ih_apply : s ⟨j + 1, hj'⟩ = t ⟨j + 1, hj'⟩ := ih (n - 1 - (j + 1)) hd' (j + 1) hj' rfl have hs_alt := hs ⟨j, hj⟩ hj' have ht_alt := ht ⟨j, hj⟩ hj' have h1 : s ⟨j, hj⟩ = -s ⟨j + 1, hj'⟩ := by simp only at hs_alt rw [hs_alt, neg_neg] have h2 : t ⟨j, hj⟩ = -t ⟨j + 1, hj'⟩ := by simp only at ht_alt rw [ht_alt, neg_neg] rw [h1, h2, ih_apply] exact hind (n - 1 - i) i hi rfl lemma altSeqPlus_isAlternating (n : ℕ) : isAlternating n (altSeqPlus n) := by intro i hi simp only [altSeqPlus] split_ifs with h1 h2 <;> first | rfl | (exfalso; omega) lemma altSeqMinus_isAlternating (n : ℕ) : isAlternating n (altSeqMinus n) := by intro i hi simp only [altSeqMinus] split_ifs with h1 h2 <;> first | rfl | (exfalso; omega) lemma altSeqPlus_last (n : ℕ) (hn : 1 ≤ n) : altSeqPlus n ⟨n - 1, by omega⟩ = 1 := by simp only [altSeqPlus] split_ifs with h · rfl · exfalso; omega lemma altSeqMinus_last (n : ℕ) (hn : 1 ≤ n) : altSeqMinus n ⟨n - 1, by omega⟩ = -1 := by simp only [altSeqMinus] split_ifs with h · rfl · exfalso; omega lemma f_alt_eq_f_altPlus (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) (hs : isAlternating n s) : f n s = f n (altSeqPlus n) := by rcases Int.units_eq_one_or (s ⟨n - 1, by omega⟩) with hlast | hlast · have hs_eq : s = altSeqPlus n := alt_eq_of_last_eq n hn s (altSeqPlus n) hs (altSeqPlus_isAlternating n) (by rw [hlast, altSeqPlus_last n hn]) rw [hs_eq] · have hs_eq : s = altSeqMinus n := alt_eq_of_last_eq n hn s (altSeqMinus n) hs (altSeqMinus_isAlternating n) (by rw [hlast, altSeqMinus_last n hn]) rw [hs_eq, ← f_altPlus_eq_f_altMinus] /-- Let $n$ be an integer with $n \ge 2$. For a sequence $s = (s_1, \ldots, s_{n-1})$ where each $s_i = \pm 1$, let $f(s)$ be the number of permutations $(a_1, \ldots, a_n)$ of $\{1, 2, \ldots, n\}$ such that $s_i(a_{i+1} - a_i) > 0$ for all $i$. For each $n$, determine the sequences $s$ for which $f(s)$ is maximal. -/ theorem putnam_2025_a5 (n : ℕ) (hn : 1 ≤ n) (s : Fin n → ℤˣ) : (∀ t : Fin n → ℤˣ, f n t ≤ f n s) ↔ s ∈ putnam_2025_a5_solution n := by constructor · intro hmax rw [solution_eq_alternating] by_contra hnotalt have hstrict := f_strict_lt_of_not_alt n hn s hnotalt have hle := hmax (altSeqPlus n) omega · intro hs_alt intro t have h1 := f_le_f_alt n hn t rw [solution_eq_alternating] at hs_alt have h2 : f n s = f n (altSeqPlus n) := f_alt_eq_f_altPlus n hn s hs_alt omega