structure CoxeterReflectionId.InversionDifferenceBridgeHyp {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Prop

Hypothesis bridge for identifying reflections from inversion-set differences: if $vt = w$ with $\ell(v) + 1 = \ell(w)$ and a generator $i$ flips its descent status, then $t$ equals the simple reflection $s_i$.

• identify_from_inversions (v w t : W) : t ∈ CoxeterBruhat.reflections M cs → v * t = w → cs.length v + 1 = cs.length w → ∀ (i : B), ¬cs.IsRightDescent v i → cs.IsRightDescent w i → t = cs.simple i

theorem CoxeterReflectionId.reflection_identification_genuine {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (bridge : InversionDifferenceBridgeHyp cs) : CoxeterBruhat.ReflectionIdentificationHyp cs

Bridge: an inversion-difference identification hypothesis upgrades to the genuine reflection identification hypothesis used by the strong exchange machinery.

def CoxeterReflectionId.bridge_from_reflection_id {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (hid : CoxeterBruhat.ReflectionIdentificationHyp cs) : InversionDifferenceBridgeHyp cs

Converse bridge: an existing reflection-identification hypothesis yields the inversion-difference bridge hypothesis.

theorem CoxeterReflectionId.strong_exchange_from_bridge {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (bridge : InversionDifferenceBridgeHyp cs) : CoxeterBruhat.StrongExchangeForBruhat cs

The Strong Exchange Property holds whenever the inversion-difference bridge holds.