Function mldsa_montgomery_reduction_certified 

pub fn mldsa_montgomery_reduction_certified() -> bool

The full ML-DSA Montgomery reduction is kernel-certified: the numerator is an exact multiple of R (divisibility) and the result is a·R⁻¹ mod q (congruence). Together these prove mldsa::montgomery_reduce — hence the AVX2 montmul32 that shares its formula — computes the right field element, with no Z3, for ALL inputs (not a sampled bit-width).