Renormalization maps form a formal composition group

Use the two explicitly supplied systems [F1]; no existence theorem for constructing them is invoked. Introduce a formal degree parameter $\lambda$ and write $\mathcal{S}(\lambda V)=1+{\sum }_{n\ge 1}{\lambda }^n{S}_n(V)$ and ${\mathcal{S}}^{\mathrm{\prime }}(\lambda V)=1+{\sum }_{n\ge 1}{\lambda }^n{S}_n^{\mathrm{\prime }}(V)$. Since $T_1=T_1^{\mathrm{\prime }}=\mathrm{id}$, the degree-one coefficients agree. Set $Z_1(V)=V$.

Suppose homogeneous maps $Z_j$ are defined for $1\le j<n$, with finite-jet kernels supported on the total diagonal and preserving supports and covariance, and $\mathcal{S}(Z_{<n}(\lambda V))$ agrees with ${\mathcal{S}}^{\mathrm{\prime }}(\lambda V)$ through degree $n-1$. In the degree-$n$ coefficient of $\mathcal{S}(Z_{<n}(\lambda V)+{\lambda }^n{Z}_n(V))$, the only occurrence of $Z_n$ is the linear term $T_1(Z_n)=Z_n$: every term with $T_k$ for $k\ge 2$ has $k$ positive degrees summing to $n$, so each degree is at most $n-1$. Therefore there is exactly one choice of $Z_n$, namely the degree-$n$ residual of ${\mathcal{S}}^{\mathrm{\prime }}$ minus the already known coefficient of $\mathcal{S}\circ Z_{<n}$.

Polarize the homogeneous residual from step 2.1 into its symmetric $n$-linear vertex kernel. Fix a point of a causal cover set $C_I$ and choose small coordinate neighborhoods of its $n$ entries whose product lies in $C_I$. For arbitrary $f_i\in C_c^{\mathrm{\infty }}$ in those neighborhoods, fix arbitrary polynomial jet labels $P_i$ of finite order and take the local functionals $F_i(\varphi )=\int f_i(x)P_i(j^{s_i}\varphi (x))d^{4}x$; their supports satisfy the same causal split. Introduce independent formal variables $t_1,\dots ,t_n$. Each lower map $Z_j$, $j<n$, has a kernel supported on the total diagonal by the induction hypothesis in step 2.1; because the two block supports are disjoint, every mixed term of $Z_j({\sum }_i{t}_i{F}_i)$ containing variables from both blocks vanishes, so $Z_j$ splits as the sum of its block restrictions. The causal-factorization identity for ${\mathcal{S}}^{\mathrm{\prime }}$ and for $\mathcal{S}\circ Z_{<n}$ then expresses the coefficient of $t_1\cdots t_n$ as a star product of block coefficients of degrees $\mathrm{\mid }I\mathrm{\mid }$ and $\mathrm{\mid }{I}^c\mathrm{\mid }$. Both degrees are strictly below $n$, so these coefficients agree by the induction hypothesis and the coefficient vanishes. For each of the arbitrary fixed polynomial jet labels, the corresponding numerical residual distribution therefore pairs to zero with every product test $f_1\otimes \cdots \otimes f_n$ in this neighborhood. Iterating [F4] over the $n$ factors shows finite sums of these product tests are dense in its test-function space, so the residual distribution vanishes on the neighborhood. Since the causal cover sets cover the complement of the total diagonal, the residual kernel is supported on that diagonal.

Fix balanced input and remaining-field labels and one $\mathrm{\hslash }$ coefficient of the polarized residual in step 3.1, and call its numerical distribution $Q$. Its field-independent numerical coefficients are translation invariant by covariance in [F1]; lower-order counterterm insertions preserve that invariance by the induction hypothesis. In coordinates $y=x_n$, $z_i=x_i-x_n$, simultaneous translation acts only on $y\in {\mathbb{R}}^4$, and step 3.1 gives $\mathrm{supp}Q\subseteq \{z=0\}$. Translation invariance implies $Q({\mathrm{\partial }}_{y_a}\mathrm{\Psi })=0$ for every test $\mathrm{\Psi }$, by differentiating its translated test curve in the fixed-support smooth topology. Choose $\eta (y)={\prod }_{a=1}^4{\eta }_a(y_a)$ with ${\eta }_a\in C_c^{\mathrm{\infty }}(\mathbb{R})$ and $\int {\eta }_a=1$, using [F5], and define $q(\psi )=Q(\eta (y)\psi (z))$. For any $\mathrm{\Psi }$, replace its dependence on $y_1$, then $y_2,y_3,y_4$, by ${\eta }_a(y_a)$ times its integral in that coordinate. Each replacement difference has zero integral in that coordinate, so its primitive from $-\mathrm{\infty }$ is compactly supported and smooth, also in the remaining variables. Hence $\mathrm{\Psi }-\eta (y)\int \mathrm{\Psi }(v,z)d^{4}v$ is a sum of four $y$-derivatives of compact smooth tests. The derivative-annihilation identity yields $Q(\mathrm{\Psi })=q(\int \mathrm{\Psi }(y,z)d^{4}y)$, that is, $Q=1_y\otimes q$. The map defining $q$ is continuous on every fixed-support test space, and its support is contained in $\{0\}\subset {\mathbb{R}}^{4(n-1)}$.

Now apply [F3] to $q$, not to $Q$: $q={\sum }_{\mathrm{\mid }\beta \mathrm{\mid }\le m}{c}_{\beta }{\mathrm{\partial }}_z^{\beta }{\delta }_0$ with finite $m$. Its finite relative scaling bound comes from the finite graph bounds of the two supplied systems and the finitely many lower-order local insertions at this fixed input, interaction and $\mathrm{\hslash }$ degree. If that bound is $B$ and $d=4(n-1)$, [F3] gives $\mathrm{\mid }\beta \mathrm{\mid }\le \lfloor B-d\rfloor$ for nonzero coefficients. In the original vertex coordinates the precise diagonal-jet formula is $Q(\mathrm{\Psi })={\sum }_{\beta }{c}_{\beta }(-1{)}^{\mathrm{\mid }\beta \mathrm{\mid }}{\int }_{\mathbb{M}}({\mathrm{\partial }}_z^{\beta }\mathrm{\Psi })(y,0)d^{4}y$, with $\mathrm{\Psi }$ here written in the $(y,z)$ coordinates. Pairing it with the finite local polynomial vertex kernels differentiates their compact smooth coefficients and remaining field jets only finitely many times, giving an integral of a finite polynomial in the field jets at $y$. Thus each coefficient of $Z_n$ belongs to $L$. Balanced representatives and derivative identities in [F1] make it independent of the density presentation. The diagonal formula confines its functional support to the intersection of the vertex supports, and covariance follows from covariance of the residual recursion. Therefore $Z_n$ has the required formal local, support-preserving and covariant coefficients.

Induction defines every $Z_n$ uniquely by the displayed residual formula; ordinary recursion and Replacement collect these unique coefficients without an axiom of choice, and each coefficient of a composition uses only finitely many partitions of its total degree. If $Z(V)=V+{\sum }_{n\ge 2}{Z}_n(V)$, solve $Z(X(V))=V$ recursively: the unknown degree-$n$ term of $X$ again occurs through the identity linear coefficient, while all other terms use lower degrees. This gives a unique formal inverse with local support-preserving coefficients. Formal composition is associative coefficientwise and preserves the identity linear term, so these maps form a group.