Validity via max is great for safety; I’m worried about burn under adversarial packing.
One that I am thinking would work is to prove that with gas_metered = max(r_i) the expected burn is monotone in normalized total usage even if builders keep max just below target.