Minimal filling architectures of polynomial neural networks: a proof for the Dao–Rodriguez table, a certified census at depth eight, exact neurovariety dimensions, and a corrected defectivity criterion

The finite-field rank step, in the kernel: for an integer matrix J and any modulus N, if the k x k submatrix of J on rows ri and columns ci has nonzero determinant in ZMod N, then k <= rank of J over Q. Proof: det commutes with the ring homomorphism Z -> ZMod N, so a nonzero reduced determinant forces a nonzero integer determinant; over Q a square matrix with nonzero determinant is a unit, and a submatrix's rank never exceeds the matrix's. No primality is needed. With control_drop showing the converse fails (det [11] = 11 is nonzero over Q and zero in ZMod 11) and controlₙonvacuous showing the hypothesis is satisfiable

The compute-first gate: the source's own printed numbers, recomputed from its definitions by an independent implementation and kernel-checked. Its worked example Jac Psi_((2,1,1),2) at theta = (w11,w12,w2) = (1,0,1) equals [[2,0,1],[0,2,0],[0,0,0]] entry by entry with determinant 0 and Psi = x1²; its Lemma 2.2 certificate at its own Appendix-C weights and its own prime p = 101 gives a 65 x 65 minor equal to 75, hence rank 65 = the ambient dimension; and the 'Reported Dimension' column 35, 60, 62, 39, 61, 59 of its Table 1 is exactly the Jacobian rank at integer points for the six maximal subarchitectures of the counterexample

Reproducible filling certificates: an explicit integer parameter point with entries in 1,2,3, the prime p = 101, and a named set of ambDim parameter columns whose maximal minor of Jac Psi_(d,r)(theta) is nonzero mod 101, for all 18 architectures of the source's Table 2 (minors 74, 45, 38, 4, 5, 89, 26, 14, 19, 90, 18, 76, 48, 14, 75, 52, 65, 16 at ambient dimensions 3, 5, 9, 17, 33 and 65 thirteen times) and for the five d₀ = 2 architectures of its Proposition 2.4 ((2,4,5,4), (2,3,3), (2,3,4,4), (2,3,4,5,3), (2,3,4,5,4); minors 98, 71, 17, 2, 5). fillingCertified checks d₀ = 2, p prime by trial division, the selected submatrix square of size exactly the ambient dimension, and the determinant nonzero

The minimality half of the source's Table 2, mechanised and kernel-only: for each of its 18 architectures and each of the 102 maximal subarchitectures obtained by decreasing one hidden width by one (83 distinct), the dimension calculus ub of Core.lean – ambient bound, expected-dimension bound, the depth-2 determinantal (Alexander-Hirschowitz at r = 2) bound, the subspace bound, and the KTB recursive bound over every split – lands strictly below the ambient dimension. With Bounds.dimₗeᵤb this proves, granting those five inputs, that no maximal subarchitecture of a Table-2 entry is filling; with the filling certificates of MR3 it proves that every entry of Table 2 IS a minimal filling architecture. Kernel-clean decide, no native_decide; fuel 2 suffices and equals fuel 12 on every case

The source's Lemma 2.5 and Table 1 reproduced and sharpened: for the six maximal subarchitectures of the counterexample (2,3,4,5,4,6,4,1) the calculus gives 35, 61, 63, 39, 61, 62 against the source's proved bounds 53, 61, 63, 39, 62, 62 – two improvements – and the maximal subarchitectures are exactly the six the source's Table 1 lists. On s₁, s₄, s₅ the bound meets the dimension the source reports (35, 39, 61), so those three neurovariety dimensions are pinned exactly once the rank witnesses are in hand; the source proves exactness only for s₄

The source's r = 3 counterexample (2,3,7,6,15,8,1) is a proved minimal filling architecture: filling certified by a 244 x 244 minor equal to 56 mod 101 at an explicit integer point (ambient dimension 244 = C(2+243-1,243)), and all five maximal subarchitectures certified not filling with calculus bounds 84, 240, 225, 235, 233 against the source's reported dimensions 84, 240, 223, 233, 231

The source's d_L = 2 counterexample (2,3,4,4,10,17,11,12,4,2), depth 9, ambient dimension 514, 619 parameters: filling certified by a 514 x 514 minor equal to 54 mod 101 at an explicit integer point, and seven of its eight maximal subarchitectures certified not filling with codimensions 254, -, 176, 5, 17, 34, 11, 124 – seven exact matches against the source's reported 254, 17, 176, 5, 17, 34, 11, 124. The eighth, (2,3,3,4,10,17,11,12,4,2), is NOT reached: the calculus gets only 514 = ambient, so its minimality is not proved here

