Remark: Switching is a choice of model

The prescription (eq:switchedaction) is part of the theorem, not a consequence of the first-order repair. A different assignment of switch factors to higher vertices must be declared separately. The proof below applies to the action actually written here.