But is it technically possible for the user in question to prove if the sequencer incorrectly asserted a provable transaction as un-provable?
No, it’s not possible to (easily) prove that the sequencer was malicious. The reason is that it requires knowing the exact state of the system at the time the sequencer tried to apply the transaction (an exception may be if we somehow move the red txs to the end of the block), but this requires the user to know all the transactions in the block which is not ideal.
The idea of this model is that the red fee (the fee that the sequencer is allowed to take, without proving anything, and without executing the transaction) will be much lower than the green fee, so a reasonable sequencer will prefer to include the transaction and take the green fee when possible.
The downside is that the sequencer may behave irrationally, in which case, it will lose money, but the user will get an annoying UX - their tx was revoked and they lost some money. Now they’ll have to resend it hoping the next sequencer will be nicer.
One optional addition is to allow the user to specify a list of sequencers that are not allowed to handle their tx. So if a user feels a specific sequencer is malicious, they can exclude it. We’re not sure how to maintain this list, and it seem to complicate the solution.