Function mldsa_montgomery_divisibility 

pub fn mldsa_montgomery_divisibility() -> bool

Certify the ML-DSA Montgomery DIVISIBILITY: a·qinv·q − a = cofactor·R·a, i.e. the reduction’s numerator a − (a·qinv)·q = −cofactor·R·a is an EXACT multiple of R (so /R is a shift, never a rounding divide). This holds because qinv·q ≡ 1 (mod R); the ring canonicalizer reduces both sides to a·(qinv·q − 1), certifying it for ALL a.