Theorem: Subsystem Möbius support

For a perfect-record tower and fixed subsystem $S$, the family

is down-closed under nonempty subsets. In particular,

Proof. For each class meeting $S$, choose an accessible member and let $Q_j$ be pinching that member on ${\mathcal{H}}_S$. If $K_j\cap S=\varnothing$, put $Q_j=\mathrm{id}$. The $Q_j$ commute.

Inspect a branch cross term. If a class has an inaccessible differing member, that term is already zero after partial trace. Every surviving term therefore has the same survival rule under global class pinching and under its selected accessible anchor. A class wholly outside $S$ cannot distinguish surviving reduced terms. Thus, for all $K\subseteq \mathcal{N}$,

Consequently,

For $L\subseteq J$,

If the rightmost argument were zero, the result would be zero. Hence a nonzero $J$-element forces every nonempty subset element to be nonzero. A nonempty support therefore contains a singleton.