Library mathcomp_eulerian.altsub


From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress.
From mathcomp_eulerian Require Import descent eulerian beta beta_omega.
From mathcomp_eulerian Require Import beta_swap.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section TurnDefs.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

is_turn s i is the boolean indicator that interior position i : 'I_n is a turning point of s : {perm 'I_n.+2}: the descent indicator at slot widen i differs (XOR) from the indicator at slot lift ord0 i. These two slots straddle position i.
Definition is_turn s (i : 'I_n) : bool :=
  is_descent s (widen_ord (leqnSn _) i) (+) is_descent s (lift ord0 i).

turn_count s is the number of turning points of s, i.e., the cardinality of [set i : 'I_n | is_turn s i]. Stanley §1.6.2: the "turn count" governing the longest alternating subsequence length.
Definition turn_count s : nat :=
  #|[set i : 'I_n | is_turn s i]|.

Definitional unfolding of is_turn to its XOR-of-descents form; used as a rewrite rule.
End TurnDefs.



alt_aux b x xs checks alternation of the seq x :: xs given the expected direction b of the first comparison (true = up, false = down). Successive directions flip at each step.
Fixpoint alt_aux (b : bool) (x : nat) (xs : seq nat) : bool :=
  match xs with
  | [::] ⇒ true
  | y :: xs' ⇒
      (if b then x < y else y < x) && alt_aux (~~ b) y xs'
  end.

is_alt xs holds when xs is alternating: comparisons of consecutive elements strictly alternate between < and >. Two starts are possible (up-down or down-up); both are accepted by disjunction.
Definition is_alt (xs : seq nat) : bool :=
  match xs with
  | [::] ⇒ true
  | [:: _] ⇒ true
  | x :: y :: xs' ⇒
      ((x < y) && alt_aux false y xs') || ((y < x) && alt_aux true y xs')
  end.


perm_seq s is the one-line word [s 0; s 1; ...; s (n+1)] of s : {perm 'I_n.+2}, as a seq nat.
Definition perm_seq n (s : {perm 'I_n.+2}) : seq nat :=
  [seq val (s i) | i <- enum 'I_n.+2].

perm_seq s always has length n.+2.
Lemma size_perm_seq n (s : {perm 'I_n.+2}) :
  size (perm_seq s) = n.+2.
Proof. by rewrite size_map size_enum_ord. Qed.


pick_seq s I is the subseq of perm_seq s indexed by the position set I : {set 'I_n.+2} in ascending order: sort I by underlying val, then read off the s-values.
Definition pick_seq n (s : {perm 'I_n.+2}) (I : {set 'I_n.+2}) : seq nat :=
  [seq val (s j) | j <- sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)].

as_perm_max s is the bijective definition of as(s) from Stanley §1.6.2: the maximum cardinality of a position set I whose ordered image pick_seq s I is alternating.
Definition as_perm_max n (s : {perm 'I_n.+2}) : nat :=
  \max_(I : {set 'I_n.+2} | is_alt (pick_seq s I)) #|I|.

as_perm s is the DIRECT definition (Path X) of as(s) as (turn_count s).+2. The headline as_perm_max_eq proves these two definitions agree.
Definition as_perm n (s : {perm 'I_n.+2}) : nat := (turn_count s).+2.



Example alt_312 : is_alt [:: 3; 1; 2] = true.
Proof. by []. Qed.

Example alt_321 : is_alt [:: 3; 2; 1] = false.
Proof. by []. Qed.

Example alt_3142 : is_alt [:: 3; 1; 4; 2] = true.
Proof. by []. Qed.

Example alt_31425 : is_alt [:: 3; 1; 4; 2; 5] = true.
Proof. by []. Qed.

Example alt_321_sub : is_alt [:: 3; 1] = true.
Proof. by []. Qed.



The empty seq is alternating. A singleton seq is alternating.


Defining equation of alt_aux on a cons tail. Used as a rewrite. Defining equation of is_alt on a 2-element prefix x :: y :: xs: either start with an ascent or a descent. Used as a rewrite.
Lemma is_alt_cons2 x y xs :
  is_alt (x :: y :: xs) =
    ((x < y) && alt_aux false y xs) || ((y < x) && alt_aux true y xs).
Proof. by []. Qed.


Shape lemma: a non-empty seq tail satisfying alt_aux decomposes as y :: xs'. Tail closure of is_alt: dropping the first element of an alternating seq of length at least 2 leaves an alternating seq.

Section TurnLemmas.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Cardinality bound: the turn-set of s : {perm 'I_n.+2} has at most n turning points.
Lemma turn_count_le s : turn_count s ≤ n.
Proof.
rewrite /turn_count (leq_trans (max_card _)) // card_ord //.
Qed.

Definitional unfolding as_perm s = (turn_count s).+2; rewrite rule.
Lemma as_permE s : as_perm s = (turn_count s).+2.
Proof. by []. Qed.

Lower bound: any as_perm is at least 2 (the empty/two-element base case). Upper bound on as_perm: bounded by n.+2, the size of perm_seq s. The identity permutation has no descents, hence no turning points: turn_count 1 = 0.
Lemma turn_count_id : turn_count (1 : {perm 'I_n.+2}) = 0.
Proof.
apply/eqP; rewrite cards_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
rewrite /is_turn /is_descent !perm1.
have H1 : (val (lift ord0 (widen_ord (leqnSn n) i)) : nat) =
          (val (widen_ord (leqnSn n.+1) (widen_ord (leqnSn n) i))).+1.
  by rewrite /=.
have H2 : (val (lift ord0 (lift ord0 i)) : nat) =
          (val (widen_ord (leqnSn n.+1) (lift ord0 i))).+1.
  by rewrite /= /bump /= add1n.
rewrite ltnNge leqW //=.
rewrite ltnNge leqW //=.
Qed.

as_perm hits its minimum 2 on the identity permutation.
End TurnLemmas.



Section AltDesc.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

When s has the alternating descent pattern, every interior position is a turning point: turn_count s = n.
Lemma turn_count_alt_desc s :
  descent_set s = alt_desc_set n.+1 → turn_count s = n.
Proof.
move⇒ Hds.
rewrite /turn_count -[RHS]card_ord.
apply: eq_card ⇒ i.
rewrite !inE /=.
rewrite /is_turn -!mem_descent_set Hds !mem_alt_desc_set /=.
rewrite negbK add0n.
by case: (odd i).
Qed.

When s has the alternating descent pattern, as_perm s attains its maximum value n.+2.
Lemma as_perm_alt_desc s :
  descent_set s = alt_desc_set n.+1 → as_perm s = n.+2.
Proof. by move⇒ Hds; rewrite as_permE (turn_count_alt_desc Hds). Qed.

Characterization of the maximum turn_count s = n: equivalent to every position i : 'I_n being a turning point.
End AltDesc.


Section AsPermMaxBounds.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Trivial alternation: any pick_seq s I of size at most 1 is automatically alternating. Trivial nonnegativity of as_perm_max; nat-valued.
End AsPermMaxBounds.




Section MaxAlternation.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

When the descent set is alternating, as_perm s equals the full sequence length size (perm_seq s) = n.+2.
End MaxAlternation.



sign_seq xs is the boolean direction sequence at each adjacent pair: xs[i] < xs[i+1] for i = 0, ..., size xs - 2. Empty for xs = nil.
Definition sign_seq (xs : seq nat) : seq bool :=
  if xs is x :: xs' then pairmap (fun a b ⇒ a < b) x xs'
  else [::].

Cons reduction for sign_seq on a 2-prefix. Size of sign_seq xs: one less than size xs.
Lemma size_sign_seq xs : size (sign_seq xs) = (size xs).-1.
Proof.
case: xs ⇒ [|x xs] //=.
by rewrite size_pairmap.
Qed.

flip_count ss is the number of adjacent disagreements (XOR flips) in a boolean seq ss. Counts indices i with ss[i] != ss[i+1].
Definition flip_count (ss : seq bool) : nat :=
  if ss is a :: ss' then \sum_(p <- pairmap (fun u v ⇒ u (+) v) a ss') p
  else 0.

Cons reduction: flip count of a :: b :: ss equals the boundary flip a (+) b plus the flip count of b :: ss. turn_count_seq xs is the seq-level turn count: number of direction flips in xs, i.e., flip_count (sign_seq xs). The seq analogue of turn_count for permutations.
Definition turn_count_seq (xs : seq nat) : nat := flip_count (sign_seq xs).

turn_count_seq of the empty seq is 0. turn_count_seq of a singleton is 0. turn_count_seq of a 2-element seq is 0: only one comparison, no flip.
Example tcs_312 : turn_count_seq [:: 3; 1; 2] = 1.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= big_cons big_nil.
Qed.

Example tcs_3142 : turn_count_seq [:: 3; 1; 4; 2] = 2.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= !big_cons big_nil.
Qed.

Example tcs_321 : turn_count_seq [:: 3; 2; 1] = 0.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= big_cons big_nil.
Qed.

Example tcs_12345 : turn_count_seq [:: 1; 2; 3; 4; 5] = 0.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= !big_cons big_nil.
Qed.





Section SignPerm.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

The sign sequence of perm_seq s has length n.+1, one slot per pair of consecutive positions.
Lemma size_sign_seq_perm s :
  size (sign_seq (perm_seq s)) = n.+1.
Proof. by rewrite size_sign_seq size_perm_seq /=. Qed.

Decomposition of enum 'I_n.+2 as ord0 followed by the lift ord0-image of enum 'I_n.+1. Used to align indexing of perm_seq with sign_seq.
Lemma enum_ord_split :
  enum 'I_n.+2 = ord0 :: [seq lift ord0 i | i <- enum 'I_n.+1].
Proof.
apply: (@eq_from_nth _ ord0).
  by rewrite /= size_map !size_enum_ord.
rewrite size_enum_ord ⇒ i Hi.
case: i Hi ⇒ [|i] Hi /=.
  apply: val_inj ⇒ /=.
  by have := @nth_enum_ord n.+2 ord0 0 Hi.
rewrite (nth_map ord0); last by rewrite size_enum_ord -ltnS.
have Hi' : i < n.+1 by rewrite -ltnS.
apply: val_inj ⇒ /=.
have H1 := @nth_enum_ord n.+2 ord0 i.+1 Hi.
have H2 := @nth_enum_ord n.+1 ord0 i Hi'.
by rewrite H1 /bump /= add1n H2.
Qed.

Negated descent indicator as a strict less-than: ~~ is_descent s i iff val (s (widen i)) < val (s (lift ord0 i)).
Lemma not_is_descentE s (i : 'I_n.+1) :
  ~~ is_descent s i =
    (val (s (widen_ord (leqnSn _) i)) < val (s (lift ord0 i))).
Proof.
rewrite /is_descent -leqNgt.
have Hne : widen_ord (leqnSn n.+1) i != lift ord0 i.
  by rewrite -val_eqE /= /bump /= add1n neq_ltn ltnSn.
have Hsne : s (widen_ord (leqnSn n.+1) i) != s (lift ord0 i).
  by apply: contra Hne ⇒ /eqP /perm_inj →.
have Hvne : val (s (widen_ord (leqnSn n.+1) i)) != val (s (lift ord0 i)).
  by rewrite val_eqE.
rewrite leq_eqVlt (negbTE Hvne) /=.
by [].
Qed.

Bridge identifying sign_seq (perm_seq s) with the (negated) descent indicator over enum 'I_n.+1. Connects the seq-level flip-count machinery to the perm-level descent/turn structure.
Lemma sign_seq_perm_seq s :
  sign_seq (perm_seq s) = [seq ~~ is_descent s i | i <- enum 'I_n.+1].
Proof.
apply: (@eq_from_nth _ true).
  by rewrite size_sign_seq_perm size_map size_enum_ord.
move⇒ i; rewrite size_sign_seq_perm ⇒ Hi.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite /sign_seq /perm_seq.
rewrite enum_ord_split map_cons -map_comp.
rewrite (@nth_pairmap _ 0 _ true (fun a b : nat ⇒ a < b)); last first.
  by rewrite size_map size_enum_ord.
rewrite not_is_descentE.
have Hidx : nth ord0 (enum 'I_n.+1) i = Ordinal Hi.
  by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
case: i Hi Hidx ⇒ [|j] Hi Hidx /=.
- rewrite (nth_map ord0); last by rewrite size_enum_ord.
  rewrite Hidx /=. by congr (s _ < s _); apply: val_inj.
- have Hj : j < n.+1 by apply: ltnW.
  rewrite (nth_map ord0); last by rewrite size_enum_ord.
  rewrite (nth_map ord0); last by rewrite size_enum_ord.
  rewrite Hidx.
  have → : nth ord0 (enum 'I_n.+1) j = Ordinal Hj.
    by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
  rewrite /=; congr (s _ < s _).
  by apply: val_inj ⇒ /=; rewrite /bump /= add1n.
Qed.

End SignPerm.


Section AsPermMaxBoundsM.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Trivial size bound: as_perm_max s ≤ n.+2, the size of the underlying perm_seq s.
Lemma as_perm_max_le_size s : as_perm_max s ≤ n.+2.
Proof.
rewrite /as_perm_max.
apply/bigmax_leqP ⇒ I _.
by rewrite (leq_trans (subset_leq_card (subsetT I))) // cardsT card_ord.
Qed.

End AsPermMaxBoundsM.

Section PickSeqFull.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

enum 'I_m is sorted by val ascending. Used to identify pick_seq s [set: ...] with perm_seq s.
Lemma sorted_val_enum_ord m :
  sorted (fun a b : 'I_m ⇒ val a ≤ val b) (enum 'I_m).
Proof.
have := iota_sorted 0 m.
rewrite -val_enum_ord.
elim: (enum 'I_m) ⇒ [|x [|y xs] IH] //=.
move⇒ /andP [Hxy Hr].
by rewrite Hxy; apply: IH; rewrite /= Hr.
Qed.

Picking the full position set yields the full one-line word: pick_seq s [set: 'I_n.+2] = perm_seq s.
Lemma pick_seq_setT s : pick_seq s [set: 'I_n.+2] = perm_seq s.
Proof.
rewrite /pick_seq /perm_seq.
congr [seq val (s _) | _ <- _].
rewrite enum_setT -enumT.
apply: sorted_sort.
- by move⇒ a b c; apply: leq_trans.
- exact: sorted_val_enum_ord.
Qed.

If perm_seq s is itself alternating, as_perm_max s hits its maximum n.+2 (witnessed by the full set).
End PickSeqFull.


Any seq of size at most 1 is alternating. An alternating seq of length at least 3 cannot have its first three entries strictly monotone in either direction.
Lemma is_alt_three x y z xs :
  is_alt (x :: y :: z :: xs) →
  (x < y < z) = false ∧ (z < y < x) = false.
Proof.
rewrite is_alt_cons2 /=.
case/orP ⇒ /andP [Hxy].
- case/andP ⇒ Hzy _.
  split.
  + by rewrite Hxy /= ltnNge ltnW.
  + by rewrite Hzy /= ltnNge (ltnW Hxy).
- case/andP ⇒ Hyz _.
  split.
  + by rewrite ltnNge (ltnW Hxy).
  + apply/andP⇒ -[Hzy _].
    by have := ltn_trans Hyz Hzy; rewrite ltnn.
Qed.

Strict-monotone base case for the upper bound: any alternating subseq of a strictly ascending seq has length at most 2.


Section SlotInterval.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

slot_iv i j is the set of descent slots k : 'I_n.+1 whose underlying nat satisfies val i ≤ val k < val j. Indexes the "slot interval" between positions i and j.
Definition slot_iv (i j : 'I_n.+2) : {set 'I_n.+1} :=
  [set k : 'I_n.+1 | (val i ≤ val k) && (val k < val j)].

Membership in slot_iv i j unfolded to the val inequalities.
Lemma mem_slot_iv (i j : 'I_n.+2) (k : 'I_n.+1) :
  (k \in slot_iv i j) = (val i ≤ val k) && (val k < val j).
Proof. by rewrite inE. Qed.

Cardinality of the slot interval: #|slot_iv i j| = val j - val i, when val j ≤ n.+1.
End SlotInterval.

Section InterTurn.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Constancy of the descent indicator on a turn-free slot interval: if no turning point of s lies in slot range [val i, val j)], then [is_descent s k1 = is_descent s k2] for all slots [k1, k2] in the range. Used to derive monotone behavior of [s] on turn-free zones.
Lemma slot_descent_const s (i j : 'I_n.+2) :
  (∀ t : 'I_n, val i ≤ (val t).+1 < val j → ~~ is_turn s t) →
  ∀ (k1 k2 : 'I_n.+1),
    val i ≤ val k1 → val k1 ≤ val k2 → val k2 < val j →
    is_descent s k1 = is_descent s k2.
Proof.
move⇒ Hnoturn k1 k2 Hi1 H12 H2j.
move: H12 Hi1.
elim: (val k2 - val k1) {-2}k1 (refl_equal (val k2 - val k1)) ⇒
      [|d IH] k1' Hd H12 Hi1.
- move/eqP: Hd; rewrite subn_eq0 ⇒ Hk21.
  have : val k1' = val k2 by apply/eqP; rewrite eqn_leq H12 Hk21.
  by move⇒ /val_inj →.
- have Hk1lt : val k1' < val k2 by rewrite -subn_gt0 Hd.
  have Hk1ord : val k1' < n.
    by have := ltn_ord k2; rewrite ltnS ⇒ Hk2; rewrite (leq_trans Hk1lt).
  pose t : 'I_n := Ordinal Hk1ord.
  have Ht : val i ≤ (val t).+1 < val j.
    apply/andP; split; first by rewrite (leq_trans Hi1).
    by rewrite (leq_trans _ H2j).
  have := Hnoturn t Ht.
  rewrite /is_turn negb_add ⇒ /eqP Hd1.
  have Hk1eq : (widen_ord (leqnSn n) t : 'I_n.+1) = k1' by apply: val_inj.
  rewrite Hk1eq in Hd1; rewrite Hd1.
  have HSk1 : val (lift ord0 t : 'I_n.+1) = (val k1').+1
    by rewrite /= /bump /= add1n.
  apply: (IH (lift ord0 t)).
  - rewrite HSk1; apply: succn_inj.
    by rewrite subnSK // Hd.
  - by rewrite HSk1.
  - by rewrite HSk1 (leq_trans Hi1).
Qed.

Constant-descent implies monotonicity: if is_descent s k = b for all slots k in [val p, val q)], then [s] is monotone on positions [(p, q)]: ascending if [b = false], descending if [b = true].
Lemma constant_descent_monotone s (p q : 'I_n.+2) (b : bool) :
  val p < val q →
  (∀ k : 'I_n.+1, val p ≤ val k < val q → is_descent s k = b) →
  if b then val (s q) < val (s p) else val (s p) < val (s q).
Proof.
move⇒ Hpq Hconst.
move: q Hpq Hconst.
elim: (n.+2 - val p) {-2}p (refl_equal (n.+2 - val p)) ⇒
      [|d IH] p' Hd q Hpq Hconst.
  have Hq2 : val q < n.+2 by exact: ltn_ord.
  move/eqP: Hd; rewrite subn_eq0 ⇒ Hp'.
  by have := leq_ltn_trans (leq_trans Hp' (ltnW Hpq)) Hq2; rewrite ltnn.
have Hp'lt : val p' < n.+1.
  by rewrite -ltnS; apply: leq_trans (ltn_ord q).
pose k0 : 'I_n.+1 := Ordinal Hp'lt.
have Hwidp : (widen_ord (leqnSn n.+1) k0 : 'I_n.+2) = p' by apply: val_inj.
case: (eqVneq (val q) (val p').+1) ⇒ [Hpq1|Hne].
- have Hkrange : val p' ≤ val k0 < val q by rewrite /= leqnn /= Hpq1.
  have Hkdesc := Hconst k0 Hkrange.
  rewrite /is_descent in Hkdesc.
  have Hliftq : (lift ord0 k0 : 'I_n.+2) = q.
    by apply: val_inj ⇒ /=; rewrite /bump /= add1n.
  rewrite Hwidp Hliftq in Hkdesc.
  have Hpqne : p' != q by rewrite -val_eqE neq_ltn Hpq.
  have Hspqne : s p' != s q by apply: contra_neq Hpqne ⇒ /perm_inj.
  have Hvspqne : val (s p') != val (s q) by rewrite val_eqE.
  have Hsd : (val (s q) < val (s p'))%N = b by [].
  case Eb : b Hsd ⇒ Hsd /=; first by [].
  rewrite -[s p' < s q]/(val (s p') < val (s q))%N.
  rewrite ltn_neqAle leqNgt Hsd /=.
  by rewrite Hvspqne.
- have HqGtSp : (val p').+1 < val q by rewrite ltn_neqAle eq_sym Hne /= Hpq.
  pose pmid : 'I_n.+2 := lift ord0 k0.
  have Hpmid : val pmid = (val p').+1 by rewrite /= /bump /= add1n.
  have Hd' : n.+2 - val pmid = d.
    rewrite Hpmid; apply: succn_inj.
    have Hp'2 : val p' < n.+2 by exact: ltn_ord.
    by rewrite subnSK // Hd.
  have Hpmidq : val pmid < val q by rewrite Hpmid.
  have Hslot1 : val p' ≤ val k0 < val q.
    by rewrite /= leqnn (ltn_trans _ HqGtSp).
  have Hd1 := Hconst k0 Hslot1.
  rewrite /is_descent Hwidp in Hd1.
  have Hliftpmid : (lift ord0 k0 : 'I_n.+2) = pmid by [].
  rewrite Hliftpmid in Hd1.
  have Hsubconst : ∀ k : 'I_n.+1,
                     val pmid ≤ val k < val q → is_descent s k = b.
    move⇒ k /andP [Hk1 Hk2].
    apply: Hconst.
    rewrite Hk2 andbT.
    by rewrite (leq_trans _ Hk1) // Hpmid leqnSn.
  have IHmid := IH pmid Hd' q Hpmidq Hsubconst.
  have Hpmidne : pmid != p'.
    by rewrite -val_eqE Hpmid eqn_leq leqNgt ltnSn /=.
  have Hspmidne : s pmid != s p' by apply: contra_neq Hpmidne ⇒ /perm_inj.
  have Hvne1 : val (s pmid) != val (s p') by rewrite val_eqE.
  case Eb : b Hd1 IHmid ⇒ Hd1 IHmid /=.
  + have Hd1' : (val (s pmid) < val (s p'))%N by [].
    have IHmid' : (val (s q) < val (s pmid))%N by [].
    by apply: ltn_trans IHmid' Hd1'.
  + have HX1 : ~~ (val (s pmid) < val (s p'))%N by rewrite Hd1.
    have Hd1' : (val (s p') < val (s pmid))%N.
      by rewrite ltn_neqAle leqNgt HX1 /=; rewrite eq_sym Hvne1.
    have IHmid' : (val (s pmid) < val (s q))%N by [].
    rewrite -[s p' < s q]/(val (s p') < val (s q))%N.
    by apply: ltn_trans Hd1' IHmid'.
Qed.

Direction transport across a turn-free slot range: if no turning point lies in [val i, val j)], then the [s]-comparison direction on any sub-pair [(p, q)] inside [[i, j]] matches the boundary direction at [(i, j)].
Lemma inter_turn_monotone s (i j : 'I_n.+2) :
  val i < val j →
  (∀ t : 'I_n, val i ≤ (val t).+1 < val j → ~~ is_turn s t) →
  ∀ (p q : 'I_n.+2),
    val i ≤ val p → val p < val q → val q ≤ val j →
    (val (s p) < val (s q))%N = (val (s i) < val (s j))%N.
Proof.
move⇒ Hij Hnoturn p q Hip Hpq Hqj.
have Hjle : val i < n.+1.
  by have := ltn_ord j; rewrite ltnS ⇒ Hj2; rewrite (leq_trans Hij).
pose k0 : 'I_n.+1 := Ordinal Hjle.
have Hk0range : val i ≤ val k0 < val j by rewrite /= leqnn /= Hij.
pose b := is_descent s k0.
have Hconst_ij : ∀ k : 'I_n.+1,
                   val i ≤ val k < val j → is_descent s k = b.
  move⇒ k /andP [Hki Hkj].
  case: (leqP (val k0) (val k)) ⇒ Hkk0.
  - rewrite /b /=.
    by apply: esym; apply: (slot_descent_const Hnoturn) ⇒ //=.
  - apply: (slot_descent_const Hnoturn) ⇒ //=.
    exact: ltnW.
have Hconst_pq : ∀ k : 'I_n.+1,
                   val p ≤ val k < val q → is_descent s k = b.
  move⇒ k /andP [Hkp Hkq].
  apply: Hconst_ij.
  by rewrite (leq_trans Hip Hkp) /= (leq_trans Hkq).
have Hmono_ij := constant_descent_monotone Hij Hconst_ij.
have Hmono_pq := constant_descent_monotone Hpq Hconst_pq.
case Eb : b Hmono_ij Hmono_pq ⇒ Hmono_ij Hmono_pq /=.
- rewrite ltnNge (ltnW Hmono_pq) /=.
  by rewrite ltnNge (ltnW Hmono_ij) /=.
- by rewrite Hmono_pq Hmono_ij.
Qed.

Existence of a witness turn for any sign flip: if three positions i < j < k have an s-comparison flip across the middle, then some turning point of s lies in the slot interval [val i, val k)].
End InterTurn.





Section UpperBound.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

turn_iv s a b is the set of turning points t : 'I_n of s whose witness position (val t).+1 lies in the half-open interval [a, b)].
Definition turn_iv s (a b : nat) : {set 'I_n} :=
  [set t : 'I_n | is_turn s t && (a ≤ (val t).+1 < b)].

Membership in turn_iv s a b unfolded to its conjunction. turn_iv s a b is a subset of the global turn set of s.
Lemma turn_iv_subset s a b :
  turn_iv s a b \subset [set t : 'I_n | is_turn s t].
Proof. by apply/subsetP ⇒ t; rewrite !inE; case/andP ⇒ →. Qed.

Cardinality bound: #|turn_iv s a b| ≤ turn_count s. Additivity of turn_iv cardinality on a split point b: #|turn_iv s a c| = #|turn_iv s a b| + #|turn_iv s b c| when a ≤ b ≤ c.

End UpperBound.



Hamming-style triangle inequality on three booleans: a XOR c ≤ (a XOR b) + (b XOR c). Building block for the flip-count monotonicity arguments.
Lemma bool_triangle (a b c : bool) : (a (+) c) ≤ (a (+) b) + (b (+) c).
Proof. by case: a; case: b; case: c. Qed.

Triangle inequality for XOR of strict nat comparisons, used to bound the flip count when an element is inserted between two others. Exploits the transitivity / total-order structure of < on nats. Mirror variant of triangle_xor_nat_g with the middle position on the left. Used for "insert at front" reductions in flip count.
Lemma triangle_xor_nat (w y z r : nat) :
  (w < z) (+) (z < r) ≤ (w < y) (+) (y < z) + ((y < z) (+) (z < r)).
Proof.
case Hwz : (w < z)%N; case Hzr : (z < r)%N; rewrite /= ?addn0 ?addn1.
- exact: leq0n.
- case Hwy : (w < y)%N; case Hyz : (y < z)%N; rewrite //=.
  move/negbT: Hwy; rewrite -leqNgt ⇒ Hyw.
  move/negbT: Hyz; rewrite -leqNgt ⇒ Hzy.
  have Hwz' : ~~ (w < z)%N by rewrite -leqNgt (leq_trans Hzy Hyw).
  by rewrite Hwz in Hwz'.
- case Hwy : (w < y)%N; case Hyz : (y < z)%N; rewrite //=.
  have Hwz' : (w < z)%N by exact: ltn_trans Hwy Hyz.
  by rewrite Hwz in Hwz'.
- exact: leq0n.
Qed.

Front-insertion monotonicity for flip_count on a pairmap: inserting one element at the front never decreases the flip count. Step 1 building block for flip_count_pairmap_insert_anywhere.
Lemma flip_count_pairmap_insert (a y : nat) (xs : seq nat) :
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a xs) ≤
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (y :: xs)).
Proof.
case: xs ⇒ [|x xs] /=.
- by rewrite /flip_count /= big_nil.
- case Exs : xs ⇒ [|x' xs'] /=.
  + rewrite /flip_count /= !big_cons big_nil !addn0.
    by case: ((a < y)%N (+) (y < x)%N).
  + rewrite /flip_count /= !big_cons.
    rewrite addnA leq_add2r.
    exact: (triangle_xor_nat a y x x').
Qed.

Inductive step helper for flip_count_pairmap_insert_anywhere: combines the IH bound s1 ≤ ... + s2 with a structural matching condition to handle the four (x < z) = (y < z) cases uniformly.
Lemma flip_step_helper (a x y z : nat) (s1 s2 : nat) :
  s1 ≤ ((x < y) (+) (y < z)) + s2 →
  ((x < z) = (y < z) → s1 = s2) →
  (a < x) (+) (x < z) + s1 ≤ (a < x) (+) (x < y) + ((x < y) (+) (y < z) + s2).
Proof.
move⇒ IHv Hsame.
case Hxz : (x<z)%N; case Hyz : (y<z)%N.
- have Hs : s1 = s2 by apply: Hsame; rewrite Hxz Hyz.
  rewrite Hs addnA leq_add2r.
  exact: bool_triangle.
- have Hxy : (x < y)%N.
    move/negbT: Hyz; rewrite -leqNgt ⇒ Hzy.
    have Hxz' : (x<z)%N by rewrite Hxz.
    exact: leq_trans Hxz' Hzy.
  rewrite Hxy /=.
  rewrite leq_add2l.
  by rewrite Hxy Hyz /= in IHv.
- have Hyx : (x < y)%N = false.
    move/negbT: Hxz; rewrite -leqNgt ⇒ Hzx.
    have Hyz' : (y<z)%N by rewrite Hyz.
    have Hyx' : (y < x)%N by exact: leq_trans Hyz' Hzx.
    apply/negbTE; rewrite -leqNgt; exact: ltnW.
  rewrite Hyx /=.
  rewrite Hyx Hyz /= in IHv.
  rewrite leq_add2l.
  exact: IHv.
- have Hs : s1 = s2 by apply: Hsame; rewrite Hxz Hyz.
  rewrite Hs addnA leq_add2r.
  exact: bool_triangle.
Qed.

Insertion-anywhere monotonicity for flip_count on a pairmap: inserting one element at any position never decreases the flip count. Generalizes flip_count_pairmap_insert to interior positions.
Lemma flip_count_pairmap_insert_anywhere (xs ys : seq nat) (y : nat) (a : nat) :
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (xs ++ ys)) ≤
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (xs ++ y :: ys)).
Proof.
move: a; elim: xs ⇒ [|x xs IH] a /=.
- exact: flip_count_pairmap_insert.
- have IHv := IH x.
  case Exs : xs IHv ⇒ [|x' xs'] IHv.
  + rewrite /= in IHv |- ×.
    case Eys : ys IHv ⇒ [|z ys'] IHv.
    × rewrite /flip_count /= !big_cons big_nil !addn0.
      by case: ((a < x)%N (+) (x < y)%N).
    × rewrite /flip_count /= !big_cons in IHv |- ×.
      apply: flip_step_helper.
      -- exact: IHv.
      -- by move⇒ →.
  + rewrite /=.
    rewrite /flip_count /= !big_cons.
    rewrite leq_add2l.
    rewrite /= in IHv.
    exact: IHv.
Qed.

Sign-seq front-insertion monotonicity: inserting y at the front of xs never decreases flip_count (sign_seq _).
Lemma flip_count_sign_seq_insert_front (y : nat) (xs : seq nat) :
  flip_count (sign_seq xs) ≤ flip_count (sign_seq (y :: xs)).
Proof.
case: xs ⇒ [|x xs] /=.
  by [].
case: xs ⇒ [|x' xs'] /=.
  by rewrite /flip_count /= big_nil.
rewrite /flip_count /= !big_cons.
by case: ((y < x)%N (+) (x < x')%N).
Qed.



Strict-subseq dropping: if xs is a proper subseq of ys, some index i of ys can be removed while still containing xs.
Lemma subseq_drop_extra (xs ys : seq nat) :
  subseq xs ys → size xs < size ys →
  ∃ i, i < size ys ∧
    subseq xs (take i ys ++ drop i.+1 ys).
Proof.
elim: ys xs ⇒ [|y ys IH] xs //=.
case: xs ⇒ [|x xs] /=.
- move⇒ _ _.
  ∃ 0; split ⇒ //=.
  by rewrite drop0 sub0seq.
- case Eeq : (x == y) ⇒ Hsub Hsz.
  + have Hsz' : size xs < size ys by [].
    have [i [Hi Hsubi]] := IH xs Hsub Hsz'.
    ∃ i.+1; split ⇒ //=.
    by rewrite Eeq.
  + ∃ 0; split ⇒ //=.
    by rewrite drop0.
Qed.

Size of ys with element at position i removed: (size ys).-1.
Lemma size_take_drop_skip (i : nat) (ys : seq nat) :
  i < size ys → size (take i ys ++ drop i.+1 ys) = (size ys).-1.
Proof.
move⇒ Hi.
rewrite size_cat size_take size_drop Hi.
case Hsz : (size ys) Hi ⇒ [|m] Hi //=.
rewrite subSS.
have Him : i ≤ m by rewrite -ltnS.
by rewrite subnKC.
Qed.

Subseq monotonicity for flip_count on a pairmap: if xs is a subseq of ys, its flip count is at most that of ys. Iterates flip_count_pairmap_insert_anywhere across the size difference.
Lemma flip_count_pairmap_le_subseq (xs ys : seq nat) :
  subseq xs ys →
  ∀ a : nat,
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a xs) ≤
  flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a ys).
Proof.
move⇒ Hsub.
have [k Hk] : ∃ k, size ys = size xs + k.
  by ∃ (size ys - size xs); rewrite addnC subnK //; exact: size_subseq.
move: xs ys Hsub Hk.
elim: k ⇒ [|k IH] xs ys Hsub Hk a.
- rewrite addn0 in Hk.
  have HL := size_subseq_leqif Hsub.
  have Heq : xs = ys.
    by case: HL ⇒ _ Hiff; apply/eqP; rewrite -Hiff Hk.
  by rewrite Heq.
- have Hszlt : size xs < size ys by rewrite Hk addnS ltnS leq_addr.
  have [i [Hi Hsubi]] := subseq_drop_extra Hsub Hszlt.
  pose ys' := take i ys ++ drop i.+1 ys.
  have Hsz' : size ys' = size xs + k.
    have := size_take_drop_skip Hi.
    rewrite -/ys' Hk addnS /=.
    by case Hsz0: (size ys) ⇒ [|m] //= [->].
  have IHv := IH xs ys' Hsubi Hsz' a.
  apply: leq_trans IHv _.
  have Hys_split : ys = take i ys ++ (nth 0 ys i :: drop i.+1 ys).
    rewrite -[in LHS](cat_take_drop i ys).
    congr (_ ++ _).
    by rewrite (drop_nth 0 Hi).
  rewrite [X in _ ≤ flip_count (pairmap _ _ X)]Hys_split.
  exact: flip_count_pairmap_insert_anywhere.
Qed.

Subseq monotonicity specialized to sign_seq: if xs is a subseq of ys, then flip_count (sign_seq xs) ≤ flip_count (sign_seq ys). Used in as_perm_max_upper to bound subseq alternation by the global flip count.
Lemma flip_count_sign_seq_le_subseq (xs ys : seq nat) :
  subseq xs ys →
  flip_count (sign_seq xs) ≤ flip_count (sign_seq ys).
Proof.
move⇒ Hsub.
case: xs Hsub ⇒ [|x xs] Hsub /=.
- by [].
- case: ys Hsub ⇒ [|y ys] Hsub.
  + by move: Hsub; rewrite /= ⇒ /eqP.
  + rewrite /sign_seq /=.
    case Eeq : (x == y) Hsub ⇒ Hsub.
    × move/eqP: Eeq ⇒ Eeq; rewrite Eeq in Hsub ×.
      have Hsub' : subseq xs ys.
        by move: Hsub; rewrite /= eq_refl.
      exact: flip_count_pairmap_le_subseq Hsub' y.
    × have Hsubys : subseq (x :: xs) ys.
        by move: Hsub; rewrite /= Eeq.
      have Hstep1 := flip_count_sign_seq_insert_front y (x :: xs).
      rewrite /sign_seq /= in Hstep1.
      have Hstep2 :
        flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) y (x :: xs)) ≤
        flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) y ys).
        exact: flip_count_pairmap_le_subseq Hsubys y.
      exact: leq_trans Hstep1 Hstep2.
Qed.


is_alt_bool_aux a xs checks alternation of a boolean seq with a leading "previous" element a: every adjacent pair must XOR to true.
Fixpoint is_alt_bool_aux (a : bool) (xs : seq bool) : bool :=
  match xs with
  | [::] ⇒ true
  | b :: rest ⇒ (a (+) b) && is_alt_bool_aux b rest
  end.

is_alt_bool xs holds when the boolean seq xs is fully alternating: every adjacent pair differs.
Definition is_alt_bool (xs : seq bool) : bool :=
  match xs with
  | [::] ⇒ true
  | a :: rest ⇒ is_alt_bool_aux a rest
  end.

Fully alternating boolean seqs maximize flip count: flip_count xs = (size xs).-1 when is_alt_bool xs holds.
Lemma flip_count_is_alt_bool xs :
  is_alt_bool xs → flip_count xs = (size xs).-1.
Proof.
case: xs ⇒ [|a xs] //=.
elim: xs a ⇒ [|b xs IH] a //=.
  by rewrite /flip_count /= big_nil.
case/andP ⇒ Hab Halt.
rewrite /flip_count /= big_cons Hab /=.
have IHv := IH b Halt.
rewrite /flip_count /= in IHv.
by rewrite IHv add1n.
Qed.

The sign seq of an is_alt nat seq is itself fully alternating as a boolean seq: every adjacent direction pair differs.
Lemma sign_seq_is_alt xs :
  is_alt xs → 2 ≤ size xs → is_alt_bool (sign_seq xs).
Proof.
case: xs ⇒ [|x [|y rest]] //=.
move⇒ Halt _.
move: x y Halt; elim: rest ⇒ [|z rest IH] x y //= Halt.
case/orP: Halt ⇒ /andP [Hcmp Halt].
- case/andP: Halt ⇒ Hzy Halt2.
  rewrite Hcmp /=.
  have Hyzn : ~~ (y < z) by rewrite -leqNgt ltnW.
  rewrite (negbTE Hyzn) /=.
  have Halt' :
    (y < z) && alt_aux false z rest || (z < y) && alt_aux true z rest.
    by rewrite Hzy Halt2 /= orbT.
  have IHv := IH y z Halt'.
  by move: IHv; rewrite (negbTE Hyzn).
- case/andP: Halt ⇒ Hyz Halt2.
  have Hxyn : ~~ (x < y) by rewrite -leqNgt ltnW.
  rewrite (negbTE Hxyn) Hyz /=.
  have Halt' :
    (y < z) && alt_aux false z rest || (z < y) && alt_aux true z rest.
    by rewrite Hyz Halt2 /=.
  have IHv := IH y z Halt'.
  by move: IHv; rewrite Hyz.
Qed.

Flip-count formula for alternating seqs: an is_alt seq of size at least 2 has flip_count (sign_seq xs) = (size xs).-2. Used in as_perm_max_upper to reduce alternation to flip-count bounds.
Lemma is_alt_flip_count xs :
  is_alt xs → 2 ≤ size xs → flip_count (sign_seq xs) = (size xs).-2.
Proof.
move⇒ Halt Hsz.
have := flip_count_is_alt_bool (sign_seq_is_alt Halt Hsz).
rewrite size_sign_seq.
by case: xs Halt Hsz ⇒ [|x [|y [|z rest]]] //= _ _ →.
Qed.


Section UpperBoundAssembly.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Sorting the enumeration of a {set 'I_n.+2} by val gives a strictly sorted seq, since the underlying enumeration is duplicate-free.
Lemma sort_enum_strict_sorted (I : {set 'I_n.+2}) :
  sorted (fun a b : 'I_n.+2 ⇒ val a < val b)
         (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)).
Proof.
have Hsort := sort_sorted (T := 'I_n.+2)
  (fun a b ⇒ leq_total (val a) (val b)) (enum I).
have Huniq : uniq (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)).
  by rewrite sort_uniq enum_uniq.
move: Hsort Huniq.
elim: (sort _ _) ⇒ [|a [|b xs] IH] //= /andP [Hab Hsorted] /andP [Han Hu].
have Hab' : val a < val b.
  rewrite ltn_neqAle Hab andbT.
  apply/eqP ⇒ Hva.
  have Hab2 : a = b by apply: val_inj.
  by move: Han; rewrite Hab2 inE eq_refl.
rewrite Hab' /=.
exact: IH.
Qed.


End UpperBoundAssembly.



Section LowerBound.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

turn_inj t injects an interior position t : 'I_n into { 'I_n.+2 } at the offset (val t).+1. Used to construct the witness set turn_witness for the lower-bound construction.
Definition turn_inj (t : 'I_n) : 'I_n.+2 :=
  lift ord0 (widen_ord (leqnSn n) t).

Underlying value of turn_inj t: (val t).+1.
Lemma val_turn_inj (t : 'I_n) : val (turn_inj t) = (val t).+1.
Proof. by rewrite /turn_inj /= /bump /= add1n. Qed.

turn_inj is injective.
Lemma turn_inj_inj : injective turn_inj.
Proof.
move⇒ a b /(congr1 val); rewrite !val_turn_inj ⇒ /succn_inj.
exact: val_inj.
Qed.

turn_witness s is the explicit alternating-subseq witness: {ord0; ord_max} ∪ {turn_inj t | t turning point of s}. Has cardinality (turn_count s).+2; its pick_seq is the alternating subsequence of length (turn_count s).+2.
Definition turn_witness s : {set 'I_n.+2} :=
  ord0 |: (ord_max |: [set turn_inj t | t in [set i : 'I_n | is_turn s i]]).

Image of turn_inj on the turn set has cardinality turn_count s.
Lemma card_turn_image s :
  #|[set turn_inj t | t in [set i : 'I_n | is_turn s i]]| = turn_count s.
Proof. by rewrite card_imset //; apply: turn_inj_inj. Qed.

Range bound: any element of the turn_inj-image of the turn set has 0 < val x ≤ n; in particular, neither ord0 nor ord_max.
Lemma turn_image_lt_max s (x : 'I_n.+2) :
  x \in [set turn_inj t | t in [set i : 'I_n | is_turn s i]] →
  0 < val x ≤ n.
Proof.
case/imsetP ⇒ t _ →.
rewrite val_turn_inj /=.
by have := ltn_ord t.
Qed.

ord0 is not in the turn_inj-image of the turn set.
Lemma ord0_notin_turn_image s :
  (ord0 : 'I_n.+2) \notin [set turn_inj t | t in [set i : 'I_n | is_turn s i]].
Proof.
apply/negP ⇒ /turn_image_lt_max /andP [].
by rewrite (_ : val (ord0 : 'I_n.+2) = 0).
Qed.

ord_max is not in the turn_inj-image of the turn set.
Lemma ord_max_notin_turn_image s :
  (ord_max : 'I_n.+2) \notin
    [set turn_inj t | t in [set i : 'I_n | is_turn s i]].
Proof.
apply/negP ⇒ /turn_image_lt_max /andP [_].
rewrite (_ : val (ord_max : 'I_n.+2) = n.+1) //.
by rewrite ltnn.
Qed.

Trivial distinction: ord0 and ord_max differ in {'I_n.+2}.
Lemma ord0_neq_ord_max : (ord0 : 'I_n.+2) != ord_max.
Proof. by rewrite -val_eqE /=. Qed.

Cardinality of the lower-bound witness set: #|turn_witness s| = (turn_count s).+2.
Lemma card_turn_witness s :
  #|turn_witness s| = (turn_count s).+2.
Proof.
rewrite /turn_witness.
rewrite cardsU1 in_setU1 (negbTE ord0_neq_ord_max) /=.
rewrite (negbTE (ord0_notin_turn_image s)) /=.
rewrite cardsU1 (negbTE (ord_max_notin_turn_image s)) /=.
by rewrite card_turn_image add1n add1n.
Qed.

Strict-left variant of slot_descent_const: hypothesis only excludes turns with witness STRICTLY greater than val i. Used in the lower-bound construction where i itself may be a turn position.
Lemma slot_descent_const_strict s (i j : 'I_n.+2) :
  (∀ t : 'I_n, val i < (val t).+1 < val j → ~~ is_turn s t) →
  ∀ (k1 k2 : 'I_n.+1),
    val i ≤ val k1 → val k1 ≤ val k2 → val k2 < val j →
    is_descent s k1 = is_descent s k2.
Proof.
move⇒ Hnoturn k1 k2 Hi1 H12 H2j.
move: H12 Hi1.
elim: (val k2 - val k1) {-2}k1 (refl_equal (val k2 - val k1)) ⇒
      [|d IH] k1' Hd H12 Hi1.
- move/eqP: Hd; rewrite subn_eq0 ⇒ Hk21.
  have : val k1' = val k2 by apply/eqP; rewrite eqn_leq H12 Hk21.
  by move⇒ /val_inj →.
- have Hk1lt : val k1' < val k2 by rewrite -subn_gt0 Hd.
  have Hk1ord : val k1' < n.
    by have := ltn_ord k2; rewrite ltnS ⇒ Hk2; rewrite (leq_trans Hk1lt).
  pose t : 'I_n := Ordinal Hk1ord.
  have Ht : val i < (val t).+1 < val j.
    apply/andP; split; first by apply: leq_ltn_trans Hi1 _.
    by rewrite (leq_trans _ H2j).
  have := Hnoturn t Ht.
  rewrite /is_turn negb_add ⇒ /eqP Hd1.
  have Hk1eq : (widen_ord (leqnSn n) t : 'I_n.+1) = k1' by apply: val_inj.
  rewrite Hk1eq in Hd1; rewrite Hd1.
  have HSk1 : val (lift ord0 t : 'I_n.+1) = (val k1').+1
    by rewrite /= /bump /= add1n.
  apply: (IH (lift ord0 t)).
  - rewrite HSk1; apply: succn_inj.
    by rewrite subnSK // Hd.
  - by rewrite HSk1.
  - by rewrite HSk1 (leq_trans Hi1).
Qed.

Strict-left variant of inter_turn_monotone: monotone direction transport with a strict lower-bound hypothesis on turn witnesses.
Lemma inter_turn_monotone_strict s (i j : 'I_n.+2) :
  val i < val j →
  (∀ t : 'I_n, val i < (val t).+1 < val j → ~~ is_turn s t) →
  ∀ (p q : 'I_n.+2),
    val i ≤ val p → val p < val q → val q ≤ val j →
    (val (s p) < val (s q))%N = (val (s i) < val (s j))%N.
Proof.
move⇒ Hij Hnoturn p q Hip Hpq Hqj.
have Hjle : val i < n.+1.
  by have := ltn_ord j; rewrite ltnS ⇒ Hj2; rewrite (leq_trans Hij).
pose k0 : 'I_n.+1 := Ordinal Hjle.
have Hk0range : val i ≤ val k0 < val j by rewrite /= leqnn /= Hij.
pose b := is_descent s k0.
have Hconst_ij : ∀ k : 'I_n.+1,
                   val i ≤ val k < val j → is_descent s k = b.
  move⇒ k /andP [Hki Hkj].
  case: (leqP (val k0) (val k)) ⇒ Hkk0.
  - rewrite /b /=.
    by apply: esym; apply: (slot_descent_const_strict Hnoturn) ⇒ //=.
  - apply: (slot_descent_const_strict Hnoturn) ⇒ //=.
    exact: ltnW.
have Hconst_pq : ∀ k : 'I_n.+1,
                   val p ≤ val k < val q → is_descent s k = b.
  move⇒ k /andP [Hkp Hkq].
  apply: Hconst_ij.
  by rewrite (leq_trans Hip Hkp) /= (leq_trans Hkq).
have Hmono_ij := constant_descent_monotone Hij Hconst_ij.
have Hmono_pq := constant_descent_monotone Hpq Hconst_pq.
case Eb : b Hmono_ij Hmono_pq ⇒ Hmono_ij Hmono_pq /=.
- rewrite ltnNge (ltnW Hmono_pq) /=.
  by rewrite ltnNge (ltnW Hmono_ij) /=.
- by rewrite Hmono_pq Hmono_ij.
Qed.

Direction LEFT of a turn witness: when b = turn_inj t and no interior turn lies in (val a, val b), the direction s a vs s b equals ~~ is_descent s (widen_ord t) (the "left half" descent indicator at slot t).
Lemma dir_left_of_turn s (a b : 'I_n.+2) (t : 'I_n) :
  b = turn_inj t → val a ≤ val t →
  (∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t') →
  (val (s a) < val (s b))%N = ~~ is_descent s (widen_ord (leqnSn n) t).
Proof.
move⇒ Hbeq Hat Hno.
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Htlt2 : val t < n.+2 by rewrite (leq_trans (ltn_ord t)) //; apply: ltnW.
pose p' : 'I_n.+2 := Ordinal Htlt2.
have Hp'val : val p' = val t by [].
have Hap' : val a ≤ val p' by rewrite Hp'val.
have Hp'b : val p' < val b by rewrite Hp'val Hbval.
have Hbb : val b ≤ val b by [].
have Hab : val a < val b by rewrite (leq_ltn_trans Hap' Hp'b).
rewrite -(inter_turn_monotone_strict Hab Hno Hap' Hp'b Hbb).
have Hwt : (widen_ord (leqnSn n.+1) (widen_ord (leqnSn n) t) : 'I_n.+2) = p'
  by apply: val_inj.
have Hlt : (lift ord0 (widen_ord (leqnSn n) t) : 'I_n.+2) = b
  by apply: val_inj ⇒ /=; rewrite Hbval /bump /= add1n.
have := not_is_descentE s (widen_ord (leqnSn n) t).
by rewrite Hwt Hlt ⇒ →.
Qed.

Direction RIGHT of a turn witness: dual of dir_left_of_turn; the direction s b vs s c equals ~~ is_descent s (lift ord0 t) (the "right half" descent indicator at slot t).
Lemma dir_right_of_turn s (b c : 'I_n.+2) (t : 'I_n) :
  b = turn_inj t → val b < val c →
  (∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t') →
  (val (s b) < val (s c))%N = ~~ is_descent s (lift ord0 t).
Proof.
move⇒ Hbeq Hbc Hno.
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Htn : val t < n by apply: ltn_ord.
have HtSlt2 : (val t).+2 < n.+2 by rewrite !ltnS.
pose c' : 'I_n.+2 := Ordinal HtSlt2.
have Hc'val : val c' = (val t).+2 by [].
have Hbc' : val b < val c' by rewrite Hbval Hc'val.
have Hbb : val b ≤ val b by [].
have Hc'c : val c' ≤ val c.
  by rewrite Hc'val -Hbval.
rewrite -(inter_turn_monotone_strict Hbc Hno Hbb Hbc' Hc'c).
have Hwt : (widen_ord (leqnSn n.+1) (lift ord0 t) : 'I_n.+2) = b.
  by apply: val_inj ⇒ /=; rewrite Hbval /bump /= add1n.
have Hlt : (lift ord0 (lift ord0 t) : 'I_n.+2) = c'.
  by apply: val_inj ⇒ /=; rewrite /bump /= !add1n.
have := not_is_descentE s (lift ord0 t).
by rewrite Hwt Hlt ⇒ →.
Qed.

Key adjacency lemma for the lower bound: at an interior witness b = turn_inj t flanked by neighbors a, c with no interior turns in the half-open intervals, the directions across (a, b) and (b, c) DIFFER (since t is a turning point). Used in triple_flip_pos_seq to verify the alternating property of pick_seq s (turn_witness s).
Lemma sign_flip_at_turn s (a b c : 'I_n.+2) (t : 'I_n) :
  is_turn s t → b = turn_inj t →
  val a ≤ val t → val b < val c →
  (∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t') →
  (∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t') →
  (val (s a) < val (s b))%N != (val (s b) < val (s c))%N.
Proof.
move⇒ Htn Hbeq Hat Hbc Hno_left Hno_right.
rewrite (dir_left_of_turn Hbeq Hat Hno_left).
rewrite (dir_right_of_turn Hbeq Hbc Hno_right).
move: Htn; rewrite /is_turn.
by case: (is_descent _ _); case: (is_descent _ _).
Qed.

End LowerBound.



uniq_adj xs holds when every adjacent pair in xs consists of distinct elements. Weaker than uniq, used to characterize when is_alt follows from sign-seq alternation.
Definition uniq_adj (xs : seq nat) : bool :=
  match xs with
  | [::] ⇒ true
  | x :: xs' ⇒ all (fun p ⇒ p.1 != p.2) (zip (x :: xs') xs')
  end.

Cons reduction for uniq_adj on a 2-prefix. Tail closure of uniq_adj. Head distinctness extracted from uniq_adj.
Lemma uniq_adj_head_neq x y rest :
  uniq_adj (x :: y :: rest) → x != y.
Proof. by case: rest ⇒ [|z r] /= /andP []. Qed.

For distinct nats, x < y iff ~~ (y < x); trichotomy in boolean form. Key reverse direction: an alternating boolean sign seq plus adjacent distinctness implies the alt_aux predicate. Building block for is_alt_from_sign.
Lemma alt_aux_from_sign x y xs :
  uniq_adj (x :: y :: xs) →
  is_alt_bool (sign_seq (x :: y :: xs)) →
  alt_aux (~~ (x < y)%N) y xs.
Proof.
elim: xs y x ⇒ [|z rest IH] y x /=.
  by [].
move⇒ Hu Hab.
have Hyz_ne : y != z by case/and3P: Hu.
have Huyz : uniq_adj (y :: z :: rest).
  by case: rest Hu {IH Hab} ⇒ [|w r] /=;
     case/and3P⇒ _ Hyz Hr; rewrite Hyz //=.
move: Hab ⇒ /=.
case/andP⇒ Hflip Hbabool.
have Hrec : alt_aux (~~ (y < z)%N) z rest by exact: IH.
move: Hrec.
have Hxy_yz : (x < y)%N (+) (y < z)%N by exact: Hflip.
case Exy : (x < y)%N Hxy_yz ⇒ Hxy_yz /=.
- have Hyz_false : (y < z)%N = false by case: (y < z)%N Hxy_yz.
  rewrite Hyz_false /= ⇒ →.
  by rewrite andbT ltn_neqAle leqNgt Hyz_false /= eq_sym Hyz_ne.
- have Hyz_true : (y < z)%N = true by case: (y < z)%N Hxy_yz.
  by rewrite Hyz_true /= ⇒ →.
Qed.

Triple-flip sufficient condition for sign-seq alternation: if every adjacent triple (js[i], js[i+1], js[i+2]) has flipping s-direction, then the sign seq of the s-image is alternating as a boolean seq.
Lemma sign_seq_alt_of_triple_flip n (s : {perm 'I_n.+2}) (js : seq 'I_n.+2) :
  (∀ i, i.+2 < size js →
     (val (s (nth ord0 js i)) < val (s (nth ord0 js i.+1)))%N
       != (val (s (nth ord0 js i.+1)) < val (s (nth ord0 js i.+2)))%N) →
  is_alt_bool (sign_seq [seq val (s j) | j <- js]).
Proof.
elim: js ⇒ [|x [|y [|z rest]]] // IH Htriples /=.
have Hrec_hyp : ∀ i, i.+2 < size [:: y, z & rest] →
  (val (s (nth ord0 [:: y, z & rest] i))
     < val (s (nth ord0 [:: y, z & rest] i.+1)))%N
     != (val (s (nth ord0 [:: y, z & rest] i.+1))
            < val (s (nth ord0 [:: y, z & rest] i.+2)))%N.
  by move⇒ i Hi; apply: (Htriples i.+1).
have Hrec := IH Hrec_hyp.
move: Hrec; rewrite /sign_seq /=.
move⇒ Hrec.
apply/andP; split; last exact: Hrec.
have H0 : 2 < size [:: x, y, z & rest] by [].
have := Htriples 0%N H0; rewrite /=.
by case: (val (s x) < _)%N; case: (val (s y) < _)%N.
Qed.

uniq_adj follows from full uniq for nat seqs.
Lemma uniq_adj_of_uniq (xs : seq nat) : uniq xs → uniq_adj xs.
Proof.
case: xs ⇒ [|x xs] //=.
elim: xs x ⇒ [|y rest IH] x //= /andP [Hx /andP [Hy Hu]].
have Hxy : x != y by apply: contraNneq Hx ⇒ ->; rewrite mem_head.
rewrite Hxy /=.
by apply: IH; rewrite Hy Hu.
Qed.

Main reverse characterization: is_alt xs follows from is_alt_bool (sign_seq xs) together with adjacent distinctness. Used to construct alternating subseqs from sign-flip witnesses.
Lemma is_alt_from_sign xs :
  uniq_adj xs → is_alt_bool (sign_seq xs) → is_alt xs.
Proof.
case: xs ⇒ [|x [|y rest]] // Hu Hab.
have Hxy_ne : x != y by exact: uniq_adj_head_neq Hu.
rewrite is_alt_cons2.
have Hrec := alt_aux_from_sign Hu Hab.
case Exy : (x < y)%N Hrec ⇒ /= Hrec.
  by rewrite Hrec.
by rewrite Hrec andbT ltn_neqAle leqNgt Exy /= eq_sym Hxy_ne.
Qed.


Section ExistenceLB.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

pos_seq s is the turn_witness s enumerated in ascending val order: the sorted seq of position indices in the lower-bound witness construction.
Definition pos_seq s : seq 'I_n.+2 :=
  sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum (turn_witness s)).

pos_seq s has length (turn_count s).+2.
Lemma size_pos_seq s : size (pos_seq s) = (turn_count s).+2.
Proof. by rewrite /pos_seq size_sort -cardE card_turn_witness. Qed.

pos_seq s is duplicate-free.
Lemma pos_seq_uniq s : uniq (pos_seq s).
Proof. by rewrite /pos_seq sort_uniq enum_uniq. Qed.

Definitional unfolding: pick_seq s (turn_witness s) equals the map of pos_seq s under val (s _).
Lemma pick_seq_pos_seq s :
  pick_seq s (turn_witness s) = [seq val (s j) | j <- pos_seq s].
Proof. by []. Qed.

pos_seq s is strictly sorted by val.
Lemma pos_seq_strict_sorted s :
  sorted (fun a b : 'I_n.+2 ⇒ val a < val b) (pos_seq s).
Proof. exact: sort_enum_strict_sorted. Qed.

Membership transfer: x \in pos_seq s iff x \in turn_witness s.
Lemma mem_pos_seq s (x : 'I_n.+2) :
  x \in pos_seq s = (x \in turn_witness s).
Proof. by rewrite /pos_seq mem_sort mem_enum. Qed.

Strict-sorted property: index-order in pos_seq s matches val-order.
Lemma pos_seq_val_lt s (i j : nat) :
  i < size (pos_seq s) → j < size (pos_seq s) → i < j →
  val (nth ord0 (pos_seq s) i) < val (nth ord0 (pos_seq s) j).
Proof.
move⇒ Hi Hj Hij.
have Htrans : transitive (fun a b : 'I_n.+2 ⇒ val a < val b).
  by move⇒ a b c; apply: ltn_trans.
exact: (sorted_ltn_nth Htrans ord0 (pos_seq_strict_sorted s)).
Qed.

Converse strict-sorted property: val-order forces index-order in pos_seq s.
Lemma pos_seq_val_lt_inv s (i j : nat) :
  i < size (pos_seq s) → j < size (pos_seq s) →
  val (nth ord0 (pos_seq s) i) < val (nth ord0 (pos_seq s) j) →
  i < j.
Proof.
move⇒ Hi Hj Hlt.
case: (ltngtP i j) Hlt ⇒ // Hij Hlt.
  by have := pos_seq_val_lt Hj Hi Hij; rewrite ltnNge ltnW.
by rewrite Hij ltnn in Hlt.
Qed.

Gap property: no element of pos_seq s has val strictly between consecutive entries pos_seq s i and pos_seq s i.+1.
Lemma no_inner_in_pos_seq s i (x : 'I_n.+2) :
  i.+1 < size (pos_seq s) →
  x \in pos_seq s →
  val (nth ord0 (pos_seq s) i) < val x →
  val x < val (nth ord0 (pos_seq s) i.+1) →
  False.
Proof.
move⇒ Hi Hin Hxa Hxb.
have Hi0 : i < size (pos_seq s) by exact: ltnW.
have /(nthP ord0) [j Hj Hxnth] := Hin.
rewrite -Hxnth in Hxa Hxb.
have H1 := pos_seq_val_lt_inv Hi0 Hj Hxa.
have H2 := pos_seq_val_lt_inv Hj Hi Hxb.
by have := leq_trans H2 H1; rewrite ltnn.
Qed.

First element of pos_seq s is ord0.
Lemma pos_seq_nth0 s : nth ord0 (pos_seq s) 0 = ord0.
Proof.
have Hsz : 0 < size (pos_seq s) by rewrite size_pos_seq.
have Hord0_in : (ord0 : 'I_n.+2) \in pos_seq s.
  by rewrite mem_pos_seq /turn_witness !inE eq_refl.
have /(nthP ord0) [k Hk Hk_eq] := Hord0_in.
case Ek : k Hk Hk_eq ⇒ [|k'] Hk Hk_eq.
  by [].
have Hk0lt : (0 < k'.+1)%N by [].
have := pos_seq_val_lt Hsz Hk Hk0lt.
rewrite Hk_eq /=.
by [].
Qed.

Last element of pos_seq s has value n.+1 (i.e., is ord_max).
Lemma pos_seq_last_val s :
  val (nth ord0 (pos_seq s) (turn_count s).+1) = n.+1.
Proof.
have Hszm1 : (turn_count s).+1 < size (pos_seq s) by rewrite size_pos_seq.
have Hord_max_in : (ord_max : 'I_n.+2) \in pos_seq s.
  by rewrite mem_pos_seq /turn_witness !inE eq_refl orbT.
have /(nthP ord0) [k Hk Hk_eq] := Hord_max_in.
have Hk_le : k ≤ (turn_count s).+1.
  rewrite leqNgt; apply/negP ⇒ Hk_gt.
  have Hsz_eq : size (pos_seq s) = (turn_count s).+2 by rewrite size_pos_seq.
  by have := Hk; rewrite Hsz_eq ltnS leqNgt Hk_gt.
case: (eqVneq k (turn_count s).+1) ⇒ [Heq|Hne].
  by rewrite -Heq Hk_eq.
have Hk_lt : k < (turn_count s).+1 by rewrite ltn_neqAle Hne.
have := pos_seq_val_lt Hk Hszm1 Hk_lt.
rewrite Hk_eq /= ⇒ Hcontr.
have Hbound : val (nth ord0 (pos_seq s) (turn_count s).+1) < n.+2
  by exact: ltn_ord.
by apply/eqP; rewrite eqn_leq; apply/andP; split;
  [have := Hbound; rewrite ltnS | apply: ltnW].
Qed.

Interior elements of pos_seq s (indices 0 < i < size - 1) are turn_inj-images of turning points: they correspond to actual turns of s.
Lemma interior_is_turn_inj s (i : nat) :
  0 < i → i.+1 < size (pos_seq s) →
  ∃ t : 'I_n, is_turn s t ∧ nth ord0 (pos_seq s) i = turn_inj t.
Proof.
move⇒ H0 Hi.
have Hi0 : i < size (pos_seq s) by exact: ltnW.
pose b := nth ord0 (pos_seq s) i.
have Hbin : b \in pos_seq s by apply: mem_nth.
rewrite mem_pos_seq /turn_witness !inE in Hbin.
case/orP: Hbin ⇒ [/eqP Hb_ord0|].
  exfalso.
  have Hsz_pos : 0 < size (pos_seq s) by rewrite size_pos_seq.
  have := pos_seq_val_lt Hsz_pos Hi0 H0.
  by rewrite pos_seq_nth0 -/b Hb_ord0.
case/orP ⇒ [/eqP Hb_ord_max|].
  exfalso.
  have Hsz_eq : size (pos_seq s) = (turn_count s).+2 by rewrite size_pos_seq.
  have Hi_lt : i < (turn_count s).+1 by have := Hi; rewrite Hsz_eq.
  have Hszm1 : (turn_count s).+1 < size (pos_seq s) by rewrite Hsz_eq.
  have := pos_seq_val_lt Hi0 Hszm1 Hi_lt.
  rewrite -/b Hb_ord_max pos_seq_last_val.
  by rewrite ltnn.
case/imsetP ⇒ t Hin Heq.
∃ t; split.
  by move: Hin; rewrite inE.
by [].
Qed.

Strict interior value bounds: 0 < val (pos_seq s i) < n.+1 for indices i strictly between the endpoints. Triple-flip property for adjacent triples in pos_seq s: directions across consecutive s-comparisons differ. The interior witness in each triple is a turning point, so sign_flip_at_turn applies.
Lemma triple_flip_pos_seq s i :
  i.+2 < size (pos_seq s) →
  (val (s (nth ord0 (pos_seq s) i)) < val (s (nth ord0 (pos_seq s) i.+1)))%N
    !=
    (val (s (nth ord0 (pos_seq s) i.+1))
     < val (s (nth ord0 (pos_seq s) i.+2)))%N.
Proof.
move⇒ Hi.
have Hi1 : i.+1 < size (pos_seq s) by exact: ltnW.
have Hi0 : i < size (pos_seq s) by do 2 apply: ltnW.
pose a := nth ord0 (pos_seq s) i.
pose b := nth ord0 (pos_seq s) i.+1.
pose c := nth ord0 (pos_seq s) i.+2.
have Hab : val a < val b by exact: pos_seq_val_lt.
have Hbc : val b < val c by exact: pos_seq_val_lt.
have [t [Htn Heqb]] := interior_is_turn_inj (i := i.+1) (ltn0Sn _) Hi.
have Hbeq : b = turn_inj t by [].
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Hat : val a ≤ val t.
  by rewrite -ltnS -Hbval.
have Hno_left :
  ∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t'.
  move⇒ t' /andP [Ht1 Ht2].
  apply/negP ⇒ Ht'turn.
  pose x := turn_inj t'.
  have Hxin : x \in pos_seq s.
    rewrite mem_pos_seq /turn_witness !inE.
    apply/orP; right; apply/orP; right.
    apply/imsetP; ∃ t' ⇒ //.
    by rewrite inE.
  have Hxa : val a < val x by rewrite val_turn_inj.
  have Hxb : val x < val b by rewrite val_turn_inj.
  exact: (no_inner_in_pos_seq Hi1 Hxin Hxa Hxb).
have Hno_right :
  ∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t'.
  move⇒ t' /andP [Ht1 Ht2].
  apply/negP ⇒ Ht'turn.
  pose x := turn_inj t'.
  have Hxin : x \in pos_seq s.
    rewrite mem_pos_seq /turn_witness !inE.
    apply/orP; right; apply/orP; right.
    apply/imsetP; ∃ t' ⇒ //.
    by rewrite inE.
  have Hxb : val b < val x by rewrite val_turn_inj.
  have Hxc : val x < val c by rewrite val_turn_inj.
  exact: (no_inner_in_pos_seq Hi Hxin Hxb Hxc).
exact: (sign_flip_at_turn Htn Heqb Hat Hbc Hno_left Hno_right).
Qed.

Witness alternation: pick_seq s (turn_witness s) is alternating. Combines triple_flip_pos_seq with the sign-seq characterization of is_alt.
Theorem is_alt_pick_turn_witness s :
  is_alt (pick_seq s (turn_witness s)).
Proof.
rewrite pick_seq_pos_seq.
apply: is_alt_from_sign.
  apply: uniq_adj_of_uniq.
  rewrite map_inj_in_uniq.
    exact: pos_seq_uniq.
  by move⇒ x y _ _ /val_inj /perm_inj.
apply: sign_seq_alt_of_triple_flip.
exact: triple_flip_pos_seq.
Qed.

Headline lower bound for as_perm_max: (turn_count s).+2 ≤ as_perm_max s. Witnessed by turn_witness s, which has (turn_count s).+2 elements and induces an alternating pick_seq (Stanley §1.6.2).
Theorem as_perm_max_lower s : (turn_count s).+2 ≤ as_perm_max s.
Proof.
rewrite -card_turn_witness.
rewrite /as_perm_max.
exact: (leq_bigmax_cond (turn_witness s) (is_alt_pick_turn_witness s)).
Qed.

End ExistenceLB.


Section UpperBoundChain.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).

Sorted enumeration of a subset is a subseq of the sorted full enumeration: sort by val (enum I) is a subseq of enum 'I_n.+2.
Lemma sort_enum_subseq_enum (I : {set 'I_n.+2}) :
  subseq (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)) (enum 'I_n.+2).
Proof.
have Hle_total : total (fun a b : 'I_n.+2 ⇒ val a ≤ val b).
  by move⇒ a b; apply: leq_total.
have Hle_trans : transitive (fun a b : 'I_n.+2 ⇒ val a ≤ val b).
  by move⇒ a b c; apply: leq_trans.
have Hsub_enumI : subseq (enum I) (enum 'I_n.+2).
  rewrite enumT /enum_mem.
  exact: filter_subseq.
have Hsorted : sorted (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum 'I_n.+2).
  exact: sorted_val_enum_ord.
have Hsort_enum : sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum 'I_n.+2) =
                  enum 'I_n.+2.
  exact: (sorted_sort Hle_trans Hsorted).
rewrite -Hsort_enum.
apply: (subseq_sort Hle_total Hle_trans).
exact: Hsub_enumI.
Qed.

pick_seq s I is a subseq of perm_seq s for any position set I.
Lemma pick_seq_subseq_perm_seq s (I : {set 'I_n.+2}) :
  subseq (pick_seq s I) (perm_seq s).
Proof.
rewrite /pick_seq /perm_seq.
exact: map_subseq (sort_enum_subseq_enum I).
Qed.

Flip-count comparison for pick_seq vs perm_seq: any pick has flip_count at most that of the full perm seq.
Lemma flip_count_pick_le_perm s (I : {set 'I_n.+2}) :
  flip_count (sign_seq (pick_seq s I)) ≤ flip_count (sign_seq (perm_seq s)).
Proof.
exact: flip_count_sign_seq_le_subseq (pick_seq_subseq_perm_seq s I).
Qed.


flip_count expressed as an indexed sum of consecutive XOR-pairs. Used to align with the turn_count sum over is_turn.
Lemma flip_count_as_sum (xs : seq bool) :
  flip_count xs =
    \sum_(0 ≤ i < (size xs).-1) (nth false xs i (+) nth false xs i.+1).
Proof.
case: xs ⇒ [|x xs] /=.
  by rewrite /flip_count /= big_nil.
rewrite /flip_count /=.
rewrite (big_nth false) size_pairmap.
apply: eq_big_nat ⇒ i Hi.
have Hi' : i < size xs by case/andP: Hi.
rewrite (nth_pairmap x) //.
case: i Hi' {Hi} ⇒ [|i] Hi' //=.
- by rewrite (@set_nth_default _ _ false x).
- rewrite (@set_nth_default _ _ false x i (ltnW Hi')).
  by rewrite (@set_nth_default _ _ false x i.+1 Hi').
Qed.

XOR is invariant under double negation: ~~ a (+) ~~ b = a (+) b.
Lemma neg_add_neg (a b : bool) : ~~ a (+) ~~ b = a (+) b.
Proof. by case: a; case: b. Qed.

Bridge identity: flip_count (sign_seq (perm_seq s)) = turn_count s. The seq-level flip count of the full word equals the perm-level turn count, via sign_seq_perm_seq and the descent-XOR characterization of is_turn.
Lemma flip_count_perm_seq_eq_turn_count s :
  flip_count (sign_seq (perm_seq s)) = turn_count s.
Proof.
rewrite sign_seq_perm_seq flip_count_as_sum.
rewrite size_map size_enum_ord /=.
under eq_big_nat ⇒ i Hi.
  have Hi1 : i < n.+1 by case/andP: Hi ⇒ _; apply: ltnW.
  have Hi2 : i.+1 < n.+1 by case/andP: Hi.
  rewrite (nth_map ord0); last by rewrite size_enum_ord.
  rewrite (nth_map ord0); last by rewrite size_enum_ord.
  rewrite neg_add_neg.
  over.
rewrite big_mkord.
have Hsum_eq : ∀ i : 'I_n,
    is_descent s (nth ord0 (enum 'I_n.+1) i)
      (+) is_descent s (nth ord0 (enum 'I_n.+1) i.+1) = is_turn s i.
  move⇒ i.
  have Heq1 : (nth ord0 (enum 'I_n.+1) i : 'I_n.+1) = widen_ord (leqnSn n) i.
    apply: val_inj ⇒ /=; rewrite nth_enum_ord //.
    by apply: ltnW; apply: ltn_ord.
  have Heq2 : (nth ord0 (enum 'I_n.+1) i.+1 : 'I_n.+1) = lift ord0 i.
    apply: val_inj ⇒ /=.
    rewrite nth_enum_ord /=. by rewrite /bump /= add1n.
    by apply: ltn_ord.
  by rewrite Heq1 Heq2.
under eq_bigr ⇒ i _ do rewrite Hsum_eq.
rewrite /turn_count -sum1_card.
rewrite [in RHS]big_mkcond.
apply: eq_bigr ⇒ i _.
rewrite inE.
by case: (is_turn s i).
Qed.

Headline upper bound for as_perm_max: as_perm_max s ≤ (turn_count s).+2. Combines the alternating flip_count formula is_alt_flip_count with the subseq monotonicity flip_count_pick_le_perm and the bridge flip_count_perm_seq_eq_turn_count.
Lemma as_perm_max_upper s : as_perm_max s ≤ (turn_count s).+2.
Proof.
rewrite /as_perm_max.
apply/bigmax_leqP ⇒ I HI.
case Hsize : (#|I| ≤ 1).
  by rewrite (leq_trans Hsize).
move/negbT: Hsize; rewrite -ltnNge ⇒ Hsize2.
have Hps_size : size (pick_seq s I) = #|I|.
  by rewrite /pick_seq size_map size_sort -cardE.
have Hsz_ge2 : 2 ≤ size (pick_seq s I) by rewrite Hps_size.
have Halt_fc := is_alt_flip_count HI Hsz_ge2.
rewrite Hps_size in Halt_fc.
have Hbound : (#|I|).-2 ≤ turn_count s.
  rewrite -Halt_fc -flip_count_perm_seq_eq_turn_count.
  exact: flip_count_pick_le_perm.
by case Hcard : #|I| Hsize2 Hbound ⇒ [|[|m]] // _ _.
Qed.

HEADLINE THEOREM (Stanley §1.6.2): the longest alternating subsequence count of s : {perm 'I_n.+2} equals (turn_count s).+2. That is, as(w) = (turn_count w).+2, proving the two definitions as_perm_max (bijective max) and as_perm (turn count) coincide. Combines as_perm_max_upper and as_perm_max_lower.
Theorem as_perm_max_eq s : as_perm_max s = (turn_count s).+2.
Proof.
apply: anti_leq.
apply/andP; split.
- exact: as_perm_max_upper.
- exact: as_perm_max_lower.
Qed.

End UpperBoundChain.