$mem_span_hom$. A polynomial computed by a reduced matrix-symmetric circuit of support size $≤ k$ and support depth $≤ Δ$ is a linear combination of homomorphism polynomials of patterns of $Δ$-forestwidth at most $k - 1$.

Applies $PatternsInductionMain.exists_phi$ ($lem:induction$) at $g := C.out$. Since $minSupport C C.out = ∅$ ($PatternsSupportBasic.minSupport_out$), $supOf hrig hn C.out = ∅$ too ($supOf_eq_minSupport$), so $leftCard hrig hn C.out = rightCard hrig hn C.out = 0$; the witness $φ$, lifted from depth $sc C C.out$ to $Δ$ ($sc_le_supportDepth$, $hdepth$, $span𝔗P_mono$), is evaluated at the (unique, since the arities are $0$) canonical enumerations, giving $p$ ($computesAt_unique$, since $C.Computes p$ unfolds to $C.ComputesAt C.out p$). Every generator $labelledHom K G n$ of $span𝔗P K Δ k n (Finset.univ : Finset (Fin 0 ⊕ Fin 0))$, evaluated at any point, is exactly the unlabelled homomorphism polynomial $hom K G.F n$ ($labelledHom_eq_hom_of_zero$, since the defining $if$-condition of $labelledHom$ is vacuously true at arity $(0,0)$), and $G ∈ 𝒯^{Δ,k}(0,0)$ is exactly $ForestwidthLE Δ (k - 1) G.F$ ($PatternsLabelledUnlabelled.inClass_ofPattern_iff$, using $G = ofPattern G.F$ since both label maps out of $Fin 0$ are forced to be $Fin.elim0$); $eval_mem_span_hom$ packages this as a $Submodule.span_induction$ argument, stated for an arbitrary arity $(ℓ, r)$ with $ℓ = r = 0$ as hypotheses (rather than literal $Fin 0$s) so that it can be $subst$ed in directly against $leftCard hrig hn C.out$/$rightCard hrig hn C.out$, with no further reindexing needed.