Negative controls on the dimension calculus: it certifies NO Table-2 entry as non-filling (all 18 are filling, so a calculus that did would be unsound); the constant-width (2,2,2,2,2,2,2,1) is certified not filling with ub = 13 < 65, and so is the source's own worked example (2,1,1) with ub = 2 < 3; the too-large architecture (2,4,4,5,4,6,4,1) is NOT certified minimal, correctly, since its maximal subarchitecture (2,3,4,5,4,6,4,1) is itself filling; fuel 1 fails while fuel 2 equals fuel 4, so the recursion has converged; and without the subspace bound the shared subarchitecture (2,3,4,5,5,4,3,1) is left at the ambient dimension 65, so three of the 18 entries would not be certified

Negative controls on the certificates: Euler's identity sum_(a,b) (Wᵢ)_(ab) dPsi/d(Wᵢ)_(ab) = r^(L-i) Psi holds layer by layer for every certificate, tying the dual-number Jacobian back to the network evaluation; the source's OWN integer point read modulo 11 or modulo 29 instead of 101 has Jacobian rank only 60 < 65 although the architecture is filling, so a rank-deficient finite-field computation is no evidence at all; (2,4,4,5,4,6,4,1) and its maximal subarchitecture (2,3,4,5,4,6,4,1) are both filling, so a filling certificate proves nothing about minimality; and (2,2,2,2,2,2,2,1) has rank 13 against ambient 65

Soundness of the dimension calculus: any dim: List N -> N satisfying the five inputs – dim d <= ambient; dim d <= sum dᵢ dᵢ₋₁ - sum_(i<L) dᵢ; the depth-2 determinantal bound at r = 2; the subspace bound dim V_d <= d_(L-1)(N - d_(L-1)) + d_L d_(L-1) for d_(L-1) <= N = C(d₀ + r^(L-1) - 1, r^(L-1)); and the KTB recursive bound dim V_((d₀..d_L)) <= dim V_((d₀..dₖ)) + dim V_((dₖ..d_L)) - dₖ – satisfies dim d <= ub r fuel d at every fuel. With a consistency control (dim identically 0 satisfies all five), a non-triviality control (the bound at (2,2,4,5,4,6,4,1) is 35 against ambient 65) and a sharpness control (on s₁, s₄, s₅ of the counterexample the bound is attained, so ub cannot be lowered in general)

Exact neurovariety dimensions: for each of the 83 distinct maximal subarchitectures of the source's Table-2 entries, the Jacobian rank at an explicit integer point mod 101 (a lower bound for dim V) and the calculus bound ub 2 2 (an upper bound) are computed together; they agree on 71, pinning those dimensions exactly, and never cross. Eight of the 71 values are already in the record (the six of the source's Table 1, its worked example (2,1,1) -> 2, and four rows of its repository CSV) and all eight agree; 63 are new. The remaining 12 have a gap of 1 to 3

Theorem A.10 of arXiv:2605.09609v2, as printed, is one step too wide. It reads: if r = 2 and d = (d₀,d₁,d₂) satisfies C(d₀-1+r,r) - d₀ < d₁ < mind₂, C(d₀-1+r,r), then V_(d,r) is defective. At d₀ = 2 that condition is d₁ = 2 and d₂ >= 3; but (2,2,3), (2,2,4) and (2,2,5) have Jacobian rank 8, 10, 12 at explicit integer points, equal to their expected dimensions 8, 10, 12, so none of the three is defective. The subspace bound proves defectivity exactly on C(d₀+1,2) - d₀ + 1 < d₁ < min(d₂, C(d₀+1,2)), one step narrower on the left, and all three counterexamples sit exactly on the extra step; the corrected region still contains (3,5,6), the only instance the source uses

