Function montgomery_reduction_certified 

pub fn montgomery_reduction_certified() -> bool

The full Montgomery reduction is kernel-certified: the constant divides exactly (so /R is a shift), the result is x·R⁻¹ mod q (congruence), and the final conditional subtract keeps it in [0, q) (range). A single gate over the three procedures.