Green restriction has one distinguished summand

The inducing assertion in F3 supplies an indecomposable $H$-module $U$ with vertex $Q$ and $M\mid {\mathrm{Ind}}_H^{G}U$. Relative projectivity passes up $Q\le P\le H$ by transitivity of induction, so $U$ is relatively $P$-projective. F4 gives ${\mathrm{Res}}_H^G{\mathrm{Ind}}_H^{G}U\cong U\oplus E_0$, where $E_0$ is $\mathcal{Y}$-projective. These inherited existence arguments use the assumed AC.

The separate restriction assertion in F3 supplies $W\mid {\mathrm{Res}}_H^{G}M$ with vertex $Q$. By F2 and F4 neither $W$ nor $U$ is $\mathcal{Y}$-projective. Thus no indecomposable in $E_0$ is isomorphic to either one.

Restricting the split inclusion from 1.1 makes ${\mathrm{Res}}_H^{G}M$ a direct summand of $U\oplus E_0$. By F5, its indecomposable multiset is a submultiset of that of $U\oplus E_0$. The copy of $W$ from 1.2 cannot lie in $E_0$, so $W\cong U$. Exactly one copy is available. The remaining multiset is contained in that of $E_0$, giving a complementary $E\mid E_0$. Family-projectivity is summand-closed as proved in F4, so $E$ is $\mathcal{Y}$-projective.

The inducing witness was obtained in 1.1, before any inverse correspondence. Every summand of $E$ has vertices excluded from $\mathcal{Z}$ by F2 and F4. If $H=G$, restriction is the identity and the empty error family forces $E=0$. If $P=1$, the normalizer hypothesis forces $H=G$. The zero module is excluded as an input but permitted as the complement. Since $P\in \mathcal{Z}$, the case $Q=P$ is included. This proves all claims. [F1, F2, F4, step 1.1, step 2.1] QED