Cost profile of the family, and one rule worth reusing. Measured 2026-09-03 under nice -n 15 ionice -c3: Core 15 s, Data 10 s, DimData 9 s, Minimal 168 s (kernel decide, fuel 2), Filling 276 s (native_decide), Dims 57 s, Bounds 13 s, Rank 9 s; the single most expensive check is the d_L = 2 counterexample's 514 x 514 minor at 133 s and 1.59 GB peak RSS. Total for the family about 0.8 CPU-hours. THE RULE: for a fuel-parameterised recursive bound, measure the smallest fuel that reaches the fixed point before committing to a decide – ub without memoisation makes 3^(L-2) calls, so at fuel 8 and depth 7 the same theorem reached 12.4 GB RSS and was killed, while at fuel 2 (identical values on all 83 subarchitectures, on the r = 3 counterexample and on the depth-9 one) it is 168 s and kernel-clean. An 80x saving that turned a memory bomb into a kernel-only proof

Reproducible filling certificates at depth 8: an explicit integer parameter point with entries in 1,2,3, the prime p = 101, and a named set of 129 parameter columns whose maximal minor of Jac Psi_(d,2)(theta) is nonzero mod 101, for all 111 depth-8 architectures (d₀ = 2, d_L = 1, r = 2) that the source's own search output flags as minimal filling. Ambient dimension 129 = C(2 + 2⁷ - 1, 2⁷) throughout; the 111 minors are printed. The Euler control sum_(a,b) (Wᵢ)_(ab) dPsi/d(Wᵢ)_(ab) = r^(L-i) Psi is kernel-checked at depth 8 on four of the certificates and holds for all 111 in the family's Python tool.

The depth-8 census: 107 of the 111 depth-8 architectures the source's search output flags as minimal filling are PROVED minimal filling architectures – filling by the certificates of MR14, minimal because each of the seven maximal subarchitectures obtained by decreasing one hidden width by one is bounded strictly below the ambient dimension 129 by the dimension calculus ub of Core.lean (777 subarchitectures, 605 distinct; kernel-only decide, no native_decide, in eleven chunks). Depth 7 had 18 entries and 93 subarchitectures. The remaining 4 are not decided: each is blocked by one of only two distinct subarchitectures (MR18). So the number of depth-8 MFAs for d₀ = 2, d_L = 1, r = 2 is at least 107 – against the count 82 printed in the source's Discussion, which matches nothing in the repository that sentence cites (the flagged count is 111 in every version of the file the repository has ever held, and no width box, parameter-count threshold, unimodality or defect filter of that data gives 82; the '20 nonunimodal' half of the same sentence matches exactly).

Seventeen new counterexamples to Conjecture 12 of Kileel-Trager-Bruna: of the 107 proved depth-8 minimal filling architectures, exactly 17 have non-unimodal width sequences – (2,3,3,4,7,6,7,6,1), (2,3,3,5,7,5,8,5,1), (2,3,3,5,7,6,7,4,1), (2,3,3,6,6,5,8,8,1), (2,3,3,6,7,6,7,3,1), (2,3,4,4,7,5,8,8,1), (2,3,4,4,7,6,7,5,1), (2,3,4,5,4,7,8,5,1), (2,3,4,5,4,8,8,4,1), (2,3,4,5,6,5,8,5,1), (2,3,4,5,7,5,7,5,1), (2,3,4,5,7,5,8,4,1), (2,3,4,5,7,6,7,3,1), (2,3,4,5,8,5,7,4,1), (2,3,4,6,5,8,6,3,1), (2,3,4,6,6,5,7,7,1), (2,3,4,6,7,5,7,4,1). Unimodality is decided by the same greedy walk the source's Conjecture 1.7 and its repository's isᵤnimodal.py use.

Exact neurovariety dimensions at depth 8: for each of the 605 distinct maximal subarchitectures of the 111 flagged depth-8 architectures, the Jacobian rank at an explicit integer point mod 101 (a lower bound for dim V) and the calculus bound ub 2 2 (an upper bound) are computed together; they agree on 533, pinning those dimensions exactly, and never cross (0 violations). The 72 remaining gaps are 1 (24 of them), 2 (8), 3 (20), 4 (11), 5 (4), 6 (3), 7 (1), 8 (1).

The depth-8 gap, named, and the depth-8 negative controls. The four flagged architectures the census does not reach are blocked by exactly two distinct maximal subarchitectures: (2,3,3,4,7,6,8,3,1) (blocking three) and (2,3,3,5,9,7,4,2,1) (blocking one). Both are left at the ambient dimension 129 by the calculus at every fuel 1..6, while the certified Jacobian rank at explicit integer points is 127 resp. 128 – strong evidence they are not filling, and not a proof, since a deficient finite-field rank proves nothing (the source's Corollary A.6; this family's wrong-prime control). Controls: the constant-width (2,2,2,2,2,2,2,2,1) certified not filling at ub = 15 < 129 and the width-one tower at ub = 2; (2,4,3,4,4,7,8,7,1) correctly NOT certified minimal, since the certified MFA (2,3,3,4,4,7,8,7,1) is one of its maximal subarchitectures; all three rungs of the fuel ladder used and none redundant (54 of the 605 subarchitectures decided at fuel 0, 402 at fuel 1, 147 at fuel 2); and dim = 0 satisfies the five inputs, so the census theorem is vacuous without the filling certificates.

