Convergence to a fully compressed t-intersecting family

Fix a finite ground set $[n]$, a distinguished element $z \in [n]$, and a $t$-intersecting family $\mathcal{A}$ (TIntersecting) of subsets of $[n]$: every two members, allowing repeats, meet in at least $t$ elements. Repeatedly applying the shifting operation $S_{z,i}$ (which moves $i$ to $z$ whenever this is possible without colliding with an existing set) for various $i \ne z$ can only ever be done finitely many times before no further shift changes anything, because each genuine shift strictly reduces the total weight $\sum_{A} \sum_{a \in A} 2^{a}$ of the family. This result packages that termination argument together with the fact that shifting preserves both cardinality and the $t$-intersecting property:

Here "stable under $S_{z,i}$" (IsCompressed) means applying the shift to $\mathcal{B}$ leaves it unchanged. Taking $z$ to be the least element of $[n]$, stability for every $i > z$ is exactly stability under every shift towards $z$, i.e. $\mathcal{B}$ is fully compressed towards $z$. This reduction — replace an arbitrary $t$-intersecting family by an equally large, fully compressed one — is the first step of Katona's 1964 proof bounding the maximum size of a $t$-intersecting family: once compressed, a family avoiding $z$ can be shown to be $(t+1)$-intersecting on the remaining $n-1$ elements, which drives an induction on $n$.

Formalization note. The measure used for termination is the standard one from Mathlib's own Kruskal–Katona development (familyMeasure there), specialized here to compressions along singleton sets $\{z\}, \{i\}$; termination is via well-founded recursion on this measure.