nx_h264_cabac_residual_gate.nx

nx_h264_cabac_residual_gate.nx -- teeth for STEP 2 residual decoding. WHAT THESE TEETH DO AND DO NOT PROVE. There is no CABAC ENCODER and no reference decoder in this ecosystem, so I cannot assert "these bins decode to these coefficients" -- that would need a vector I have no way to produce. What IS provable without one: bounds refusal, array initialisation, loop TERMINATION on adversarial input, and sign/zero handling. Those are real defects if broken, and every one below is a matched pair (the property fires AND its control). END-TO-END SPEC CONFORMANCE IS NOT CLAIMED HERE -- it needs a real CABAC stream decoded to an image. Do not read GREEN here as "CABAC posters work".