The subspace bound (D4) at depth 8, and a repair to its statement. (i) NECESSITY: deleting (D4) – the elementary Grassmann-secant bound this family adds to the four inputs it takes from the source – costs 30 of the 107 certified entries, blocked by 17 distinct maximal subarchitectures; at depth 7 the same experiment cost 5 of 18, blocked by 2. (ii) REPAIR: Core.subspaceBound states (D4) as dim V_d <= m(N - m) + d_L m at m = d_(L-1), guarded only by m <= N, but the Grassmann-secant argument bounds the GENERIC span dimension m* only by m* <= d_(L-1), so what it justifies is max over 1 <= t <= d_(L-1) of t(N + d_L - t); since that expression peaks at t = (N + d_L)/2, the landed form is the maximum only when 2 d_(L-1) <= N + d_L. That side condition fails for 18 of the 7933 architectures the depth-8 calculus visits (e.g. (2,5,8,8,4): N = 9, d_L = 4, f(8) = 40 < 42 = f(6)), so the distinction is not vacuous. Under the strict form, re-run in full, NOTHING CHANGES: all 107 depth-8 entries and all 18 depth-7 Table-2 entries keep their certificates, and the strict calculus returns the same value on every one of the 605 depth-8 and 93 depth-7 subarchitectures. Soundness of the strict calculus is proved (Depth8Bounds.dimₗeᵤbSafe), and both censuses are restated over the weaker hypothesis.

The interior subspace bound (D6), derived and measured not to help. Fix 1 <= k <= L-1 and let Nₖ = C(d₀ + rᵏ - 1, rᵏ). Replacing the layer-k activation tuple v by another basis A v of the same span is absorbed by Wₖ₊₁ -> Wₖ₊₁ A⁻¹, so the image of the top of the network depends only on span(v) in Gr(m, Nₖ) with m <= dₖ; substituting fixed forms into the top network's output is a linear map on coefficients, so the fibre over a fixed span has dimension at most dim V_((m,dₖ₊₁,...,d_L)). Hence dim V_d <= max over 1 <= m <= min(dₖ, Nₖ) of m(Nₖ - m) + dim V_((m,dₖ₊₁,...,d_L)). At k = L-1 the top is one linear layer and (D6) IS the strict form of (D4), so it is a genuine generalisation. It is also useless in this regime: adding (D6) at every interior layer changes no value on any of the 605 distinct depth-8 subarchitectures, and in particular leaves both depth-8 blocking subarchitectures at 129 and the open depth-9 subarchitecture (2,3,3,4,10,17,11,12,4,2) of the source's d_L = 2 counterexample at 514. The reason is visible: Nₖ = 2ᵏ + 1 grows with k, so for middle layers the Grassmann term alone exceeds the ambient dimension, while for k = 1, 2 the maximum over m is attained where the top network's own bound is its parameter count.

Cost profile of the depth-8 census, and two rules worth reusing. Measured 2026-09-03 under nice -n 15 ionice -c3. (i) KERNEL DECIDE MEMORY IS IN THE CHUNK, NOT THE FILE: one decide over all 107 architectures peaked at 11.3 GB and 435 s; the identical content split into eleven decide theorems of ten peaked at 4.0 GB and 149 s in the same file – memory is released between theorems, so chunk a large kernel sweep by theorem, not by file. (ii) NATIVE_DECIDE ON THIS FAMILY IS DYLIB TERRITORY AT DEPTH 8: interpreted, the 111 depth-8 filling certificates did not finish in the time the 18 depth-7 ones take twenty times over (killed at 4 CPU-min with no output); the whole hot path is the Mathlib-free Core.lean, so families/mfa-rank-cert/tools/mfa_core_dylib.sh compiles it to a shared library and the checks run compiled. Consequence for the repository: the depth-8 native_decide modules must never be rebuilt by lake build – rebuild them with –load-dynlib or not at all.