The characterisation of bounded-depth matrix-symmetric circuits.

The forward direction (1 → 2) is the concept $PatternsFromCircuits.mem_span_hom$ directly.

For the backward direction (2 → 1), $Submodule.mem_span_set'$ writes $p = ∑ i, f i • hom K (F i) n$ for finitely many patterns $F i$ with $ForestwidthLE Δ (k - 1) (F i)$. For each $i$, a circuit $D i$ computing $hom K (F i) n$ is obtained from the concept $CircuitsForPatterns.exists_circuit$; it is reduced, matrix-symmetric, with support size $≤ k$ and support depth $≤ Δ$. These are glued ($BoundedDepthGlueCircuit.glueCircuit$) by scaling each block's output by $f i$ (via a new $mul$-gate and a new $const (f i)$ input gate) and summing all of these via a new output $add$-gate; the glue circuit computes $∑ i, f i • hom K (F i) n = p$ ($BoundedDepthGlueComputes.glueCircuit_computes$) and is matrix-symmetric ($BoundedDepthGlueSymmetric.glueCircuit_isMatrixSymmetric$), since every block is. Rigidifying it ($RigidConstruction.reduced$) yields a reduced, matrix-symmetric circuit computing $p$ ($RigidReduced.isReduced_reduced$, $RigidSymmetric.isMatrixSymmetric_reduced$, $RigidComputes.computes_transfer$) with support size $≤ k$ ($BoundedDepthGlueSize.glueCircuit_reduced_supportSize_le$) and support depth $≤ Δ$ ($BoundedDepthGlueSc.glueCircuit_reduced_supportDepth_le$), the latter via a potential built from each block's own $sc$, since every glue gate has empty minimal support and every block's own minimal support is unaffected by rigidifying the glue circuit as a whole ($BoundedDepthEmbed.embed_equiv_eq$, $BoundedDepthReducedFormula.reduced_σOf_eq$).

The concept $Rigidification.exists_reduced$ is deliberately not used: it does not preserve support size or support depth, so the proof rigidifies with $RigidConstruction.reduced$ and tracks the supports of the block gates through it directly.