Function exactness_gate 

pub fn exactness_gate(budget: &OutputBudget) -> Result<(), AnaLowerError>

The integer lane’s ½-grid exactness proof: integer inputs on a grid-preserving region read back EXACTLY through the rounding ADC iff the compiler’s own error budget stays under half a grid step. Ok(()) is the exactness CERTIFICATE’S admission condition; the refusal carries the budget that broke so the diagnostic names the cost.