Lemma: Concrete diamond

Distinct enabled liberal redexes occupy nonnested positions and own disjoint runtime-name sets. Firing either and then the residual of the other gives equal joint weights and equivalent resulting configurations.

Proof. An enabled root redex has no enabled accessible redex inside it: its required arguments are values, and bodies and alternatives are inaccessible. Distinct redexes are therefore nonnested. Their positions are separated by context-splitting rules. Shared additive contexts occur only in inaccessible alternatives.

Disjoint administrative transitions commute. Allocations commute up to fresh-name renaming and commute with operations on existing factors. Disjoint gates commute. A gate commutes with destructive readout on disjoint factors, with the canonical identification of the surviving output space.

For disjoint readouts,

Both orders have joint weight

and, on a positive joint branch, the same normalized residual. Zero joint weights contribute zero in both orders.