Function is_sequence_disabled 

pub fn is_sequence_disabled(sequence: u32) -> bool

BIP68: Check if sequence number has disabled bit set

Bit 31 (0x80000000) disables relative locktime when set.

BIP68 invariant: when the disable bit is set, bit 31 is set, so sequence > i32::MAX (any u32 value ≥ 2^31 satisfies this). Z3 verifies: result == true ⟹ sequence > 2147483647.