Remark: The precise cancellation proved

The theorem proves an exact cancellation of the explicit second-scalar-test-derivative terms in $B_4+B_7$. It does not prove cancellation of those two branches, much less of all six.

It also does not establish that either branch is of lower microlocal order in a common characteristic calculus. That conclusion would require the calculus and order comparison still missing at E1.