Downcrossings and Pathwise Reversal Lemmas — Re-export Shim

This file is the umbrella for the crossing-based reverse-martingale infrastructure. Following the split for maintainability, the contents now live in three sub-files:

• Crossings/Pathwise.lean — downcrossingsBefore, downcrossings, congruence lemmas, upBefore_le_downBefore_rev_succ
• Crossings/Bounds.lean — upcrossings_bdd_uniform (uniform-in-N bound on upcrossings of the reverse martingale)
• Crossings/AntitoneLimit.lean — condExp_exists_ae_limit_antitone, ae_limit_is_condexp_iInf

Existing call sites continue to work via this umbrella import.