theorem Q2Presentation.Lifting.omega2Mod_val_mod_four {Yt : BoundaryFramedTarget} [Finite Yt.Y] (h4 : 4 ∣ Nat.card Yt.Y) : (omega2Mod (Nat.card Yt.Y)).val % 4 = 1

theorem Q2Presentation.Lifting.odd_of_mod_four {Yt : BoundaryFramedTarget} [Finite Yt.Y] (h4 : (omega2Mod (Nat.card Yt.Y)).val % 4 = 1) : Odd (omega2Mod (Nat.card Yt.Y)).val

The mod-4 residue condition implies the oddness threaded through the Stokes layer.