theorem CoxeterRootSignChange.isReduced_drop {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {word : List B} (hred : cs.IsReduced word) (j : ℕ) : cs.IsReduced (List.drop j word)

Dropping the first $j$ letters of a reduced word yields another reduced word.

noncomputable def CoxeterRootSignChange.rootSignChangeHyp {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (bridge : CoxeterExchangeGenuine.GeometricBridgeHyp M cs) : CoxeterExchangeGenuine.RootSignChangeHyp M cs

Geometric root sign change hypothesis derived from the geometric bridge, packaging the fact that the simple reflection $\sigma_s$ flips a positive root at the descent index.