For H=max(2,|a|,b), each cleared integer matrix entry has absolute value <=A=(3q)^n*(2H)^(6q). Prove inequalities symbolically; never materialize this huge matrix for the universal proof.
Method: native-order. Induction: none. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.