Function mldsa_montgomery_congruence 

pub fn mldsa_montgomery_congruence() -> bool

Certify the ML-DSA Montgomery CONGRUENCE: (a − lo·q) − a = −q·lo, so the reduction numerator redc·R = a − lo·q differs from a by a multiple of q ⇒ redc·R ≡ a (mod q) ⇒ redc ≡ a·R⁻¹ (mod q). A ring identity in the free variables a, lo, certified for all values.