Proof. Induct along the relevant order. Input copies, gates, and dummies uniquely determine the next content bit from data already determined. These are exactly the bits of \(U_y\) or \(V_y\). The only possible obstruction is an additional terminal comparison. Shortening a valid prefix removes requirements without changing retained bits, so the valid lengths form an initial interval. At length \(h\), all terminal comparisons have been imposed, giving the two equivalences. ◻

Proof. At stage \(h\), the first description gives \[A=Q_x,\qquad B=Q_y,\qquad y=S(x),\qquad P(y)=x.\] The reconstruction template from \(y\) computes \(P(y)=x\) and then \(S(x)=y\), so it agrees with \(A\) at every position and satisfies all its comparisons. This gives the second description. Conversely, the second description at \(h\) gives \(B=Q_y\) and a full reconstruction \(A=V_y\) with \(S(P(y))=y\). Put \(x=P(y)\). Then \(P(S(x))=P(y)=x\), so \(A=Q_x\) and \(\operatorname{out}_S(A)=y\). Since \(B=Q_y\), it is the full forward prefix required in the first description. These identities include all copy gates and dummies. At \(2h\), both descriptions have \(A\) empty and \(B\) a valid full transcript. At \(3h\), both have \(A=B\) a valid full transcript. At \(4h=0\), both have \(A\) full and \(B\) empty. ◻

Proof. In the first range, erasing the newly filled position recovers its previous blank content and occupation. Conversely, a valid longer forward prefix has the uniquely prescribed value at its last position, so filling its shortened prefix recovers it. In the second range, erasure shortens a reconstruction prefix. Its erased value is uniquely determined by earlier retained positions and the unchanged full tape \(B\), so reverse reconstruction recovers it. The converse follows from the same uniqueness. In the last two ranges, the unchanged full tape determines the copied value, and erasure recovers the blank position. Boundary agreement applies to each use of these statements at a boundary. In particular, at \(c=4h-1\), the reverse proposal from stage zero copies \(A_{\pi_{\mathrm f}(0)}\) into the first forward position of the empty \(B\) tape, exactly reversing the wraparound erasure.

Shortening a valid computed prefix is always valid, as are extending or shortening a copied prefix. When extending a computed prefix, all earlier conditions remain true. Its next value is obtained from at most two earlier operands or a specified full-tape input bit, so the only new condition that can fail is the stated terminal comparison. That comparison needs one additional specified bit. Thus the relevant operands, old bits, and comparison bits suffice to decide both proposals and the corresponding existence flags. Equation (7) gives at most one predecessor, and the definition gives at most one successor. Every edge changes the stage by one modulo \(4h\), and \(4h\ge4\), so no edge is a self-edge. ◻

Proof. We first identify all endpoints. A missing successor can occur only in the first range of the schedule. Write its full tape as \(A=Q_x\) and put \(y=\operatorname{out}_S(A)=S(x)\). The current \(B\) tape is its longest valid forward prefix, so Lemma 5 gives \[ P(S(y))\ne y,\qquad P(y)=x. \tag{8}\] If \(y=0^{n_0}\), then \(x=P(0^{n_0})=0^{n_0}\) and \(y=S(0^{n_0})\ne0^{n_0}\), a contradiction. Thus this designated vector is a nonzero End-of-Line answer. Such a vertex has a predecessor: shorten its forward prefix when its length is positive; at stage zero use the reverse wraparound copy from the preceding frame.

A missing predecessor can occur only at a stage \(s=c+1\) with \(h\le c<2h\). Its full tape is \(B=Q_y\), where \(y=\operatorname{in}_S(B)\), and its reconstruction prefix has its maximal length \(k_{\mathrm r}(y)<h\). Hence \[ s=2h-k_{\mathrm r}(y),\qquad S(P(y))\ne y. \tag{9}\] For \(y\ne0^{n_0}\) this is again a permitted answer. The vertex has a successor obtained by shortening the reconstruction prefix; if the prefix is empty, the next copying step supplies a successor. Every proposal in the two copying ranges succeeds in the relevant direction, except that an incoming reconstruction proposal at stage \(2h\) is covered by the case just considered. Together with Lemma 7, this exhausts the possible missing neighbors and proves that no vertex is isolated.

It remains to specify the zero-labelled exception. The last promise in (2) supplies the unique full transcript \(Q_{0^{n_0}}\), whereas the first two promises give \[S(P(0^{n_0}))=S(0^{n_0})\ne0^{n_0}.\] Let \(k_*=k_{\mathrm r}(0^{n_0})<h\). Then \(v_*\) is exactly the vertex at stage \(2h-k_*\) whose \(B\) tape is \(Q_{0^{n_0}}\) and whose \(A\) tape is \(\operatorname{pref}_{\pi_{\mathrm r},k_*}(V_{0^{n_0}})\), with their prescribed occupations. Prefix uniqueness proves that this is the only missing-predecessor vertex with designated vector zero. It has no predecessor and has the successor just described. Evaluate \(U_{0^{n_0}}\) and \(V_{0^{n_0}}\), locate the first failed reconstruction terminal comparison, and take the preceding prefix. This computes \(v_*\) and its successor in polynomial time. This proves the endpoint claims, including the existence of the public source. Other directed paths and directed cycles may remain in the graph; nothing here requires one connected component.

We next make the local edit interface explicit. At start frame \(c\), let \(j(c)\) be the position in the transition table. Allot this position to the content and occupation arrays of the active tape, and allot the fixed default position \(0\) to the two inactive arrays. Denote these four addresses by \(j_D(c)\), for \(D\in\{A,E^A,B,E^B\}\). If \(\mathbf e_{D,j}\) is the unit vector at position \(j\) of array \(D\), define, over a field \(K\), \[ h_\sigma(c)=\sum_{D\in\{A,E^A,B,E^B\}} \sigma_D\mathbf e_{D,j_D(c)}\in K^{4h}, \qquad \sigma\in\{-1,0,1\}^4, \tag{10}\] where the integers \(-1,0,1\) are mapped into \(K\). For a proposed Boolean write, choose its content coefficient as the desired bit minus the old bit and its occupation coefficient as the desired occupation minus the old occupation. Set both inactive coefficients to zero. Each coefficient lies in \(\{-1,0,1\}\), and the resulting additive edit is precisely the proposal, in either direction. The vector in (10) is public once \(c\) and \(\sigma\) are fixed; addition by it is defined on all of \(K^{4h}\). The assertion about valid Boolean proposals does not require a validity interpretation for other field-valued inputs.

The necessary public data at a frame are its phase, active tape, write position, rule type, at most two operand addresses, the old content and occupation addresses, and, when applicable, the extra comparison address. A forward fill uses its forward rule; a reverse fill uses its reconstruction rule. Lemma 7 shows that the existence flag is the new comparison result in the only direction where failure is possible, and is one otherwise. These are fixed Boolean decisions once the finitely many addressed bits and public rule data are supplied. Define the decisions on arbitrary Boolean reads by the same formulas, using a fixed default rule and address for unused roles. Their agreement with graph neighbors is asserted on valid input vertices. No global validity check or full circuit evaluation is hidden in an existence flag.

For completeness, the bounded-multiplicity assertion includes more than internal gate edges. Each internal value has boundedly many uses after copy-tree normalization. Each designated output is used once by the other circuit’s input-copy rule and participates in only a bounded number of terminal or external-vector comparisons. Each external-vector bit is used once as an input bit and once for its corresponding terminal comparison. Copied-prefix equations use each full-tape position once. Occupation indicators condition only the rules at their positions; prefix monotonicity, if expressed by adjacent-position tests, reads a position at most twice in each order. Thus all local content, bitness, occupation, gate, copy, comparison, and dummy conditions use bounded-arity records, and each logical position appears as an operand only boundedly often across the fixed list of phases. The requirement that the occupied prefix have its specified length is separate: one may either inspect the prescribed occupation pattern directly, or use prefix monotonicity together with the occupation sum. The latter is a single global count condition for each tape and will be represented separately in the algebraic construction.

All normalization and ordering operations are deterministic. Their records and the two permutations occupy \(O(h\log(N+2))\) bits. Tabulate the transition data for the \(4h\) frames in the same space bound, including both directions and defaults. Scanning the arrays and these records tests membership in \(\mathcal V_s\) in polynomial time. The designated endpoint vectors and the circuit inequalities (8) and (9) give a polynomial-time endpoint decoder. At every fixed stage a valid vertex is determined by the input of its full transcript, since its other tape is a unique computed or copied prefix. Consequently the graph has at most \(4h\,2^{n_0}\) vertices, even though an individual label has only \(O(N)\) bits. The construction outputs the normalized records, public tables, and algorithms, never this potentially exponential vertex list. All constants in these bounds depend only on the fixed Boolean basis and padding cutoff. This proves the remaining uniformity and size assertions. ◻

Proof. First consider a factor of \(H\). The reductions of the upper and lower unit elementary matrices, with their inverses, have a uniform Cayley gap in \(\operatorname{SL}_2(\mathbb{F}_p)\). This is the elementary-generator case of the congruence gap discussed in (Bourgain and Gamburd 2008, 626), and also follows directly from (Bourgain and Gamburd 2008, Theorem 1), since the corresponding fixed subgroup of \(\operatorname{SL}_2(\mathbb Z)\) is non-elementary. Passing to the quotient by the center preserves the upper gap. A half-lazy walk has a uniform absolute gap. The finitely many small primes are absorbed by decreasing this fixed gap.

For odd \(p\), the subgroup \(\operatorname{PSL}_2(\mathbb{F}_p)\) is normal of index two in \(\operatorname{PGL}_2(\mathbb{F}_p)\). Add a representative of the nonsquare determinant class and its inverse; in the index-one case pad with identities. To check a uniform gap, work in an arbitrary unitary representation. The preceding subgroup gap bounds the distance of a vector to its subgroup-invariant projection by a fixed multiple of its maximum displacement under the subgroup labels. Normality makes that invariant subspace invariant under the extra label, which controls its quotient of order at most two. Thus distance to the full invariant subspace is bounded by a fixed multiple of the maximum displacement under all these labels. The three factor projections commute; applying this argument to the three factors gives the same statement for \(H\), with a fixed-size generating list. The regular-representation gap used here applies to every representation of the finite group, by its decomposition into irreducible representations.

We next give a bounded list of translations which, together with these \(H\) labels, expands \(\Gamma\). Consider a block of \(n'\) bits with cycle \(R\). For a nonzero frequency \(y\in\mathbb{F}_2^{n'}\), let \(d'\) be the dimension of the span of its cyclic shifts. Identifying vectors with polynomials modulo \(Z^{n'}-1\), this span is a cyclic ideal. Every such ideal of dimension \(d'\) is specified by a complementary monic divisor of degree \(d'\). There are at most \(2^{d'}\) such divisors and at most \(2^{d'}\) vectors in each ideal. In particular, there are at most \(2^{2d'}\) frequencies with this span dimension. This argument uses only the ideal structure of the polynomial quotient and remains valid when \(Z^{n'}-1\) has repeated factors in characteristic two.

For a uniform seed \(a\in\mathbb{F}_2^{n'}\), the correlation vector \((y\cdot R^ta)_{t=0}^{n'-1}\) is uniform on a shift-invariant linear space of dimension \(d'\). Take \(j_0\) independent seeds. In the product of these spaces, the subset with total weight less than \(j_0n'/4\) is invariant under cyclic shifts and permutation of the seeds. If this subset is nonempty, its uniform distribution has the same marginal at every coordinate, with probability of one at most \(1/4\). An information set of \(j_0d'\) coordinates determines a vector in the product space. Entropy subadditivity consequently bounds the size of this subset by \(2^{j_0d'\mathcal H(1/4)}\), where \(\mathcal H\) is binary entropy. The subset of weight greater than \(3j_0n'/4\) has the same bound, by the marginal entropy estimate with probabilities at least \(3/4\); it is unnecessary for the space to be closed under complementation. Thus a fixed sufficiently large \(j_0\) makes the probability of any failure at any nonzero frequency at most \[ 2\sum_{d'\ge1} 2^{-\{j_0(1-\mathcal H(1/4))-2\}d'}<1. \tag{15}\] There exist \(j_0\) seeds whose cyclic translates have absolute Walsh bias at most \(1/2\) at every nonzero frequency. Enumerating all seed tuples and checking their biases constructs them in time \(2^{O(r)}\), which is polynomial in \(N\).

Take the Cartesian product of the three block seed lists. Averaging its translations under \(\langle R_1\rangle\times\langle R_2\rangle \times\langle R_3\rangle\) has absolute Walsh bias at most \(1/2\) off zero: the three factors multiply, and a nonzero frequency has a nonzero block. Averaging further over cosets in \(H\) preserves this bound. Denote by \(T\) the average of the resulting \(H\)-conjugates of seed translations. On the orthogonal complement of \(G_0\)-invariants, \(T\) has all eigenvalues in \([-1/2,1/2]\), by Fourier decomposition for \(G_0\).

Let \(v\) be a unit vector in a representation of \(\Gamma\), and let \(\eta\) be its maximum displacement under the fixed \(H\) labels and the fixed product-seed translations. The \(H\)-invariant projection \(v_H\) satisfies \(\|v-v_H\|\le K\eta\) for an absolute \(K\). Its displacement under any seed translation is at most \((1+2K)\eta\). Since \(v_H\) is \(H\)-invariant, the same holds for every \(H\)-conjugate of a seed. Writing \(P_{G_0}\) for projection to \(G_0\)-invariants gives \[\|v_H-P_{G_0}v_H\|^2 \le 2\langle v_H,(I-T)v_H\rangle \le (1+2K)^2\eta^2.\] Normality of \(G_0\) implies that \(P_{G_0}v_H\) is also \(H\)-invariant. Distance to the \(\Gamma\)-invariant subspace is therefore at most a fixed multiple of \(\eta\). The symmetric half-lazy average on our fixed generating list has a uniform positive gap: its Dirichlet form is the average of squared label displacements divided by a fixed constant. Its spectrum is nonnegative. A fixed power of this walk has mean-zero norm at most the requested \(\lambda\). Reversing words shows that the powered list remains symmetric. Its length is fixed, and the same conclusion holds for left and right regular actions. ◻

Proof. The maximal-minor condition gives star distance at least \(c_0+1\ge\delta_0d_0\): a nonzero word of smaller support would give a linear dependence among at most \(c_0\) columns, which could be enlarged to a dependence among \(c_0\) columns. This also proves the assertion for vector entries, either by applying a nonzero scalar component or by solving the independent-column equations componentwise.

For a nonzero whole local word, let \(l,u\) be the fractions of left and right base vertices incident to its support, and let \(a=\max(l,u)\). Its edge-support fraction \(e\) obeys, by star distance and mixing, \[\delta_0a\le e\le lu+\lambda_0\sqrt{lu} \le a(a+\lambda_0).\] Hence \(a\ge\delta_0-\lambda_0\) and \(e\ge\delta_1\). Mixing here and below follows by subtracting the two constant means and applying the cross-part operator norm to the indicator functions.

For agreement, apply the A-base checks to the columns of \(F\). Mark every base star at which any check syndrome is nonzero. Each nonzero syndrome, as a row indexed by the \(d\) columns, is a scalar linear combination of B-code rows, and is therefore a nonzero B-codeword over \(U\). Its support has size at least \(\delta_1d\). In each such column there must be a discrepancy with \(D\) on an edge incident to the marked star, since \(D\) satisfies that star’s check. A discrepancy cell is incident to at most two base stars. If \(w_0\) is the total marked-star count divided by \(n_b\) (counting both base sides), then \[ w_0\le \frac{2zd^2}{\delta_1dn_b} =\frac{2d_0z}{\delta_1}. \tag{19}\]

We now confine every low-discrepancy difference column to edges inside a small set of base vertices. Deleting those row indices, together with the columns having large discrepancy, will leave a rectangle on which \(F\) and \(D\) agree.

Close the marked set by adding a vertex whenever at least \((\delta_0/2)d_0\) incident edges lead to the set. If the initial set is empty it stays empty. Otherwise suppose its normalized size first reaches \(w\ge2w_0\). A single addition is at most \(1/n_b\le w_0\), so \(w\le3w_0\). Edges made internal by additions give internal edge fraction at least \((\delta_0/2)(w-w_0)\). Mixing gives the upper bound \(w^2/4+\lambda_0w/2\). Since \(w\ge2w_0\), these inequalities imply \(\delta_0\le w+2\lambda_0\). They are incompatible when \(3w_0<\delta_0-2\lambda_0\). For sufficiently small \(z\), therefore, the final closure \(T\) satisfies \(|T|/n_b\le2w_0\), with strict inequality when \(w_0>0\). Every star outside \(T\) still satisfies all checks on \(F\), and fewer than \((\delta_0/2)d_0\) of its edges enter \(T\).

Fix a constant \[0<z_0<\delta_0(\delta_0/2-\lambda_0).\] Consider a column whose discrepancy fraction is less than \(z_0\). The difference between its \(F\) and \(D\) columns satisfies all checks outside \(T\). An outside vertex incident to its support consequently has at least \(\delta_0d_0\) support edges in total and more than \((\delta_0/2)d_0\) support edges to other outside vertices. The left and right fractions of such outside vertices are each at most \(z_0/\delta_0\), by counting their total support edges. If \(a\) is their maximum fraction, mixing on the outside support would give \[(\delta_0/2)a\le a(a+\lambda_0), \qquad a\le z_0/\delta_0<\delta_0/2-\lambda_0.\] Thus \(a=0\). The difference column vanishes on every edge having an endpoint outside \(T\).

Delete the row indices corresponding to edges internal to \(T\), and delete columns with discrepancy fraction at least \(z_0\). The former fraction is at most \(|T|/(2n_b)\le w_0\), since each internal edge consumes two incidences in \(T\), and the latter fraction is at most \(z/z_0\). The two tables agree on the complementary rectangle. Choose a fixed \(z_*>0\), depending only on the base parameters, so small that for \(z<z_*\) the closure inequality holds and each deleted fraction is less than \(\delta_1\). Puncturing either scalar local code to its retained coordinates is then injective by distance. Its inverse on the image is a scalar linear map. Lift the common rectangle in the B direction and then in the A direction. Applying scalar linear maps in one direction preserves the constraints in the other; hence the resulting table belongs to the full tensor code. By injectivity it agrees with every retained whole row of \(F\) and every retained whole column of \(D\). This gives (18) with \(2d_0/\delta_1+1/z_0\) for \(z<z_*\). For \(z\ge z_*\), use the zero tensor table and the bound \(2\le(2/z_*)z\). The maximum of these two constants is a suitable \(C_0\). All lifting maps and all support counts act on joint vector entries, so no dimension factor occurs. ◻

Proof. Consider one A-axis system. Eliminate part-one variables with the A-edge equations. At each \(k\), the two types of base-star checks in part zero contribute \(2c_0s_b^2\) equations; those in part one contribute the same number after substitution. There are exactly \(q_{\rm par}=4c_0s_b^2\) parity-label variables at part zero for each \(k\), so the resulting parity system is square, also after scalarizing \(U\). Its entries are linear polynomials in the entries of the four A check matrices.

Its determinant polynomial is nonzero in the prime characteristic. For this purpose partition the \(4c_0\) parity permutation numbers into four disjoint sets of \(c_0\) numbers, one for each pair consisting of an outer part and a base side. Specialize each associated check matrix to selectors of its set. For a fixed permutation number, every label-index edge occurs exactly once at the specified base side. At outer part zero its selected coordinate is unshifted; at part one it is pulled back through an invertible group shift and an invertible entry twist. Thus every scalarized parity coordinate is selected exactly once, up to an invertible block and a permutation. The specialized parity matrix is invertible. The same proof works for the B axis and for every allowed twist type. It does not require this selector specialization itself to have the desired maximal minors: it separately witnesses that each determinant is a nonzero polynomial. Each maximal-minor polynomial is also nonzero. Their product is nonzero because a polynomial ring over a field is an integral domain.

Here is a degree bound that justifies this field choice without reference to any future number of slots. There are exactly \[ 8c_0d_0 \tag{27}\] scalar indeterminates. Scalarizing a one-axis parity matrix gives dimension at most \[ q_{\rm par}|\Gamma|\dim_JU \le q_{\rm par}m|H|^3\le q_{\rm par}mr^{27}. \tag{28}\] Its determinant has degree at most this number. At most \(2(1+3\cdot4)=26\) axis systems cover every required type, with redundancies harmless. The product of the maximal minors of the eight check matrices has degree \(8c_0\binom{d_0}{c_0}\). Thus the total degree is at most \[ 26q_{\rm par}mr^{27}+8c_0\binom{d_0}{c_0}<m^3. \tag{29}\] For the last inequality increase the fixed cutoff so that \(r^{27}\le m\), \(m\ge2\cdot26q_{\rm par}\), and \(m^2\ge2\cdot8c_0\binom{d_0}{c_0}\). The first term is then at most \(m^3/2\) and the second at most \(m^2/2<m^3/2\). The exponent three is independent of \(s_b\); only the cutoff depends on the already fixed local degree.

A nonzero polynomial of total degree less than a finite field’s cardinality cannot vanish on every tuple over that field. For completeness, view it as a polynomial in the last variable; by induction choose the other variables so that a nonzero leading coefficient remains nonzero, and then use the univariate root bound. Since \(|J|=p^4>m^3\), such a tuple exists in \(J\). Enumerate all tuples of the fixed number (27) of field elements, testing maximal minors and parity ranks, until one succeeds. The field cardinality and every matrix dimension are polynomial in \(N\), so this is a deterministic polynomial-time algorithm with a fixed exponent. A direct sum of already invertible parity systems is invertible with the direct sum of their inverses. It introduces no new polynomial condition, even when the number of slots grows with \(N\).

It remains to justify two-axis extension. Regard an A parity matrix as a matrix of operators on \(U^\Gamma\): each entry is a scalar combination of left translations and A twists. B entries are scalar combinations of right translations and B twists. They commute entrywise across axes. An invertible A parity matrix \(L_A\) therefore intertwines the diagonal actions of any B-entry operator \(T\) on its domain and codomain. From \(L_AT=TL_A\) one obtains \(L_A^{-1}T=TL_A^{-1}\), with the same indexed domain and codomain interpretation. Thus the operators making up either axis encoder commute with every entry operator of the other axis encoder, including its inverse parity solve.

Start with the systematic rectangle at part \((0,0)\). Extend along A for every systematic B column and then along B for every resulting A row. The second extension preserves all first-axis constraints by this commutation. Both encoders leave their systematic entries unchanged. Reversing their order gives the same map. Finally, one-axis uniqueness applied in both directions shows that a full word is uniquely determined by its systematic rectangle. Gaussian elimination computes these extensions in polynomial time in \(N\), or in polynomial time in the total explicit input size for an arbitrary direct sum. ◻

Proof. First replace every locally invalid whole tuple at a vertex by zero. There are at most \(\theta|V|\) such vertices. Initially at most \(d\theta|V|\) undirected edges conflict, and this replacement creates at most \(2d\theta|V|\) further conflicts. Starting with this locally valid word, repeatedly replace a whole vertex by a locally valid tuple whenever that strictly decreases its number of incident conflicting edges. The total integer conflict count strictly decreases, so at most \(3d\theta|V|\) replacements occur. This argument establishes existence and termination; it is not asserted to be an efficient search through the alphabet. At most \((1+3d)\theta|V|\) vertices have been touched, and the final conflict count is no larger than the count before the replacements.

At a stable vertex \(v\), let \(p_A(v),p_B(v)\) be the fractions of its A and B edges that conflict, and put \(p(v)=p_A(v)+p_B(v)\) and \(\mu=\mathbb{E}_Vp\). Neighbors across A edges suggest rows, transported by the appropriate twist or inverse twist. They are valid B-code rows. Neighbors across B edges similarly suggest valid A-code columns. At cell \((i,j)\) these suggestions agree unless at least one of the two opposite square edges conflicts: the common far corner and commuting twists supply the equality when both opposite edges agree. If \(P_A,P_B\) average over the respective neighbor maps, their cell-disagreement fraction is at most \(P_Ap_B(v)+P_Bp_A(v)\). Lemma 10 gives a local replacement whose incident conflict fraction is at most \(C_0\) times this number. Stability therefore gives pointwise \[ p\le C_0(P_Ap_B+P_Bp_A)\le C_0(P_Ap+P_Bp). \tag{32}\]

All norms and inner products in this proof use uniform normalized counting measure on \(V\). Let \(\bar p\) be the function equal to the mean of \(p\) on each of the four parts. Nonnegativity gives \(\|\bar p\|_2\le2\mu\). Each neighbor operator permutes the part means and has norm at most \(\lambda\) on their orthogonal complement. Consequently (32) implies \[\|p\|_2\le2C_0(2\mu+\lambda\|p\|_2), \qquad \|p\|_2\le C_1\mu,\quad C_1=8C_0,\] by (20). This bound has no dependence on \(d\).

Fix an A label \(i\), let \(S_i\) be the vertices whose incident A edge of that label conflicts, and let \(p_i=\Pr_V(S_i)\). At such an edge the difference of its two transported rows is a nonzero B-codeword, so it has at least \(\delta_1d\) nonzero cells. In each corresponding B direction, either a B edge conflicts at one A endpoint or an \(i\)-label A edge conflicts at the opposite B neighbor. The involution exchanging the two A endpoints preserves \(S_i\). Averaging this implication, and then subtracting the four part means in the mixing term, yields \[\begin{align*} \delta_1p_i &\le 2\mathbb{E}_V[1_{S_i}p_B] +\langle1_{S_i},P_B1_{S_i}\rangle \\ &\le 2\mathbb{E}_V[1_{S_i}p_B]+4p_i^2+\lambda p_i. \tag{33}\end{align*}\] Indeed, the squared norm of the four part means of \(1_{S_i}\) is at most \(4p_i^2\), and the squared norm of its remaining part is at most \(p_i\). Also \(p_i\le d\mu\). For sufficiently small \(\mu\), depending on the now fixed \(d\), we have \(4d\mu+\lambda<\delta_1/2\). Average (33) over \(i\) and repeat the argument with A and B exchanged. It follows that \[ (\delta_1/2)\mu \le4\mathbb{E}_V[p_Ap_B]\le4\mathbb{E}_V[p^2]\le4C_1^2\mu^2. \tag{34}\] If \(0<\mu<\delta_1/(8C_1^2)\) this is impossible. Since the initial zeroing left at most \(3d\theta|V|\) conflicts, stability has \(\mu\le6\theta\). For example, choose \(\theta_*\) so that \(6\theta_*<\min\{\delta_1/(32d),\delta_1/(16C_1^2)\}\). Then \(\mu=0\). The final word is exact, and (31) gives \(K_*=4(1+3d)\) as a permissible proximity constant for this normalization. Common scalar local checks, block diagonal twists, and joint conflict events justify every step for an arbitrary tuple without a slot-count factor. ◻

Proof. For one A slice with fixed \(t\), a nonzero vertex has at least \(\delta_1d\) nonzero row symbols by local distance. Each is carried to a nonzero symbol at its opposite endpoint, because twists are invertible. If \(l,u\) are the two vertex-support fractions and \(a=\max(l,u)\), the fraction \(e\) of nonzero carried edges obeys \[\delta_1a\le e\le lu+\lambda\sqrt{lu}\le a(a+\lambda).\] Thus \(a\ge\delta_1-\lambda\). Support on these two parts is at least \((\delta_1-\lambda)/2\) in their own normalization and at least \(\Delta_A\) in the four-part normalization. At least one slice is nonzero. The argument for B, differences, and joint entries is identical.

For two systematic A row labels, their difference at \(s=0\), considered over both \(t\) parts and all \(k\), is a B-only word: the scalar B checks and B twists are the same for both rows. If nonzero it has the distance just proved. Differences between systematic B columns are A-only words. A nonduplicated systematic rectangle contains two unequal entries connected either by a change of its A label or a change of its B label, so one of these comparisons is nonzero. Conversely, for a duplicated payload, B-axis uniqueness extends the same systematic row data identically at every systematic A label, and A-axis uniqueness does the analogous thing for columns.

For the last assertion, if \(v=w\), A-axis uniqueness identifies the two whole columns at every systematic B label. If \(v\ne w\), a systematic payload cell differs somewhere, so one of the compared column differences is a nonzero A-only word and has support at least \(\Delta_A\). The B-sharing assertion is proved in the same way. These comparisons use whole one-axis codewords, which is why an arbitrary localized payload disagreement has a constant exact gap. ◻

Proof. Let \(S\) be the joint vertex-disagreement set. At each vertex in \(S\), local distance gives at least \(\delta_1d\) nonzero difference rows. For each corresponding label, either the other endpoint also lies in \(S\), or agreement of \(V_0\) forces an actual conflict of \(W\). Consequently \[\delta_1p\le z_A+\langle1_S,P_A1_S\rangle \le z_A+4p^2+\lambda p,\] by the four-part mixing bound used above. For \(p\le\delta_1/16\) and (20), \(4p+\lambda<\delta_1/2\), giving the stated rearrangement. The proof concerns one fixed received word and one joint reference. It can be applied to successively larger prefixes of a tuple without modifying the received word or accumulating a number-of-prefixes loss. ◻

Proof. Parts (i) and (ii) follow from Lemmas 9 and 11, the field construction, and the coordinate count after (30). Part (iii) is Lemma 10, Lemma 13, and the parsing and exact-gap argument following (36). Decrease \(\theta_{\mathrm{out}}\) and increase \(K_{\mathrm{out}}\) once to cover those fixed costs. Part (iv) is Lemmas 14 and 15. The degree and dependency assertions are (27)– (29) and the parameter order fixed in (20). No external local-testability theorem is used for these specialized conclusions. ◻

Proof. At a target part \((k,0,t)\), take the row of label \(i\) from \((a_ik,1,t)\) and apply \(\alpha_i^{-1}\). At \((k,1,t)\), take it from \((a_i^{-1}k,0,t)\) and apply \(\alpha_i\). Combine all other indices and all slots into one row-symbol vector. Decode these \(d\) row suggestions in \(C_A^s\) up to strictly fewer than \(\delta_1d/2\) joint row errors. There is at most one such local word by the distance in Lemma 10. A total deterministic implementation enumerates all subsets \(T\subseteq[d]\) with \(|T|>d-\delta_1d/2\), solves the local scalar constraints together with the suggested values on \(T\) componentwise, and verifies that the candidate has fewer than \(\delta_1d/2\) joint row errors. Such a puncturing is injective by local distance, so each consistent system gives at most one candidate. If the distance promise holds, the set of all correct suggestions is one enumerated \(T\) and gives the required word. Return zero if no candidate passes. Malformed neighbor symbols are first replaced by the fixed parsable default. Restore each control bit by majority on the forward A-neighbor list, with fixed tie behavior, and write canonical padding.

If \(k\notin S'\), each relevant list contains fewer than \(\delta_1d/2\) positions of \(S\). Every other row suggestion equals the corresponding row of \(V_0\), by its exact A agreement. Thus the local decoder recovers all four reference parts and all slots jointly. The same good-neighbor count is strictly below \(d/2\), so control majorities are also correct. This proves the support containment for every assignment of values on \(S\).

For either forward or inverse averaging operator \(P\) on \(\Gamma\), the mean-zero bound gives \[\mathbb{E}_k(P1_S(k)-u)^2 \le\lambda^2u(1-u)\le\lambda^2u.\] When \(u<\delta_1/4\), Chebyshev’s inequality at threshold \(\delta_1/2-u>0\) and a union bound for the two lists prove the first inequality in (38). Its right side is then at most \(32\lambda^2u/\delta_1^2\le u/2\) by (20).

Iterate the deterministic operation on supports in (37). The preceding reasoning holds for every completion at each step, so the same iterated supports contain all possible errors. A depth-\(q\) dependency cone is obtained by composing at most \(q\) forward or inverse A moves, with the finite part and slot bookkeeping. For fixed \(q\) this is a fixed finite list of permutations. A consistent assignment to repeated initial addresses in one cone extends to a global initial word agreeing with \(V_0\) outside \(S\). Applying the global support statement to that extension proves the claimed result for that cone. This argument can use a different global extension for each target.

Assume now \(|S|/|\Gamma|<\delta_1/4\). Every iterated support stays in this regime, so its integer cardinality decreases by a factor of at least two while nonempty. More than \(\log_2|\Gamma|\) rounds make it zero. Running these rounds synchronously on the complete array uses \(O(|\Gamma|\log|\Gamma|)\) local calls, each of polynomial bit complexity as established above. This proves polynomial-time global correction without using the existential greedy repair in Lemma 13 as an algorithm. ◻

Proof. A bit-conjunction mask is a product of one-bit masks, applied in sequence. For the integer interval \([0,a)\) with \(0\le a\le M_o\), represent \(a\) by \(r+1\) public or already identical control bits. Use the zero operator for \(a=0\) and the identity for \(a=M_o\). For \(0<a<M_o\), use the disjoint prefix rectangles obtained by specifying the most significant differing bit: at a position where \(a\) has bit one, match its more significant bits and require the current bit to be zero. There are at most \(r\) rectangles. More explicitly, writing \(a_r\) for the endpoint bit, one fixed padded program applies the mask \[a_r+(1-a_r)\sum_{i=0}^{r-1}a_i\, 1[x_i=0]\prod_{j=i+1}^{r-1}1[x_j=a_j].\] All endpoint decisions and rectangle coefficients are identical at every index; the program keeps all candidate stages and uses scalar coefficient selection, so its topology and polynomial size do not depend on \(a\). Differences of two such masks give arbitrary intervals.

Let \(m\) be the indicator of a conjunction not involving bit \(i\). The pullback of the permutation that flips bit \(i\) precisely when \(m=1\) is \[ f-mf+R_{(e_i,1)}(mf). \tag{39}\] To verify this, if \(m(x)=0\) then \(m(x+e_i)=0\), and the result is \(f(x)\); if \(m(x)=1\) then \(m(x+e_i)=1\), and the result is \(f(x+e_i)\). The independence of \(m\) from the flipped bit is essential here. Three controlled XOR operations exchange two index bits, so they implement bit reversal and any prescribed bit permutation.

For an integer subtraction of \(2^j\) modulo \(2^r\), flip bit \(i>j\) when the original bits \(j,\ldots,i-1\) are all zero, and flip bit \(j\) unconditionally. Process the higher bits in descending order; then none of the bits used by a condition has yet changed. The addition rule uses ones instead of zeros. Pullbacks reverse the chronological composition of index permutations: thus the table stages apply these borrow gates in ascending bit order, the reverse of their descending index-permutation order. This implements the desired cyclic table shift. A conjunction uses \(O(r)\) bit operations, so this procedure is polynomial in \(r\).

For the Fourier transform we realize the radix-two Cooley–Tukey decomposition (Cooley and Tukey 1965, 299–300) by the certified full operations above. Let \(D=2^v\in\{h,M_o\}\) and let \(\xi=\zeta^{M_o/D}\) have order \(D\). The transform acts on the low \(v\) integer bits, independently within each block of fixed higher bits, and is \[ \mathcal F_D(f)(y)=\sum_{z=0}^{D-1}\xi^{yz}f(z). \tag{40}\] First reverse these \(v\) bits. At level \(j\), pair positions separated by XOR of bit \(j-1\) in each aligned window of length \(2^j\). Writing \(a<2^{j-1}\) for the offset and \(U,V\) for the lower and upper entries, replace the pair by \[ U+\xi^{aD/2^j}V,\qquad U-\xi^{aD/2^j}V. \tag{41}\] The factor is a product of one-bit factors, since if \(a=\sum_{i<j-1}2^ia_i\), then \(\xi^{aD/2^j}=\prod_{i<j-1}(\xi^{2^iD/2^j})^{a_i}\). Half-window masks, the bit pull, these factors, and addition implement the displayed rule. The identity \[\sum_{z=0}^{D-1}\xi^{yz}f(z) =\sum_{z=0}^{D/2-1}(\xi^2)^{yz}f(2z) +\xi^y\sum_{z=0}^{D/2-1}(\xi^2)^{yz}f(2z+1)\] proves the algorithm by induction, with bit reversal placing the recursive even and odd subproblems in the required order. More explicitly, if \(\operatorname{rev}_a\) reverses \(a\) bits, after level \(j\) the entry at \(b2^j+y\), \(0\le y<2^j\), is \[\sum_{z=0}^{2^j-1}(\xi^{D/2^j})^{yz} f\bigl(\operatorname{rev}_{v-j}(b)+2^{v-j}z\bigr).\] The level-\(j\) butterfly combines the even and odd values of \(z\) in the level-\((j-1)\) formula, proving this invariant from the bit-reversed input at level zero; at level \(v\) it is (40). Using \(\xi^{-1}\) and multiplying by \(D^{-1}\) gives the inverse: \(\sum_{y=0}^{D-1}\xi^{y(z-z')}=D\,1[z=z']\). Without initial bit reversal, apply the sum/difference butterflies directly to the input table, one coordinate bit at a time, and use no twiddle factors. This gives \[ \mathcal W(f)(x)=\sum_y(-1)^{x\cdot y}f(y). \tag{42}\] They can be applied on all \(r\) bits or just a specified block. The Walsh inverse is \(M_o^{-1}\mathcal W\) when all bits are used.

Finally set \(\omega=\zeta^{M_o/h}\) and \[ L_j(Z)=h^{-1}\sum_{a=0}^{h-1}\omega^{-ja}Z^a. \tag{43}\] The root sum just used gives \(L_j(\omega^i)=1[i=j]\). For a length-\(M_o\) coefficient table \(F\), cyclic multiplication by \(L_j\) has coefficient at \(w\) equal to \[ h^{-1}\omega^{-jw}\sum_{a=0}^{h-1}F_{w-a}\omega^{j(w-a)}, \tag{44}\] with subscripts modulo \(M_o\). The powers are well defined under cyclic indexing because \(h\mid M_o\). Each of the two diagonal factors splits over the bits of \(w\) and has coefficients computable from \(j\). If \(T_bf(w)=f(w-b\bmod M_o)\), the middle window sum is \[\prod_{i=0}^{\ell-1}(I+T_{2^i}).\] Every integer in \([0,h)\) has a unique binary expansion, proving this identity. The previously constructed shifts implement it. When \(\deg(F L_j)<M_o\), cyclic and ordinary multiplication coincide; we impose this degree bound at every ordinary-product use.

For clarity, crude stage bounds suffice: a bit operation uses \(O(r)\) elementary stages, a conjunction \(O(r^2)\), a carry shift \(O(r^3)\), and the window product \(O(r^4)\). The Fourier, Walsh, and range-mask constructions also fit a fixed polynomial bound. Coefficient calculation, layout descriptions and every elementary local operation use polynomially many bit operations in \(r\). Padding unused steps with zero or identity operations makes all lengths independent of the particular control or address values. ◻

Proof. Theorem 16 first repairs parsing, repetition and full codes at \(O(\theta)\) symbol cost. A repeated illegal clock is excluded by its range test. The full-code duplication gap then excludes any failure of duplicated payload, for small enough \(\theta\). Replace all locally A-invalid scratch parts by zero. This is one further packed \(O(\theta)\) change. Call the resulting word \(W\), and keep this word fixed throughout the following induction.

If preprocessing changed at most \(C_{\mathrm{pre}}\theta\) packed sites, any test using \(\Pi\) can change its outcome only on their \(q\) inverse images. After harmless fixed conversions of edge and part normalizations there are constants \(C_z,C_r\) such that \[ z_A(W)\le C_z\theta,\qquad \Pr[\text{some scratch recurrence or inactive-zero test fails on }W] \le C_r\theta. \tag{45}\] One can use constant multiples of \(1+qC_{\mathrm{pre}}\) for both constants. These bounds concern the entire packed scratch tuple, so they contain no slot-count factor.

Order all initialized families topologically, putting public focus first, and include the inactive-zero families with their zero references. Let \(V_j\) be the exact reference of the first \(j\) families on the corrected full parents and legal clock, and let \(p_j\) be the joint part distance from the corresponding prefix of \(W\) to \(V_j\). The empty prefix has \(p_0=0\). The full parents may have incorrect advertised identities, but are A-coded; every allowed initial \(X\) is A-coded on such parents. Right pulls and identical coefficients preserve this property. Public focus begins with hardwired correct constant encodings and the identical clock. Its completed reference supplies globally identical coefficients to subsequent recurrences. Consequently every \(V_j\) is exactly A-coded.

An error in the new family occurs only at a recurrence-failure center or at a center reading an erroneous earlier part. A joint part-error set of density \(p_j\) occupies at most \(4p_j\) of the packed sites. Taking a union over the \(q\) maps, and retaining the old prefix, gives \[ p_{j+1}\le C_r\theta+(1+4q)p_j. \tag{46}\] This remains true when a recurrence reads all earlier slots or types at one of those sites: the error event is already joint. Put \(K=2C_z/\delta_1\) and choose \(\theta_{\mathrm{sc}}\) so small that \[ (C_r+(1+4q)K)\theta_{\mathrm{sc}}<\delta_1/16. \tag{47}\] If \(p_j\le K\theta\), the provisional estimate is in the small-error range of the A near-code inequality of Theorem 16. Apply that inequality to the same fixed word \(W\), restricted to the enlarged tuple, and to \(V_{j+1}\): \[\delta_1p_{j+1} \le z_A(W|_{j+1})+4p_{j+1}^2+\lambda p_{j+1}.\] The conflict count of a prefix is at most that of the whole tuple. Since \(\lambda\le\delta_1/8\) and \(p_{j+1}<\delta_1/16\), this implies \[p_{j+1}\le 2z_A(W)/\delta_1\le K\theta.\] Induction proves this bound for the complete scratch tuple. It resets an estimate, without making successive word repairs. Only now replace the whole scratch tuple by its reference, at symbol cost at most \(4K\theta\). The common scalar local checks act on joint vectors, and the finitely many twist types act by a block-diagonal invertible map; the near-code estimate is therefore valid in exactly this joint metric. Together with preprocessing this proves the lemma. ◻

Proof. Write the operation’s local expression as \(X\) and its duplicated systematic payload as \(v\). For each label, part and entry coordinate expand in the \(x\) variable: \[X(x,u)=\sum_{\nu\in\mathbb F_2^r}\widehat X_\nu(u)(-1)^{x\cdot\nu}, \qquad \widehat X_\nu(u)=M_o^{-1}\sum_xX(x,u)(-1)^{x\cdot\nu}.\] For \(0\le\tau\le M_o\) define a Fourier multiplier \(P_\tau\) by \[ w_\tau(\nu)=|H|^{-1}\sum_{a\in H} 1[\underline{a^{-1}\nu}<\tau]. \tag{48}\] Thus \(P_0=0\) and \(P_{M_o}=I\). The inverses of \(|H|\) and \(M_o\) exist in \(J\). The multipliers are constant on frequency orbits of \(H\); they are not asserted to be projections.

Here is the required commutation in detail. A left pull by \((w,a)\) sends \((x,u)\) to \((x+u^{-1}a^{-1}w,au)\), so it preserves each frequency, changing its coefficient by a known sign and an \(H\)-index permutation. A right pull sends \((x,u)\) to \((a^{-1}(x+w),ua)\), carrying a frequency \(\nu\) to \(a\nu\), with sign \((-1)^{w\cdot a\nu}\). Hence \(P_\tau\) commutes with both pulls. The constant entry twists act on a different coordinate and also commute. Every parity operator and every systematic injection thus intertwines \(P_\tau\) on its domain and codomain. If an invertible parity operator \(T\) satisfies \(TP_\tau=P_\tau T\), then its inverse does too, by multiplication by \(T^{-1}\) on both sides. Applying the two one-axis extensions gives \[ P_\tau E_{\mathrm{out}}v =E_{\mathrm{out}}(P_\tau v). \tag{49}\] No commutation with a preliminary index-dependent operation such as \(W(k)\mapsto W(k)\rho_e(k)\) is needed: \(P_\tau\) is applied to its already formed expression \(X\).

The mode-bit selector \[ \frac{I+(-1)^bR_{(e_i,1)}}2 \tag{50}\] retains precisely those frequencies with \(\nu_i=b\). For each \(a\in H\), decompose \(\underline{a^{-1}\nu}<\tau\) into at most \(r\) disjoint prefix rectangles and multiply their selectors. Sum over rectangles and average over \(a\). This gives an A-only program computing \(P_\tau X\) with \(\mathop{\mathrm{poly}}(r)\) stages. Include all candidate rectangles and use coefficient bits from the microclock, so topology and length are fixed. The case \(\tau=M_o\) uses the identity with the same padding. All selectors use the elementary pull list via stored bit alignments.

The partial target at cutoff \(\tau\) is \(Y_\tau=E_{\mathrm{out}}(P_\tau v)\). Compare it with the completed cutoff program using the shared-axis test of Definition 18. In the shared-B case, intermediate scratch is only A-coded. The test’s justification is made after Lemma 20: the completed reference is then exactly \(P_\tau X\), which satisfies the target’s B constraints by the commutation above. One may now use B distance on its whole systematic A rows. This argument neither assumes nor tests B validity of unfinished scratch. The shared-A case uses the analogous columns. Thus equality of the required payload suffices, and its failure has the same constant gap at every cutoff.

It remains to compute a cutoff increment locally. Let \(a_\tau\) be the bit vector for the integer \(\tau<M_o\), and set \(O=Ha_\tau\). The increment multiplier is zero outside \(O\) and, for \(\nu\in O\), is \[ (w_{\tau+1}-w_\tau)(\nu) =\frac{\#\{a\in H:aa_\tau=\nu\}}{|H|} =\frac1{|O|}. \tag{51}\] For each \(\nu\) in the fixed-length list \((aa_\tau)_{a\in H}\), apply all \(r\) mode selectors to \(X\). Repetitions are harmless. The resulting pure-mode slot is \(X_\nu(x,u)=(-1)^{x\cdot\nu}\widehat X_\nu(u)\). Also store each right pull \(R_{(0,b)}X_\nu\), \(b\in H\), through generator paths and their intermediate stages. At the current \(k=(x,u)\) its systematic payload is \[ (-1)^{(b^{-1}x)\cdot\nu}\widehat v_\nu(ub). \tag{52}\] For any desired \(u'\in H\), take \(b=u^{-1}u'\) and remove the displayed known sign. One symbol now contains every coefficient \(\widehat v_\nu(u')\) for \(\nu\in O\) and every \(u'\in H\). These are read from locally stored pull slots, not from remote global payload positions.

We can apply \(E_{\mathrm{out}}\) to this coefficient list locally. Remark 12 supplies the inverse of each one-axis parity system on the \(O\)-frequency subspace: both this subspace and its complement are invariant, and the restricted domain and codomain have equal dimensions. Here its Fourier coordinates are indexed by frequency, \(H\), labels, parts and entry coordinates, so the restricted dimension is at most \[ C|O|\,|H|\,\dim_J U\le C|H|^4=\mathop{\mathrm{poly}}(r), \tag{53}\] where \(C\) depends only on the fixed labels, and \(\dim_JU\le |H|^2\). Form its entries using the explicit pulls and Walsh signs, solve the two successive axis systems by Gaussian elimination, and sum the output modes at \(x\). Together with (51), this computes every local entry of \[E_{\mathrm{out}}((P_{\tau+1}-P_\tau)v).\] Matrix assembly, elimination and field arithmetic take \(\mathop{\mathrm{poly}}(r)\) bit operations. Canonical parsing and fixed defaults on malformed values, illegal clocks or failed pivots make the local algorithm total; on the promised data the prescribed matrices are invertible.

Use two cutoff-program buffers and one orbit-focus buffer. Initially the target and all three buffers are zero. At iteration \(\tau\) keep the completed buffer for cutoff \(\tau\) when \(\tau>0\), and compare the target with it; at \(\tau=0\) compare the entire target with zero. In the other, empty buffer fill the cutoff-\(\tau+1\) program in dependency order, and fill the orbit focus in dependency order. With both complete, perform one pivot adding the local encoded increment to the target. Its required comparison now uses the completed cutoff-\(\tau+1\) buffer. Erase focus in reverse order and erase the old cutoff buffer in reverse order when present. Swap the buffer roles, determined by the iteration parity. At cutoff \(M_o\), compare the target directly with \(X\) while erasing the final cutoff buffer. This finishes with the full desired target and zero temporary scratch.

At every clock value enforce the full-code and duplication constraints of the target, all initialized-prefix recurrences, inactive zeros, and the stated comparison. While a new proof is being prepared, a completed old proof remains available. At a pivot both the next proof and the increment focus are complete. In reverse traversal, erased prefixes are first reconstructed in forward dependency order, so the reverse pivot subtracts the same locally available increment. Thus both directions are local, mutually inverse on canonical data, and never use a partial certificate as a completed one.

For the size bound, each cutoff program uses at most \(O(|H|r^3)\) elementary stages up to fixed padding factors. The orbit selectors and all right-\(H\) paths use at most \(O(|H|r^2+|H|^3)\) such stages, with a polynomial allowance for metadata. Even a bound \(O(r^{30})\) for both programs and their descriptions suffices. Each entry alphabet has at most \(r^{18}\) field coordinates, each of \(O(r)\) bits. The two reused buffers therefore have \(\mathop{\mathrm{poly}}(r)\) bits per index. There are \(M_o\) iterations of a common polynomial sublength, with a special initial omission and final erasure; their location is decoded by arithmetic on a logarithmic microclock. No local step loops over all \(M_o\) modes. The different cutoffs reuse the same zeroed buffers and do not contribute a factor \(M_o\) to the word length. Separate buffers for the finitely many required A types keep every slot’s type fixed. These observations prove all bounds and claims of the lemma. ◻

Proof. Sparse row equations. Use the normalization in Lemma 8. The Boolean tests for the four arrays are \(z(z-1)=0\) at each row, and content must vanish where occupation is zero, by \(a(1-e)=0\). For occupation in a prescribed order \(\pi\), impose \[e_{\pi(i+1)}(1-e_{\pi(i)})=0\quad(0\le i<h-1).\] Together with Booleanity, these equations say that occupied positions form a prefix. Its desired length is imposed separately by its integer count. Full occupation may instead be imposed row by row. Fixed gate truth tables have multilinear representing polynomials over \(J\): for a Boolean input \(a\in\{0,1\}^m\) its indicator is \(\prod_{i:a_i=1}z_i\prod_{i:a_i=0}(1-z_i)\), so summing the indicators weighted by the truth-table values gives the desired polynomial. The arity is fixed. Gate, input-copy, designated-comparison, dummy, and tape-to-tape-copy equations are conditioned by the occupation of their destination where appropriate. This expresses exactly the phase rules in Section 2; the phase prescription ensures that an occupied computation only depends on earlier occupied positions or the fixed full tape. In a full \(Q_x\), its \(S\) inputs are free, with the terminal and other-input relations imposed as in its definition. At shared phase boundaries fix either equivalent description.

For each of the four phases and each unconditional family, organize these equations into a fixed number of length-\(h\) lists, padding with zero equations. Every operand map from list rows to an original logical array has bounded multiplicity: this follows from bounded fan-out for internal feeds, separate designated copies, and partial permutations for adjacency and same-position copies. An operand map of multiplicity at most \(B\) splits into \(B\) partial injections by coloring its preimages separately at each target. Each partial injection extends to a permutation of \([h]\), by any bijection between the unused domain and range. Separate logical array types and intersect the finitely many operand-color and active-row cases. Because arity and \(B\) are constants, this causes only a constant number of cases. Expand the representing polynomials into monomials. Each row list is now a sum of a fixed number of bounded-length monomials, whose factors are permuted logical arrays or public coefficient and mask arrays. Empty monomials represent constant terms. Counting coefficient factors in the length still gives a fixed bound on the degree.

Routing arbitrary permutations. For completeness a permutation of \(2^\ell\) locations has a binary switch realization with \(2\ell-1\) layers, each layer switching pairs along one fixed XOR bit, with a public Boolean mask constant on each pair. This is the binary specialization of the Beneš rearrangeability construction (Beneš 1964, Lemma 3 and Theorems 2–3). Pair sources along the top bit and do the same for targets. The prescribed item routes form a bipartite multigraph on these pairs with degree two at every vertex. Every component is an even cycle, including a pair of parallel edges; alternate its edges with two colors. An initial top-bit switch and a final top-bit switch route each item through the half corresponding to its color. Each half now has a permutation of \(2^{\ell-1}\) items. Recurse with the same layer schedule in the two halves. The base case \(\ell=1\) has one layer and \(\ell=0\) none; the recurrence for depth is \(L(\ell)=L(\ell-1)+2\). Cycle coloring and recursive routing take polynomial time in \(h\).

Introduce a variable factor type for every routed intermediate, and for each layer introduce the XOR-pulled counterpart \(D^*\) of its input \(D\). The layer output \(D'\) satisfies the row equation \[ D'-D-m_{\mathrm{sw}}(D^*-D)=0. \tag{55}\] The mask is pair-constant, so this is exactly either the identity or a transposition on each pair. The counterpart identity itself is checked by a scalar program below. These equations are always imposed, including in inactive phases. Induction through the network makes each variable factor a known permutation of an original logical array, for arbitrary field values of that array. There are only \(O(r)\) layers among a fixed number of routing networks, hence \(\mathop{\mathrm{poly}}(r)\) factor and equation types with bounded arity per row. For an edit of an original logical array at \(j\), every factor derived from it changes only at the image of \(j\) under its fixed permutation. All such addresses for one frame occupy \(\mathop{\mathrm{poly}}(r)\) bits. Their entire frame-indexed tables need not have a succinct random-access formula; they will be stored as public encoded tables and focused before use in Section 5.

Primaries and assigned degree. For every factor array \(D\in J^h\), define its unique degree-\(<h\) interpolant on the subgroup grid by \[ F_D(Z)=\sum_{j=0}^{h-1}D_jL_j(Z). \tag{56}\] For each factor-occurrence list of each monomial, include primaries for every subset \(S\) of its occurrences, with payload the length-\(M_o\) coefficient table, padded by zeros, of \[ F_S(Z)=\prod_{a\in S}F_{D_a}(Z). \tag{57}\] The index set here consists of occurrences: repeated uses of one factor remain distinct. The empty subset gives \(1\). Identify shared singleton primaries or impose direct full-word equalities on copies, and include independent singletons when needed. The assigned logical degree \(k_S\) counts variable occurrences only; public factors have degree zero. Let \(d_2\) bound the length of every factor-occurrence list after all switch and row equations have been included. It is a fixed constant, and \(k_S\le d_2\). The honest ordinary polynomial degree is at most \(d_2(h-1)\). Choose the earlier size constant so that \[ M_o>(8d_2+8)h. \tag{58}\] All primary formulas exist for arbitrary \(b\in J^{4h}\).

Index independence and support. Scalar primaries are intended to depend only on \(x\), not on \(u\). Test invariance of their payloads under left \((0,a)\) pulls for the fixed generating list of \(H\). Such a pull fixes \(x\) and changes \(u\) to \(au\), and shares B with the original untwisted scalar slot. Compare whole systematic A rows as above, using the pulled local expression without introducing a free encoder witness. The shared-B exact gap forces invariance under each generator; since these generate \(H\), this is precisely independence from \(u\). No independent invariance test is needed on a derived program stage whose exact recipe already determines it, and matrix intermediates need not be \(u\)-independent.

Use range masks from Lemma 19 to require singleton coefficient support in \([0,h)\) and product-primary support in \([0,d_2h+1)\), with sharper public bounds when appropriate. Encode the masked complement as a full output and compare that entire word with zero. A nonzero output has full-code distance. Compare each public singleton and each empty product with its precomputed canonical full encoding. These are structural conditions.

Product certification. Compute the length-\(M_o\) DFT of each relevant primary coefficient table by certified full stages. Its payload at integer \(y\) is the polynomial’s value at \(\zeta^y\). For every nontrivial subset choose one occurrence \(a\in S\) and check, at one fixed systematic payload cell at \(s=t=0\), \[ F_S(\zeta^y) =F_{S\setminus\{a\}}(\zeta^y)F_{D_a}(\zeta^y). \tag{59}\] These are pointwise nonlinear tests; the stored transform stages themselves have linear recipes. Once support, independence and transform identities hold, a false equality is the nonzero polynomial \(F_S-F_{S\setminus\{a\}}F_{D_a}\), of degree less than \((d_2+1)h+1<M_o/2\). A nonzero polynomial of degree \(D\) over a field has at most \(D\) roots, as follows by successively dividing by \(Z-z\) at distinct roots. Thus the false equality fails at more than half the \(M_o\) distinct points \(\zeta^y\). Uniform \(k\) has uniform \(x\), and independence from \(u\) prevents the extra index from diluting this gap. Induction on subset size forces exactly all products (57) once these tests hold.

Counterparts and the subgroup annihilator. Apply the length-\(h\) Fourier transform to the low \(\ell\) bits of each singleton’s padded coefficient table. Its first block is the value table \(D\), and every higher block is zero by coefficient support. For each XOR counterpart use the certified bit pull on this padded table and compare its full output with the counterpart’s separately computed padded value table. Their full-operation gap forces the exact counterpart identity needed in (55).

For a row-equation list let \(R(Z)\) be the indicated linear combination of its product primaries. Its value at \(\omega^j\) is exactly the row expression at \(j\). Its remainder modulo \(Z^h-1\) has coefficients \[ [Z^i](R\bmod(Z^h-1)) =\sum_{z=0}^{M_o/h-1}[Z^{i+zh}]R, \quad 0\le i<h, \tag{60}\] and zero padding elsewhere. This formula follows from \(Z^{i+zh}\equiv Z^i\pmod{Z^h-1}\), since the coefficient table is supported below \(M_o\). It is a short linear program: apply \(\prod_{i=\ell}^{r-1}(I+R_{(e_i,1)})\) to sum all high-bit blocks, then mask to high bits zero. Require its entire full word to be zero when the equation is imposed.

The polynomial \(Z^h-1\) is exactly the annihilator of the subgroup grid: it has the \(h\) distinct roots \(\omega^j\), because \(h\) is invertible in \(J\), and its degree is \(h\). The remainder has degree below \(h\). Therefore it vanishes as a polynomial if and only if \(R\) vanishes at all grid points. In one direction divisibility suffices; in the other direction a degree-\(<h\) polynomial with \(h\) distinct roots is zero. This proves that the folded full-word checks impose the row equations exactly, without any random sampling loss over rows. All structural switch equations and their folded computations are always present. All phase-specific folded computations are also stored persistently; the repeated clock selects only which final zero conditions are imposed.

Counts and address transforms. The constant coefficient of (56) is \[ [Z^0]F_e=h^{-1}\sum_{j=0}^{h-1}e_j, \tag{61}\] since every \(L_j\) has constant coefficient \(h^{-1}\). Mask the occupation coefficient table to index zero, using all bit masks. Compare its full word with the public full encoding of \(1[\underline x=0]\) times \(c h^{-1}\), where the expected count \(c\in[0,h]\) is computed from the legal repeated stage and phase. This scalar is used in the comparison; it is not part of a changing persistent value. On Boolean occupation data, characteristic \(p>M_o\ge h\) implies that two counts in \([0,h]\) are equal in \(J\) only when they are equal as integers. Together with monotonicity this enforces the prescribed prefix exactly.

For address access, take the padded length-\(h\) value table obtained above and apply the full \(r\)-bit Walsh transform. Its result is (54). Walsh orthogonality gives \[M_o^{-1}\sum_x U_D(x)(-1)^{x\cdot j} =\sum_{i<h}D_i \left(M_o^{-1}\sum_x(-1)^{x\cdot(i+j)}\right) =D_j \qquad(j<h).\] In particular the high bits of the zero-padded value table cause \(U_D\) to repeat across the corresponding high output blocks; they do not introduce an additional normalization factor.

Exact alternatives and complexity. Every stage of every mask, transform, counterpart comparison and remainder computation is stored as a full slot with its specified linear recipe, including mixed and untwisted matrix intermediates. Give a derived stage the maximum assigned degree of its primary ancestors and retain its ancestor subprogram or shared directed acyclic recipe. Public indexed arrays are degree-zero inputs with precomputed encoded constants.

On exact duplicated full codewords, a false independence, support, public-constant, full-operation, counterpart, folded-zero or count identity has a constant gap by the shared-axis or full-code distance. If none is false, the polynomial root argument forces all primary products. Singleton support makes the interpolant unique from its subgroup values. The counterpart and switch equations then determine all factors as their prescribed permutations of the four original logical arrays, and the public factors are fixed. Thus the structural tests force precisely \(P(b)\). The remaining Boolean, prefix, count and selected-phase row equations are exactly the macrovertex rules. If any is false, its folded or count check has the same exact gap. All tests are packed at the center; choosing one false relation in this argument entails no division by their number. The minimum of the fixed code gaps and the product gap gives \(\gamma_{\mathrm{per}}>0\) and proves both alternatives.

There are \(O(r)\) routed factor and row families before the scalar program expansions, a constant number of occurrence subsets per monomial, and polynomially many stages per transform. Thus the number of full slots, recipes and local metadata is \(\mathop{\mathrm{poly}}(r)\). The entry dimension and field bit length give a further fixed polynomial factor. At one center the checker scans these lists, performs field operations and evaluates fixed-length control decisions, all in \(\mathop{\mathrm{poly}}(r)\) bit operations. It reads public encoded constants only at the publicly specified positions in \(\Pi(k)\); arbitrary hidden-frame table lookup is never assumed. All public permutations, masks, coefficients, encodings and complete canonical arrays are constructible globally by polynomial-time combinatorial and linear-algebra algorithms. Since \(|\Gamma|=M_o|H|=O(N\operatorname{polylog} N)\) and every scalarized encoding system has polynomial dimension in \(N\), this takes \(\mathop{\mathrm{poly}}(N)\) time. The persistent word length is \(O(N\operatorname{polylog} N)\) field-bit storage, with a fixed exponent in the polylogarithmic factor. This completes the construction and proof. ◻

Proof. For a primary use (62). If \(D\) is another persistent stage with linear payload recipe \(\mathcal L_D\), apply \(\mathcal L_D\) to the corresponding primary increments, replacing degree-zero primary increments by zero. At this fixed frame its coefficients, pulls, and encoder types are fixed. Hence \[\mathcal L_D\bigl((F_S(b+h_\sigma(c)))_S\bigr) -\mathcal L_D\bigl((F_S(b))_S\bigr) =\mathcal L_D\bigl((\Delta_\sigma F_S(b))_S\bigr).\] The operations used in Section 4 implement this identity at the payload level. In particular, multiplying a scalar slot by the public matrix \(\rho_e(k)\) is linear in that scalar; changing one encoder axis or contracting matrix entries is also linear. These operations introduce no additional logical degree.

Allocate full slots for every stage of each increment program, with new slots for its mixed and untwisted verification stages. An identity or zero stage may be inserted to give an output its required type. Order stages topologically, so that Lemma 21 can initialize one full target using already completed parents. For every newly allocated stage, record the ancestor directed acyclic graph that expresses its payload in the persistent primaries. Its roots have degrees at most one less than those of the target whose increment is being computed. If its assigned degree is positive, apply the same construction to this new stage for every edit. This includes a stage introduced solely for verification: it will be retained at full preparation and therefore needs its own increment.

Inlining here means substitution in a directed acyclic graph, with sharing retained within each target computation. If a primary is used many times, substitute its increment program once and fan out its result. Separate target computations may use fresh copies. Along any chain of newly generated targets the assigned degree drops by at least one. Therefore the construction stops after at most \(d_2\) derivative tiers. At each tier the number of target graphs, their sizes, their ancestor descriptions, and their substitutions are bounded by a fixed polynomial in the preceding total description size and \(r\). A fixed number of such polynomial expansions remains polynomial in \(r\).

The programs verify the computed increments by their own stage relations, starting from the lower-degree primaries. They do not test a finite-difference assertion about an otherwise unspecified witness. Neither their construction nor their identities use the final validity equations. This also ensures that increment recipes remain defined on field data produced by an edit that is not a legal macrograph move. ◻

Proof. Concatenate the public focus, all full-target filling schedules, and the critical-read focuses. The stage lists for selectors and cutoffs have fixed padded lengths independent of their address values. The per-target mode schedule consists of \(M_o\) iterations of fixed polylogarithmic sublength, together with its initial and final buffer steps. The exceptional first iteration and final erasure are specified separately. Thus a binary microclock can be interpreted by scanning the polynomial-in-\(r\) list of program boundaries and performing arithmetic on \(O(\log M_o+\log\operatorname{poly}(r))\) bits. The interpreter selects the current iteration, buffer, initialized prefix, and transition; it does not execute all preceding iterations. Distinct programs may use distinct scratch indices to keep their shapes and twists fixed. An idle preparation step supplies \(J_{\max}\geq1\) if needed.

For the last assertion, write \(D_\sigma(b)\) for the stored full increment of a positive-degree full slot \(D\). At the top perform, simultaneously, \[ D(b)\longmapsto D(b)+D_\sigma(b) =D(b+h_\sigma(c)) \tag{64}\] for every persistent and transient full computation slot. Equation (64) is valid in its own encoder because that encoder is linear. The increment slots themselves are included in this update whenever their assigned degree is positive; their required increments exist by Lemma 23. Degree-zero slots do not change. All additions read the old tuple before writing the new one.

The full-target temporary buffers are already empty. Public focus depends only on \(c\) and remains fixed. Each main critical-read stack is a linear selector-and-pull program at fixed public addresses. Adding the matching focused increment stack therefore updates all its initialized stages to their new canonical values. Those increment stacks have degree zero and stay fixed. This verifies the assertion also for the retained A-only data. The preparation can now be erased in the reverse order, using exactly the same recipes on the new \(b\) and unchanged frame. ◻

Proof. Put \(\theta=\operatorname{rej}(W)\). The parsing, repetition, and full-code proximity conclusions of Theorem 16 first change \(O(\theta)\) centers to give legal constant clock data and exact full codewords. A corrected repeated clock of illegal range would cause rejection everywhere, so small enough \(\theta\) rules it out. Exact one-axis distance then forces systematic-payload duplication in every full slot. Otherwise that one failed duplication relation already has a fixed positive rejection probability. Zeroing locally A-invalid scratch parts costs another \(O(\theta)\) centers. A change on \(z\) centers changes any simultaneous test on at most \(qz\) centers; this estimate uses the common permutation list and does not depend on the number of slots.

We next restore all scratch relative to these corrected full codewords and the corrected clock, before using any advertised full-operation identity. The reference for the public focus is the actual hardwired public word at the corrected frame. Treat its recurrences first. A later table-dependent recurrence is active only when this reference focus is complete and hence gives identical correct coefficients at every center. Each initial expression \(X\) in a mode-fill program is A-coded from its exact full parents, even if those parents do not yet satisfy their advertised payload recipes. The critical and increment focuses also start from exact A-coded full words. Thus every required reference prefix is exactly A-coded.

These are precisely the reference and ordering hypotheses of Lemma 20. The preprocessing above changed only \(O(\theta)\) sites, so the common query list bounds both the joint A-conflict fraction and the simultaneous recurrence-failure fraction of this one preprocessed word by \(O(\theta)\). Apply the lemma to its entire scratch tuple, including inactive zeros. Its fixed-word induction keeps every prefix estimate \(O(\theta)\) and makes only one final replacement. All scratch is therefore restored at cost \(O(\theta)\), independently of the number of stages. No full-operation identity has been used to obtain this conclusion.

Call the resulting tuple \(\widetilde W\). Its remaining tests still fail with probability at most \(C'\theta\) for a fixed \(C'\). By Lemma 22, either its persistent tuple is exactly \(P(b)\) for logical bits \(b\) valid at the selected macro stage, or a persistent relation fails with fixed positive probability. Choose \(\theta\) below that gap divided by \(C'\) to obtain the former alternative. Now follow the initialization order of the transient full targets. Completed targets with canonical parents are forced to their exact outputs by the shared-axis gap following Definition 18. For the current partial target, its required cutoff comparison has the same gap by Lemma 21. The cutoff scratch has already been restored: its completed value is precisely \(P_{t'}X\). In the case that the target shares only the B axis with \(X\), orbit invariance makes this completed reference B-coded. Only at this point is B-axis distance applied. No intermediate A-only scratch is assumed to be B-valid. Inactive full targets are forced to zero by full-word distance.

There are only finitely many kinds of these gaps, uniformly in their stage indices, program lengths, and vector dimensions. Their minimum is positive. If any relation failed exactly on \(\widetilde W\), it alone would give at least that gap in the packed test. Decrease \(\theta\) once more to rule out every such failure. All full slots and restored scratch then have the unique canonical values of \((c,b,\eta,j)\). The total restoration cost is \(C_{\rm rep}\theta\) for a fixed \(C_{\rm rep}\).

Canonical snapshots satisfy every test by their construction, proving perfect completeness. If a neighborhood avoids the disagreement set between \(W\) and \(R_v\), its test accepts; a union bound over \(\Pi\) proves the converse. Finally, two labels with different repeated data differ at every center. If only their logical arrays differ, one logical singleton interpolant differs. Its full encoded difference is nonzero and has the fixed distance of Theorem 16, including the constant conversion between four-part and whole-symbol metrics. This gives \(\delta_{\rm raw}>0\). ◻

Proof. The graph and local evolution were established in Lemma 24 and (67). The tester and distance are Lemma 25. For example, its constants allow \[\theta_\alpha= \min\{g_{\rm rep}/2,\alpha/(2C_{\rm rep})\}.\] All local proposals use the same primitive permutation list as the tester, enlarging it by a fixed number of maps if necessary.

For the correction claim, let \(d\) and \(\delta_1\) be the outer A-code degree and distance. Choose \(\rho_{\rm raw}\) smaller than both \(\delta_{\rm raw}/3\) and \(\delta_1/4\), and smaller than the fixed uncertainty radius in Lemma 17. An admissible choice of \(U^+\) is the set of centers having at least \((\delta_1/2)d\) neighbors in \(U\) in a forward or inverse A list. Off this set all row suggestions have fewer than half the local minimum distance in errors, so the joint decoder recovers the reference exactly; the clock majority and padding agree there too. If \(u=|U|/|\Gamma|\), the spectral estimate from that lemma gives \[\frac{|U^+|}{|\Gamma|} \leq\frac{2\lambda^2u}{(\delta_1/2-u)^2} \leq\frac u2.\] Neither this support nor the proof refers to the values inside \(U\). For a requested-center cone with consistent repeated positions, extend its initially supplied values arbitrarily to the whole word, setting the reference outside \(U\). The same support argument applies. This proves the assertion even when separate cones choose different extensions.

After \(O(\log|\Gamma|)\) synchronous global rounds the uncertainty set has cardinality less than one, giving exact recovery in polynomial time. From a recovered logical singleton slot, read its coefficient payload and evaluate the degree-\(<h\) interpolant at \(\omega^j\), \(0\leq j<h\), to obtain the corresponding logical bits. The repeated clock gives \((c,\eta,j)\). The distance choice makes the promised reference unique. On inputs outside the recovery promise the algorithm has a total default; it may check the decoded label and its canonical word by the global polynomial-time algorithms. Finally, (69)–(73) and (74) give all asserted cost and parameter-order statements. ◻

Proof. Choose \(a_2<\nu_B\) and then \(a_1\) so small that \(C_Ba_1<\theta_B(a_2)/4\). Estimate port-tester rejection by a fixed number of independent trials and compare to \(\theta_B(a_2)/2\). Bounded independent variables give any fixed confidence by increasing the fixed sample count. In the interval between the two promises either Boolean result is permitted. An unflagged block on the good event is within \(a_2\) of an encoding, unique because \(a_2<d_B/4\); take its logical string as the intended input. A flagged input is explicitly a public zero, so it requires no external near-port premise. A union bound is applied to the finite list of completed flag promises, after that list has been fixed. Their internal tester answer trees are not counted as new logical promises. ◻

Proof. Choose \(\rho_{\rm acc}\) small enough that \(\rho_{\rm acc}/a_1\) is within the raw uncertainty-correction radius. Choose \(\alpha<\rho_{\rm acc}/4\) and take the raw gap \(0<\theta_\alpha\leq1\) from Theorem 26. Writing \(q=|\Pi|\) for its bounded checker-neighborhood size, choose \(0<a<a_1\) and \(b_0>0\) satisfying \[ \alpha+a+b_0<\rho_{\rm acc},\qquad qb_0<\theta_\alpha/16, \qquad p_{\max}=b_0\theta_B(a)>0. \tag{79}\] Decrease \(p_{\max}\) if necessary. Let \(p\) be the average port-tester rejection over all sites. Estimate \(p\), and independently simulate the raw checker at sampled centers using the flagged/substituted inputs. Accept when the first estimate is at most \(p_{\max}/2\) and the simulated raw rejection estimate is at most \(\theta_\alpha/2\).

On statistics of error less than \(p_{\max}/4\), acceptance gives \(p<p_{\max}\). Consequently the fraction of sites not within \(a\) of any port encoding is less than \(b_0\). At a center whose entire neighborhood avoids these sites, good flag promises leave all inputs unflagged and make the simulated checker exactly the checker on the global word \(s^*\). Exceptional centers occupy at most \(qb_0\). In the analysis, also estimate the true checker result on \(s^*\) to accuracy \(\theta_\alpha/8\) and the exceptional-center fraction to accuracy \(\theta_\alpha/16\). These are fixed bounded statistics; the algorithm need not compute the hypothetical true statistic. On their good events and the completed flags’ good events, \[\Pr[\text{raw checker rejects }s^*] \leq\theta_\alpha/2+\theta_\alpha/8+qb_0+\theta_\alpha/16 <\theta_\alpha.\] Raw soundness makes \(s^*\) \(\alpha\)-close to a valid \(R_w\). Charging all raw-disagreement sites and all non-\(a\)-close sites at cost one yields \[\mathop{\mathrm{dist}}(y,E_w)<\alpha+a+b_0<\rho_{\rm acc}.\] The uniqueness radius makes this reference independent of subsequent random acceptance decisions for the fixed \(y\).

Conversely, if \(\mathop{\mathrm{dist}}(y,E_w)<\rho_{\rm comp}\), then \(p\leq C_B\rho_{\rm comp}\). By Markov’s inequality at most \(\rho_{\rm comp}/a\) of the ports are at distance at least \(a\) from their true block. Outside their \(\Pi\)-neighborhoods the simulated checker is the perfectly accepting raw checker. Choose \(\rho_{\rm comp}\) so small that both means are strictly below one quarter of their acceptance thresholds; choose the sampling errors with the remaining slack. Flag error probabilities are set after the sample counts. This proves both assertions. The proof requires concentration of the sampled exceptional fraction when \(p\) is small. It never requires an arbitrarily long batch to avoid every exceptional site. ◻

Proof. Fix a rounded seed that can be accepted on good validation, and its unique reference \(R_w=(s_k)\). Put \[U_0=\{k:\mathop{\mathrm{dist}}(y_k,\mathcal D(s_k))>a_1\}, \qquad |U_0|/|\Gamma|\leq\rho_{\rm acc}/a_1.\] Outside \(U_0\), good flags unflag the port and its unique nearest logical string is \(s_k\). Within \(U_0\), substitution and intermediate flag choices may supply arbitrary values. In each deduplicated cone extend those initial values to a whole raw word agreeing with \(R_w\) outside \(U_0\). The raw uncertainty theorem gives a residual set \(U_t\), depending only on \(U_0\), with arbitrarily small fixed density after sufficiently many fixed rounds \(t\). Its guarantee holds simultaneously for every such extension. Thus different cones and correlated intermediate flags cause no additional exceptional support. A corrected symbol is right off \(U_t\); a local proposal and edge flag are right off a fixed permutation expansion of \(U_t\).

Compute an edge flag at a uniform-marginal center. For a requested own or neighboring encoding bit, compute the appropriate raw output symbol and then the requested coordinate polynomial of \(\mathcal D\). Matching coordinates are uniform in the output average; the statistical requests have the same center marginal. Each fixed permutation expansion therefore costs at most its size times \(|U_t|/|\Gamma|\). Set \(t\) for the already fixed list of high-level true roles and calls. No union over all possible intermediate flag patterns is necessary.

The raw simulation uses at most \(C_tL^{c_{\rm raw}}\) Boolean gates, with exponent independent of \(t\). A degree-at-most-ten Boolean polynomial has at most \(\sum_{j=0}^{10}\binom Lj=O((L+1)^{10})\) monomials. Compute each monomial by a bounded-fanin AND tree and their sum by XOR gates expanded in the fixed basis. Coefficients and the requested bit’s description are publicly generated. The extra bit-index and padding work has a fixed polynomial exponent. Our initial choice of \(c_{\rm allow}\) leaves slack for this work. The number of raw ports and the multiplicative factor may increase with \(t\), but are now fixed. The port encoding and its radius do not change. ◻

Proof. Write an output coordinate as \((b,k_0,z_0)\) with \(b\in[4]\), \(k_0\in\Gamma\), and \(z_0\in[S_0]\). Use fixed-length labeled walks in the outer Cayley expander starting at \(k_0\). Fresh bounded segments and auxiliary uniform positions in \([S_0]\) supply all center and word statistics. Averaging over uniform \(k_0\) makes every walk position stationary. If the mean-zero operator norm is at most \(\lambda<1\), bounded centered functions at times \(s,t\) have covariance at most \(C\lambda^{|s-t|}\). Independent auxiliary randomness only changes the bounded diagonal terms and replaces off-diagonal functions by their conditional means. Therefore a batch of \(q_s\) samples satisfies \[\operatorname{Var}\left(\frac1{q_s}\sum_{j=1}^{q_s} Z_j\right) \leq\frac{C}{q_s^2}\sum_{s,t=1}^{q_s}\lambda^{|s-t|} \leq\frac{C(1+\lambda)}{(1-\lambda)q_s}.\] Chebyshev’s inequality and a finite union give any fixed confidence by choosing a sufficiently large fixed \(q_s\). The argument permits distinct bounded functions at the different slots and separate batches for physical blocks.

Apply it to port rejection, the fixed global raw-checker and exceptional indicators in validation, and each actual reference candidate’s statistics in the geometric procedure. At fixed rounded seeds those reference vertices are fixed whenever good acceptance is possible. Analyze all their roles before a numerical minimum or uncertain acceptance chooses which ones to use. The concentration is not conditioned on the realized answer path. Each walk has a fixed number of fixed-degree label choices. Each remaining choice has polynomial-in- \(L\) support, and only a fixed number of choices is used. Their joint support per output coordinate is consequently polynomial in \(L\). ◻

Proof. Let \(Q(L)\) bound the enumerable rational support of every tape law. For a common square \(T\geq Q(L)S_0/\eta_0\), round each mass \(Tp_j\) down to an integer and distribute the remaining copies among nonzero support entries. Each mass error is at most \(1/T\), and total variation is at most \(Q(L)/T\leq\eta_0/S_0\). Floors, remainders and the ordering of entries are computed with exact rational arithmetic in polynomial time. The probability descriptions have polynomial bit complexity. A function in \([0,A]\) changes expectation by at most \(A\) times total variation, proving the bounded-statistic assertions.

For the load assertion, explicitly list all potential direct slots \(\mathcal A\), including their fixed earlier-answer paths; set \(H=|\mathcal A|\). If a slot is omitted or supplied a public value, its read subdistribution is dominated by that of its potential slot; it is never renormalized on being selected. Fix a target \((b',k',z')\) and a possible \(\pi\in\mathcal P\). Its preimage \(k_0=\pi^{-1}(k')\) is fixed. For every fixed offset, the true law gives \[ \sum_{z_0=1}^{S_0} \mathbb{E}[\text{number of direct reads at }(b',k',z')] \leq C, \tag{82}\] where \(C\) is the sum of the unconditioned fixed-slot density constants. Matching coordinates contribute one, uniform sampled coordinates contribute their bounded counts, and tester queries contribute their smoothness constants. Branches and seed roles add only a fixed factor. A position-count random variable lies in \([0,H]\). Changing the law for one output by total variation \(\eta_0/S_0\) adds at most \(H\eta_0/S_0\) to its expectation; summing over \(z_0\) adds only \(H\eta_0\). Sum the fixed preimages and physical roles and multiply by \(T_{\rm tap}\). This is the asserted \(O(T_{\rm tap})\) load. A constant total-variation tolerance without the \(S_0\) denominator would not give this bound. ◻

Proof. Fix a physical block and a raw site \(k'\). For each of the fixed possible address permutations, a functional port requesting \(k'\) has a fixed \(k_0\) preimage. There are \(S_0\) output bit positions and \(T_{\rm tap}\) tapes at that preimage, and only a bounded number of invocation/port roles. Thus at most \(C S_0T_{\rm tap}\) invocation ports request \(k'\). By (76), any position in that site is used at most \[ C S_0T_{\rm tap}\,\frac{C_{\rm occ}G_0}{S_0} \leq C' T_{\rm tap}K_c=C'R \tag{85}\] times. Lemma 32, followed by replication over the cohort, gives \(O(T_{\rm tap}K_c)=O(R)\) direct comparison occurrences at each base coordinate. Enumerate all these occurrences and assign successive ones round robin to its \(R\) physical replicas. Each actual replica has bounded resulting multiplicity. Each comparison is performed in its own gate cone directly on that replica’s \(x\) value. In particular, an error in one comparison wire is not broadcast to other inner cones. ◻

Proof. All hidden nodes, including \(p,n\), remain in \([0,1]\) even when their logical values are wrong. Satisfied final Scale gates therefore make each signed term at most \(t_\beta+\varepsilon\). The absolute change from the computed average is at most their sum plus the final arithmetic errors. The averaging chain is within \(C\varepsilon\) of its exact average. Returning to physical units gives (88), after enlarging \(C_{\rm ar}\). For the fine bound, induction through the shielded Boolean selections supplies the correct digits in (87). Scale is nonexpansive and clipped Add and Subtract are Lipschitz with respect to the sum of their input errors. For an explicit bound, let \(J_d\) be the number of dyadic digits in one magnitude. A magnitude uses \(J_d\) Scale and \(J_d-1\) Add gates; its error is at most \((3J_d-1)\varepsilon\). The sixteen Scale and fifteen Add gates for the average contribute at most \(31\varepsilon\). The two final Scale gates and the final Add/Subtract pair therefore contribute a total error at most \((6J_d+33)\varepsilon\) in node units, or \((18J_d+99)\varepsilon\) in physical units. An optional final Copy adds \(3\varepsilon\). The coarse bound’s arithmetic error is at most \(108\varepsilon\) including that Copy. Thus \(C_{\rm ar}=18J_d+108\) suffices for this implementation, uniformly in all Scale parameters in \([0,1]\). The exclusive-sign identity gives (89). ◻

Proof. Disjointness of direct gate sets proves (i). The number of invocations violating the threshold in (ii) is at most \(\delta|T|/(\delta_gG_0)\). Charging \(K_c\) outputs for each and using (83) and (90) proves (ii), even if the same cohort is charged repeatedly. For (iii), Markov’s inequality gives at most \(mR\lVert X-\bar X\rVert_{\rm rep}^2/\omega^2\) excessive physical replicas. Lemma 33 bounds their total comparison multiplicity by a constant. The normalization \(K_{\rm out}=4mR\) only improves the bound.

For (iv), fix a port of an invocation at site \(k\) and threshold \(\xi\). Equation (76) bounds its ambiguous occurrences by \[C_{\rm occ}G_0\, \frac{\#\{z:|\bar X_{kz}-\xi|\leq4\omega\}}{S_0}.\] Every site is an image of a uniform \(k_0\) under a member of the fixed permutation list. Sum over that list and all invocation ports under the unconditioned tape law, before selecting any answer branch. Averaging the offset and using (91) bounds the expected number per trial by \(C G_0(D_{\rm grid}^{-1}+\omega)\). The full occurrence bound is uniform in threshold-dependent function data. Tape rationalization changes a count bounded by \(CG_0\) by at most \(CG_0\eta_0/S_0\). Dividing each trial’s charge by its \(K_c\) output replicas gives (iv). Direct slots use the full-tree density argument in (82), and the same grid count; their count per trial is bounded by \(H_{\rm out}\). This reasoning applies to every fixed eventual mean, rather than a mean selected before construction. Finally, (v) is the same threshold counting proof as (ii), with spoiled occurrences replacing failed gates. ◻

Proof. Apply (88) to nonfailed direct cones. At failed ones, both \(X_{ir}\) and \((A_{\rm rep}X)_{ir}\) belong to \([-1,2]\), so their difference is at most three. The factor four in the norm and Lemma 35(i) give \[\lVert X-A_{\rm rep}X\rVert_{\rm rep} \leq4\beta B_1+2C_{\rm ar}\varepsilon +6\sqrt{C_{\rm tot}\delta}.\] On the other hand (86) and the reverse triangle inequality give \(\kappa\lVert X-\bar X\rVert_{\rm rep} \leq\lVert X-A_{\rm rep}X\rVert_{\rm rep}\). Equation (94) proves the assertion. In particular, failures at physical feedback outputs, threshold constants, or the numeric averaging gates are already included; no decision is trusted in establishing this estimate. ◻

Proof. Fix the actual mean \(\bar X\) in all ideal tape experiments. Coarse synchronization permits all spoilage charges already budgeted. Discard cohorts with a high-failure or high-spoil invocation. In every remaining invocation whose ideal branch-pattern inputs are all near ports or public substitutions, Theorem 27 applies. Mark all cohort outputs receiving an incorrect designated wire from any such invocation. Equations (75) and (84) bound their union by \(2B_{\rm out}\upsilon\) of the outputs. Do this marking for every near-input hypothetical invocation before following the selected path. Non-near-input invocations are irrelevant unless selected; on the ideal good-port event a selected invocation necessarily is a near-input one.

Outside these marks and the other unstable events, every direct comparison in the complete tree has the needed margin and every selected invocation supplies its correct near-bit. Induct on the ideal answer sequence: earlier reliable bits select its actual substitution/function branch, the selected gadget is reliable, and Boolean shielding removes arbitrary unused outputs. Thus the whole selected direct computation equals its ideal Boolean run, and (89) holds.

For an unstable but entirely satisfied direct cone, use only (88) and \(|v_i(\bar X)|\leq B_1\): its discrepancy from the clipped true-field update is at most \(3\beta B_1+C_{\rm ar}\varepsilon\). This is proportional to \(\beta\) apart from numeric error. Failed direct cones use only the range bound three. The empirical ideal error, clipping nonexpansiveness, and the total unstable fraction at most \(q_0\) therefore give \[E_{\rm res} \leq\beta\bigl(c_*\kappa/20+6B_1\sqrt{q_0}\bigr) +2C_{\rm ar}\varepsilon+6\sqrt{C_{\rm tot}\delta} <\beta c_*\kappa/2\] by (92) and (95). This includes arbitrary concentration on extraction gates: above-budget invocations lose their whole cohort; below-budget invocations lose their guaranteed fraction of designated wires, and the lower bound in (75) prevents a concentration factor. ◻

Proof. Write \(Q=I-J\) and \(g=\mathop{\mathrm{clip}}_{\mathcal B}(JX+c)\), a repeated vector. The mean projection minimizes distance to repeated vectors, and coordinate clipping is nonexpansive. Hence \[\lVert QF\rVert_{\rm rep} \leq\lVert F-g\rVert_{\rm rep} \leq\lVert A(X-JX)\rVert_{\rm rep} \leq(1-\kappa)\lVert QX\rVert_{\rm rep}.\] Projecting \(X-F\) gives \(\lVert QX\rVert_{\rm rep}\leq E+(1-\kappa)\lVert QX\rVert_{\rm rep}\), which proves the first inequality. Taking means and then comparing to \(g\) gives \[\lVert JX-g\rVert_{\rm b} \leq\lVert J(X-F)\rVert_{\rm rep}+\lVert JF-g\rVert_{\rm rep} \leq E+(1-\kappa)\lVert QX\rVert_{\rm rep}\leq E/\kappa.\] This argument does not exchange averaging and clipping. ◻

Proof. Construct a continuous self-map of \([0,1]^V\). At an arithmetic gate’s unique output use its exact numerical operation. At a Less gate with inputs \(a,b\), use the clipped linear ramp that is zero when \(x_b-x_a\leq-\varepsilon/2\) and one when \(x_b-x_a\geq\varepsilon/2\). For Boolean gates define a continuous signal \(h:[0,1]\to[0,1]\) equal to zero on \([0,2\varepsilon]\), equal to one on \([1-2\varepsilon,1]\), and linear between them. Use respectively \[\max\{h(x_a),h(x_b)\},\qquad \min\{h(x_a),h(x_b)\},\qquad 1-h(x_a)\] for Or, And, and Not. Set coordinates not produced by gates to zero. Unique output ownership makes these prescriptions a well-defined continuous cube map. Brouwer’s fixed-point theorem (Brouwer 1911) gives a fixed point \(x^*\); no efficient computation of it is asserted.

Round every coordinate to the nearest point of \(\{0,1/q,\ldots,1\}\), obtaining \(\widetilde x\) with \(|\widetilde x_v-x_v^*|\leq1/(2q)\leq\varepsilon/40\). Constant errors are at most \(\varepsilon/40\), Scale and Copy errors at most \(2\varepsilon/40\), and Add and Subtract errors at most \(3\varepsilon/40\), using parameter bounds and nonexpansive clipping. For a triggered strict Less antecedent after rounding, its signed input gap before rounding has the same sign and magnitude strictly greater than \(\varepsilon-2\varepsilon/40>\varepsilon/2\). Its fixed-point output is therefore the required endpoint zero or one, which rounding preserves.

If a weak Boolean low antecedent \(\widetilde x_a\leq\varepsilon\) holds, then \(x_a^*\leq\varepsilon+\varepsilon/40<2\varepsilon\), so \(h(x_a^*)=0\). Similarly \(\widetilde x_a\geq1-\varepsilon\) implies \(h(x_a^*)=1\). Every applicable Or, And, or Not conclusion follows from its displayed exact formula, including equality at the weak threshold. The corresponding fixed-point output is zero or one and is unchanged by rounding. This verifies every gate implication.

The denominator \(q\) is a fixed integer depending only on \(\varepsilon\). There are at most a fixed multiple of \(M+1\) explicitly listed nodes in a length-\(M\) input, and each output rational has a fixed bit bound. Accounting also for order, indices if used, and delimiters, a sufficiently large fixed integer \(C\) makes \(p(M)=C(M+1)^2\) an upper bound for the entire assignment. This polynomial has nonnegative integer coefficients and is independent of the particular circuit and its parameter denominators. ◻

Proof of Theorem 3. The preceding argument uses Theorem 27, whose construction is proved in Sections 7–9, and Lemma 80, proved in Section 10. Use the fixed rational \(\varepsilon,\delta\) chosen in (93)–(95) and the polynomial \(p\) from Lemma 39. That lemma proves totality, with all gates satisfied. The explicit construction and (98) give the claimed complete quasilinear encoding bound and a deterministic polynomial-time reduction. Equations (97) and (80), followed by the global endpoint decoder, give the required solution from every acceptable assignment, with the stated polynomial running time. Every constant and algorithm has been fixed independently of the input. This proves all four assertions. ◻

Proof. Impose bitness on all logical coordinates, and \[ e_z e_{z'}=0\quad(z\ne z'),\qquad \sum_{z\in C}e_z=1. \tag{103}\] For each stage \(c\), multiply all its work requirements by \(e_{c^{-1}}\). Gate equations have degree at most two before this multiplication, so the resulting degree is at most three. A copy requirement at an occupied position is specifically \[ e_{c^{-1}}w_{i,j}-e_{c^{-1}}s_i[j]=0. \tag{104}\] The requirements are vacuous at unselected stages. At the one selected stage, the prefix equations determine all assigned work positions in topological order and force every other position to zero. This proves the characterization and the dependency assertion.

For start frame \(c\), list \(k\) work write slots and the two legacy slots \(c^{-1},(\gamma c)^{-1}\). During a gate step only the first work slot is active; use a zero unit vector for every inactive slot. Write \(v_1(c),\ldots,v_{k+2}(c)\) for these public vectors in the logical tape space, and for \(\sigma\in\{0,1\}^{k+2}\) put \[ h_\sigma(c)=\sum_{r=1}^{k+2}\sigma_r v_r(c). \tag{105}\] At a valid pre tape, choose a work coefficient to be the old bit plus its required new assignment; choose both legacy coefficients to be one. The required assignment is a read input, a degree-at-most-two gate of earlier work bits, or the unchanged value for an inactive slot. At a valid post tape, the inverse clears precisely the newly assigned positions and flips the same legacy positions. Earlier operands have not changed, so the two operations are reciprocal. There is a bounded list of old-value, operand, and input reads for fixed \(k\). Public phase, gate, activity, and wrap bits select their roles. Define the same coefficient rules on arbitrary Boolean read answers; at the disabled wrap use an idle work proposal. This gives a finite branch system without any assumption that those arbitrary answers describe a valid tape. ◻

Proof. Replace the unique macro tape at stage \(x\) by its post labels in frame \(\gamma^{-1}x\), in decreasing order of \(t\), followed by its pre labels in frame \(x\), in increasing order of \(t\). The frame-advance edge joins the two halves. Each enabled macro edit joins the full pre end of one such segment to the full post start of the next. The only absent join is the wrap join from the final stage to stage zero. This gives exactly the stated path and endpoints. Every segment has more than one vertex, so there are no isolated vertices; each edge changes a label component, so there are no self edges. The final work assignment and all its ancestors have been completed at the last stage, proving the output claim. ◻

Proof. Modulo \(M\) we have \(q^b=h^{vb}\) and \(h^\ell=1\), hence \[\widetilde j\equiv \sum_b j_{vb\bmod\ell}h^{vb\bmod\ell}=j\pmod M.\] The two monomials therefore agree on \(C\), where the powers \(1,Z,\ldots,Z^{M-1}\) form the usual interpolation basis. Each map \(Z\mapsto Z^{q^b}\) is linear over \(\mathbb F_q\), so the coordinate degree of the lifted monomial is at most \(\sum_t j_t\le\ell(h-1)\).

Multiplication of \(\widetilde j\) by \(q\) modulo \(q^\ell-1\) cyclically rotates its base-\(q\) digits. Under (108), this is the permutation \(j\mapsto qj\bmod M\). The digit list all of whose entries equal \(h-1\) is excluded by \(j<M\); exponent zero is consequently the unique representative of residue zero on \(C\). If the original interpolant is \(\sum_j a_jZ^j\) and its values belong to \(\mathbb F_q\), uniqueness of interpolation on \(C\) gives \[a_{qj\bmod M}=a_j^q.\] The digit rotation then proves that its lift \(F\) satisfies \(F(z)^q=F(z)\) for every \(z\in K^\times\). At zero, \(F(0)=a_0\) and \(a_0^q=a_0\), so the same assertion holds.

The coordinate degree is below \(q\) after our cutoff. Conjugating the coordinate coefficients by the \(q\)-power map leaves the values on \(\mathbb F_q^\ell\) unchanged. Uniqueness of interpolation with individual degrees below \(q\) forces each coefficient to be fixed by that conjugation, and thus to lie in \(\mathbb F_q\). Finally \(x^{\widetilde j}=x^j\) for \(x\in C\), which proves the scaling assertion on every basis monomial. These arguments apply coefficientwise in any additional independent variables. ◻

Proof. We give the construction, uniqueness, degree, and probe arguments.

Why arbitrary scaling factors preserve the linear condition. In a rotating call substitute \(RZ\) for the designated variable of a primary and denote the resulting chart by \(f_R\). An unchanged primary stays unchanged. We first show that legal input arrays satisfy \(\mathcal S\) for every \(R\in K\), rather than only for \(R\in C\). Extend scalars in the evaluation space and its linear subspace \(\mathcal S\) from \(\mathbb F_q\) to \(K\). Since \(|C|=M\) is odd, it is invertible in characteristic two. The character projections \[\Pi_j=\frac1M\sum_{x\in C}x^{-j}\rho(x) \qquad(0\le j<M)\] for the simultaneous scaling action \(\rho\) decompose the space and preserve every invariant subspace. On the imposed lift shape, the character \(j\) is represented by the single exponent \(\widetilde j\) in every rotating primary. Nonrotating components occur in character zero. Substitution by \(R\ne0\) therefore acts by the scalar \(R^{\widetilde j}\) on each character space, and preserves the extended subspace. At \(R=0\) it projects onto character zero, which also preserves the subspace. Scaled evaluations of our \(\mathbb F_q\)-valued chart are still \(\mathbb F_q\)-valued; intersecting with the original evaluation space, or using the original defining rows, proves the assertion over \(\mathbb F_q\).

A failed original row fails at \(R=1\), so it remains a nonzero polynomial condition. Tests requiring the substitution sample \(R\) uniformly from \(K^\times\); this changes a uniform density by at most \((1-|K|^{-1})^{-1}\) and keeps primary point marginals uniform. The substitution is bilinear in coordinate variables and at most doubles total degree. In a nonrotating call omit \(R\) everywhere below.

Separate row contributions and partial sums. Pad the row set by zero rows to \(H^\rho\), with \(\rho=O(\ell)\). For one primary block with \(m_0\) native \(q\)-coordinates, put \(m'=vm_0\). An \(H\)-basis of \(\mathbb F_q\) gives a packing map \[w_{\rm pack}:\mathbb F_q^{m'}\longrightarrow\mathbb F_q^{m_0}.\] This is a surjective \(\mathbb F_q\)-linear map whose restriction to \(H^{m'}\) is a bijection onto \(\mathbb F_q^{m_0}\). In particular it sends uniform inputs to uniform outputs. For each primary slot \(s_0\), interpolate that block’s public matrix entries as \(A_{s_0}(I,X)\) on \(H^\rho\times H^{m'}\), with individual degrees below \(h\). Define, for this block only, \[\begin{align*} p_{m'}(R,I,X) &=\sum_{s_0}A_{s_0}(I,X) f_{s_0,R}(w_{\rm pack}(X)), \tag{109}\\ p_j(R,I,X_1,\ldots,X_j) &=\sum_{x_{j+1},\ldots,x_{m'}\in H} p_{m'}(R,I,X_1,\ldots,X_j,x_{j+1},\ldots,x_{m'}) \quad(0\le j<m'). \tag{110}\end{align*}\] The top identity requests the primary with the public slot mask \((A_{s_0}(I,X))_{s_0}\), made smooth by additive splitting. This is a linear probe; the matrix entries are not unknown operands.

The final condition is the tested identity \[ \sum_{\text{primary blocks }b} p_{0,b}(R,I)=0. \tag{111}\] No chart for this mixed sum is stored. On legal data it vanishes on every \(I\in H^\rho\) and every \(R\in K\). Its individual \(I\) degrees are below \(h\), and its honest \(R\) coordinate degrees are below \(q\), so this is a polynomial identity. Conversely, its vanishing at \(R=1\) and at the row grid, with correct partial sums, is exactly the original matrix condition.

Division enforces all partial sums uniquely. For \(1\le j\le m'\) introduce quotient and remainder charts and impose \[\begin{align*} p_j&=(X_j^h-X_j)Q_j+X_j^{h-1}p_{j-1}+E_j, \tag{112}\\ p_{j-1}&\text{ is independent of }X_j, \qquad \deg_{X_j}E_j\le h-2. \tag{113}\end{align*}\] In characteristic two, \[\sum_{x\in H}x^r=0\quad(0\le r<h-1),\qquad \sum_{x\in H}x^{h-1}=1.\] Here the \(r=0\) identity is \(h=0\) in the field. The coefficient of \(X_j^{h-1}\) in the remainder modulo \(X_j^h-X_j\) is thus precisely the sum of the original polynomial over \(X_j\in H\). Euclidean division by this monic polynomial uniquely fixes \(Q_j\), the top remainder coefficient \(p_{j-1}\), and \(E_j\). Starting at (109), downward induction fixes all certificates and gives (110). Independence from later trailing coordinates follows in the same induction.

To test the degree restriction without concentrated reads, write \[ G_j(R,I,X_{\ne j},U) =\sum_{b=0}^{h-2}E_{jb}(R,I,X_{\ne j})U_b, \qquad U\in\mathbb F_q^{h-1}, \tag{114}\] where \(E_{jb}\) is the coefficient of \(X_j^b\) in \(E_j\). Check independence from \(X_j\), addition in \(U\), and homogeneity under a uniform nonzero scalar \(\lambda\in\mathbb F_q\). Sampling a nonzero scalar makes \(\lambda U\) uniform; zero homogeneity already follows from addition. If these identities are exact, \(G_j\) is pointwise \(\mathbb F_q\)-linear in \(U\), and uniqueness of reduced interpolation makes its polynomial linear in \(U\). Now check \[ E_j(R,I,X)=G_j(R,I,X_{\ne j},(1,X_j,\ldots,X_j^{h-2})). \tag{115}\] The special \(U\) tuple is queried as two uniform additive summands. Only after linearity has been established in the exact-soundness case analysis do we use the \(O(D+h)\) degree bound for this substitution. The earlier linearity discrepancies have degree \(O(D)\) and themselves have constant gap. Equation (115) then enforces (113) and fixes \(G_j\) uniquely.

A whole list is checked at once. Sampling a single recurrence index would lose a factor \(m'\). Instead choose a cyclic permutation \(\omega\) of the \(m'\) scalar coordinates so that coordinate \(j\) of \(\omega^jX\) is one fixed coordinate of \(X\). Store \[ \overline p_j(R,I,X)=p_j(R,I,\omega^jX), \qquad p_{j-1}(R,I,\omega^jX) =\overline p_{j-1}(R,I,\omega X), \tag{116}\] and store \(Q_j,E_j,G_j\) in the equation-\(j\) frame, with \(U\) unchanged. Both public powers in (112), and the predecessor independence axis in its corresponding frame, are now common across all \(j\). A uniform mask on the recurrence-index list checks all its equations with boundedly many point probes. Endpoint slices and predecessor shifts only change the requested linear mask, which is split smoothly. The coefficient families use the same \(U\) group in every slot. If \(m'=0\), retain only the unsummed top contribution and introduce no division family.

Degree, covariance, and exact gap. The top degree is at most \[ 2d_{\rm in}+(\rho+m')(h-1). \tag{117}\] Monic division by \(X_j^h-X_j\), reduction, coefficient extraction, and finite summation do not increase total degree. Multiplication by a linear \(U_b\) costs at most one. This proves the honest degree bound. There is a fixed number of families per primary; the growing recurrence index is one \(O(\ell)\) slot axis, and the additional \(U\) domain has \(h-1\le\ell\) coordinates.

First test ignored coordinates and the independence and linearity devices. Unless they hold identically, one has a nonzero polynomial discrepancy of degree \(O(D)\) and constant rejection probability. Once they hold, every remaining displayed discrepancy has degree \(O(D+\ell h)=o(q)\) and a failed slot identity survives a random contraction with constant probability. Exact identities give the uniqueness just proved and then (111). A fixed mixture of test types therefore has a uniform positive gap. Perfect completeness concerns canonical tuples within the budgets; it does not claim that every legal primary of degree exactly \(D\) has auxiliaries of degree at most \(D\).

For covariance even on invalid inputs, expand a lifted primary after substitution over \(K\) as \[f_R=\sum_{j=0}^{M-1}R^{\widetilde j}v_j\] in its evaluation arrays. All subsequent operations in (109)–(114) are the same fixed linear maps on that primary, independent of \(R\). This includes division and coefficient extraction, since honest-degree evaluation arrays determine the required polynomials by interpolation. These maps preserve the exponent list, and rotating the input by \(x\in C\) replaces \(R\) by \(xR\). No final zero-row identity is used. In particular every canonical certificate is defined even when its primary belongs to data failing the final condition.

Finally, all point substitutions used in these tests are coordinate permutations, surjective packing, nonzero scaling, fresh independent coordinate replacement, or additive splitting. They have bounded point marginals. Requested masks are split. All arrays have polynomial size, and every construction operation is finite linear algebra on them. This proves the remaining claims. ◻

Proof. Use the needed \(T_W\) inputs and the output \(G\) as primaries. Impose their lifted shapes in the designated variables and the linear rows \[ G(z,\cdot)=\sum_{x\in C}L_{x^{-1}z}(T(x,\cdot)) \quad(z\in C). \tag{125}\] Rows also range over every output evaluation position and slot. On canonical \(T\) inputs, only \(x=c^{-1}\) contributes, giving (124). The lift shape then determines the whole chart uniquely. The row condition is invariant under the simultaneous replacement \(G(z)\mapsto G(u_0z)\) and \(T(x)\mapsto T(u_0x)\): setting \(x'=u_0x\) changes the map index to \((x')^{-1}u_0z\). The shape conditions are invariant too, so Lemma 44 applies. Every input has logical degree at most \(k_0\); interpolation and all per-primary certificate operations are linear and preserve that degree. Covariance follows first on \(C\) and then by uniqueness of the lift, and for the auxiliaries by the last part of the linear tool. No validity row on \(b\) was used. Public clock-dependent terms are supplied through \(T_1=J_c\), keeping the rotating condition linear. ◻

Proof. Let \(F\) have positive assigned tier \(k_0\). For every required flip mask, retain its native variables \(Y\) and slots, adjoin a new full variable \(Z\), and prescribe on the cyclic grid \[ G_F^\sigma(c,b;z,Y) =F(cz,b+h_\sigma(cz);Y)-F(cz,b;Y),\qquad z\in C. \tag{126}\] Extend in \(Z\) by the cyclic lift. Both parent terms are evaluated in frame \(cz\); the parent’s existing argument coordinates remain exactly \(Y\). A tag-\(0\) parent uses the full flip alphabet (105). For a tag-\(i\) parent, only the two legacy coefficients matter: the input bits \(s_i\) are never written and work bits are absent from its recipe. Use the fixed four masks \[ h_\chi(y)=\chi_1\mathbf 1_{e_{y^{-1}}} +\chi_2\mathbf 1_{e_{(\gamma y)^{-1}}}, \qquad \chi\in\{0,1\}^2, \tag{127}\] independent of \(k\) and \(i\).

For a squarefree monomial, a fixed Boolean translation gives \[ \prod_{j\in S}(b_j+h_j)-\prod_{j\in S}b_j =\sum_{T\subsetneq S}\left(\prod_{j\in T}b_j\right) \left(\prod_{j\in S\setminus T}h_j\right). \tag{128}\] Thus (126) has logical degree at most \(k_0-1\). Lifting its new variable adds at most \(\ell(h-1)\) to its coordinate degree. For each absolute frame \(y\), output evaluation point, and inherited slot, the derivative is a known linear combination of grid monomials of degree at most \(k_0-1\): from \(\{w,e\}\) for tag \(0\), or from \(\{s_i,e\}\) for tag \(i\).

These coefficients are computed from the canonical parent recipe, not from the presently supplied parent table. An explicit method is bounded-degree Boolean interpolation. For a multilinear function \(P\) of degree at most \(r\) on a universe of \(N\) bits, its coefficient on \(S\), \(|S|\le r\), is \[ [b_S]P=\sum_{T\subseteq S}(-1)^{|S|-|T|}P(\mathbf 1_T). \tag{129}\] In characteristic two the signs are all one. Use this on the right side of (126), which is computable on every Boolean argument, including translated invalid tapes. There are only \(\sum_{j\le r}\binom Nj=\mathop{\mathrm{poly}}(n')\) required subsets, because \(r\le3\) and \(N=\mathop{\mathrm{poly}}(n')\). For tag \(i\) the interpolation universe is the common ordered list of its \(L\) source bits and \(M\) legacy bits, with no work coordinates. Interpret the resulting coefficients as public maps \(L_y\) on the permitted monomial arrays.

Apply Lemma 45 using only inputs through tier \(k_0-1\). The output derivative and every newly introduced auxiliary receive that tier and the parent’s tag. In particular a certificate for a shared tag-\(0\) \(T\) input in this positive call receives the positive ancestry tag. The derivative rotates only its new variable, since on the grid \[G_F^\sigma(u_0c,b;z,Y)=G_F^\sigma(c,b;u_0z,Y),\] and lift uniqueness extends this to \(K\). Its older parent variables are not additionally scaled under a frame change. Each verification auxiliary instead rotates its own new \(R\), as proved by the linear tool.

Repeat this operation for every added positive-tier family, including derivatives and all their proof families. Every descendant call strictly lowers its assigned tier, whether or not its actual degree was already smaller. The recursion ends after at most three levels. A family has only finitely many children for fixed \(k\). A derivative inherits its parent’s single slot axis; a verification auxiliary uses its own recurrence-index axis rather than tensoring it with primary slots. Consequently the number of families is fixed, their native dimensions and slot lengths remain \(O(\ell)\), and their coordinate degrees remain \(O(\ell h)\). Tier-zero charts require no derivative for a fixed-frame Boolean edit.

All maps have polynomial construction cost: there are polynomially many frames, evaluations, slots, monomials, and rows, and only a fixed number of recursive levels. Finite sums, monic division, coefficient extraction, and interpolation are fixed linear operations on each primary array. They neither create a further logical product nor import another primary’s dependency. This remains true when the final row sum fails, by Lemma 44. The asserted invalid-tape recipes and their degree bounds follow as well. ◻

Proof. Choose row lists, their order, and zero padding separately for each call’s local template. Do not choose a row dimension by maximizing over all calls in the actual graph. In each copy/port call use the same input-shape rows, bitness rows, and \((c,j)\) copy rows, and the same full primary-list conventions. Although the work-side matrix depends on \(w_{i,j}\), its dimensions do not. This makes all port-dependent primary blocks literal copies of their dummy blocks.

For a concrete example, consider \(W_{e,s_i}\) in (119). Its matrix \(A_{e,s}(I,X)\) knows the stage and the source position \(\iota(j)\), and has no reference to \(w_{i,j}\). That destination appears only in the separate \(A_{e,w}\) block. The top formula for its positive certificate is \[p_{m',e,s}(I,X) =A_{e,s}(I,X)W_{e,s_i}(w_{\rm pack}(X)),\] with the evident slot contraction when needed. Its row padding, packing, recurrence permutation, recurrence-index order, and coefficient-vector domain are therefore exactly those of the one-port construction. Each partial sum, quotient, remainder, and coefficient chart uses that block alone. The equality with the work-side contribution is tested only in (111); there is no mixed stored chart from which work addresses could enter this positive family.

The critical source-bit calls agree directly, since they use the same initial-copy address rule and the same zero rule thereafter. For the remaining families, induct on positive ancestry. If a parent’s recipe and native layout agree, its derivative uses exactly the same restricted mask (127). Its values on every subset in (129), including translated invalid inputs, are identical in the two templates. Hence its maps \(L_y\) are identical. Make each derivative call separately by parent type and mask, with the fixed allowed lower-tier monomial list, full output-equality rows, shape rows, deterministic order, and local padding. Its output and every per-primary auxiliary then agree literally by the linear-tool formulas. This includes auxiliaries whose primary is a shared legacy-only or constant \(T\) chart: the input formula is common and the auxiliary’s own call matrix is the standardized positive one. These auxiliary families are themselves parents in the induction. Strictly decreasing tiers terminate it.

Keep descendants from distinct standardized calls separate, without coalescing them differently with circuit-dependent tag-\(0\) families. Additional full work masks and additional tag-\(0\) calls then create separate branches and do not change any positive branch. The construction does not use validity to establish this correspondence. ◻

Proof. Initially a monomial uses at most \(d\) full variables and a \(T\) chart one more. Base linear calls have native dimension \(O_d(\ell)\). Their row counts are bounded by \(q^{C\ell}\) for an absolute fixed \(C\) independent of \(k\): the work grid, clock grid, input length, and stage count are at most \(h^\ell\), and shape conditions are polynomial in the corresponding full evaluation sizes. Occupied-copy calls are separate, so their number does not enter an individual row dimension. They use fixed stage/source-index lists.

For a derivative call on a parent of \(m_0\) native coordinates and one possible slot axis, its output, shape, and clock-equality rows have size polynomial in \(q^{m_0+C\ell}\), with a fixed exponent. Its permitted monomial input list is fixed by its tag and tier. Different masks have separate calls. Therefore \(\rho/\ell\), the new native dimension divided by \(\ell\), and the new slot length divided by \(\ell\) are bounded by a fixed multiple of one plus the corresponding parent bounds. Digit unpacking contributes the fixed factor \(v\); the coefficient-vector domain contributes at most \(h-1\le\ell\) coordinates. Iterating through the at most three tier drops gives an absolute bound \(C_{\rm dim}\ell\), independent of the number of calls or ports.

Choose \(u\) to accommodate this bound and at most \(d+1\) additional whole labels along an inherited derivative-axis chain. Put every full \(K\) variable in a whole label, and pack remaining native \(q\)-coordinates into additional labels, ignoring their padding. An initial chart or a new verification auxiliary is a placement root; unrelated roots may reuse labels according to their native templates. A derivative retains exactly its parent’s placements and chooses a deterministically first unused whole label for its new variable. Repeat along that chain. No labels have to be globally disjoint across all ports: tests between unrelated charts assemble their native arguments separately and fill ignored coordinates uniformly. Enforce all ignored-coordinate conditions. These deterministic choices depend only on local templates and ancestry, proving positive-family agreement.

For tag-\(0\) calls at fixed \(k,L\), use the full uniform (stage, work-position) validity list, fixed critical-read roles and tiers, the full fixed flip alphabet for every parent, and the allowed monomial, shape, and output lists fixed by domain and tier. Only matrix entries and rule values vary with the circuit. This makes the entire actual layout independent of circuit wiring, as claimed. ◻

Proof. Center the \(\mathbb F_q\) coordinates of \(Z_\alpha\) at the coordinate vector of \(1\in K\). Decompose \(F\) into parts homogeneous of degree \(r\) in the centered coordinates. Their sums under all nonzero scalar dilations have multiplier \[\sum_{j=0}^{q-2}g^{jr} =\begin{cases}1,&r=0,\\0,&0<r<q-1.\end{cases}\] For \(r=0\) this is \(q-1=1\) in characteristic two, and for positive \(r\) it is a geometric sum with ratio different from one. Thus only the constant homogeneous part remains. Pullbacks on disjoint labels commute by direct substitution. ◻

Proof. For each nonempty \(S\), fix one \(\alpha\in S\) and require \[ C^S_{F,(j_\alpha,\mathbf j_-)} =D_\alpha C^S_{F,(j_\alpha+1,\mathbf j_-)} +M^{\rm mark}_{j_\alpha} C^{S\setminus\{\alpha\}}_{F,\mathbf j_-}, \tag{135}\] with the upper boundary at \(j_\alpha=N\) defined to be zero. For fixed \(\mathbf j_-\) this is triangular downward in \(j_\alpha\). If the marker is zero its only solution is zero. If it is one-hot at \(t-1\), its solution is \[C^S_{F,(j_\alpha,\mathbf j_-)} =\begin{cases} D_\alpha^{t-1-j_\alpha} C^{S\setminus\{\alpha\}}_{F,\mathbf j_-}, &j_\alpha<t,\\ 0, &j_\alpha\ge t. \end{cases}\] Induction on \(|S|\) gives exactly (134).

Here are explicit slot formulas for the shift, including boundary handling. Use little-endian radix digits \(j=\sum_{s=0}^{a-1}j_sB^s\) and let \(\lambda_L(j)=\prod_{s=0}^{a-1}L_s[j_s]\). With out-of-range coefficients zero, \[\begin{align*} \sum_{j=0}^{N-1}\lambda_L(j)C_{j+1} &=\sum_{r=0}^{a-1}L^{(r,+)}\cdot C, \tag{136}\\ L_s^{(r,+)}[d] &=\begin{cases} L_s[B-1]\mathbf1_{d=0},&s<r,\\ \mathbf1_{d\ge1}L_r[d-1],&s=r,\\ L_s[d],&s>r, \end{cases} \\ \sum_{j=0}^{N-1}\lambda_L(j)C_{j-1} &=\sum_{r=0}^{a-1}L^{(r,-)}\cdot C, \tag{137}\\ L_s^{(r,-)}[d] &=\begin{cases} L_s[0]\mathbf1_{d=B-1},&s<r,\\ \mathbf1_{d\le B-2}L_r[d+1],&s=r,\\ L_s[d],&s>r. \end{cases} \end{align*}\] Indeed the first pullback mask on index \(k>0\) is \(\lambda_L(k-1)\). Partition \(k\) by its least digit \(r\) which is nonzero; precisely the lower digits borrow. The second pullback is \(\lambda_L(k+1)\) for \(k<N-1\); partition by the least digit below \(B-1\). Overflow is absent in both formulas. Slicing at zero is a single separable restriction, and interval restrictions use the bounded rectangle decomposition used in (133). Tensoring these expansions over the bounded number of stack axes still gives a bounded number of separable masks. Split every requested mask additively as in (107).

Contract the entire identity (135) over all slots. The last term factors into a contraction of the marker on axis \(\alpha\) and a contraction of the smaller stack on its other axes and inherited slots. In the exact-soundness analysis marker constancy has already been imposed, so its full point can be sampled independently of the smaller stack point. This retains perfect completeness on canonical data. If the recurrence is not an identity, its discrepancy has point degree at most \(2D\) and bounded mask degree, giving constant rejection probability. Honest stacks are affine pullbacks of persistent charts or zero, so they have the same honest coordinate degree. Marker tag \(0\) is compatible with every parent tag. This proves all claims. ◻

Proof. The tests just constructed constitute a fixed number of family types for fixed \(k\); growing slot lists are checked by whole contractions. We prove exact soundness in an order that licenses all substitutions. First consider ignored-coordinate requirements, mode and marker constancy, and the independence and coefficient linearity devices of every linear tool. If one fails, its direct test has constant gap. Otherwise these are exact polynomial identities. Monomial factorization and the nonrotating base calls then force a Boolean tape, all its monomial extensions, its union-of-stages validity, its output chart, and the canonical per-primary certificates. Mode and marker membership give unique \(\eta\) and \(t\). The legacy identity (122) forces the unique frame \(c\) and fixes \(J_c\); clock-monomial factorizations fix all \(T_W\).

Now apply the clock-formula calls in construction order. Their uniqueness fixes each critical output, each derivative, and every auxiliary. A derivative’s rows were computed from a prescribed parent recipe; the proof never treats an unverified parent table as an additional oracle for those rows. The strictly decreasing tier construction is therefore acyclic. Finally the triangular stack identities give (134). Hence exactness of all identities gives precisely a valid label’s canonical tuple. Conversely every valid label satisfies every identity for every random choice in the support.

If exactness fails, the first failed identity in this ordering has point degree \(O(D+\ell h)\) after the stated preliminary devices and bounded degree in its mask variables. The polynomial zero and contraction bounds give a uniform positive rejection probability. Taking the minimum over the fixed mixture gives the asserted gap. Honest degrees are \(O(\ell h)<D\) eventually, also after any later fixed-factor enlargement of the point domain. The constants in these degree bounds and in the finite family list depend on fixed templates, not on the values of public circuit coefficients.

For the product claim, the only possibilities are monomial factorizations, \(J_cW\) factorizations, marker membership, and marker times smaller stack. In a factorization, choose the two native operand arguments independently, assemble the output’s relevant groups from them, and independently fill all ignored coordinates. Even repeated operand types then have independent full operand points. The relevant output groups are independent uniform too. For marker products use independent points, justified by the earlier constancy step. Every such pair has compatible tags by construction. Bitness, diagonal grid entries, copy equalities, and all other correlated grid uses are linear matrix rows, so they require no concentrated unknown-product query. The linear tool’s packing, permutation, and splitting probes have bounded individual point density. Dependent or prescribed masks, including those inside products, are smoothed by fresh independent axis splittings. These observations prove the stated probe interface. ◻

Proof. We give formulas for each transition, including the boundaries. Write \(C^{S,t}_{F,\mathbf j}\) for the stack at progress \(t\).

Progress increase and decrease. On increasing from \(0\) to \(1\), initialize every nonempty stack by \[ C^{S,1}_{F,\mathbf j} =\mathbf1_{\mathbf j=\mathbf0}F, \qquad M^{\rm mark,new}_j=\mathbf1_{j=0}. \tag{138}\] For \(0<t<q-1\), and \(\mathbf j\) in the padded radix range, let \(Z(\mathbf j)=\{\alpha\in S:j_\alpha=0\}\) and put \(k_\alpha=0\) for \(\alpha\in Z(\mathbf j)\) and \(k_\alpha=j_\alpha-1\) otherwise. Then \[ C^{S,t+1}_{F,\mathbf j} =\left(\prod_{\alpha\in Z(\mathbf j)}D_\alpha\right) C^{S,t}_{F,\mathbf k},\qquad M^{\rm mark,new}_j=M^{\rm mark,old}_{j-1}, \tag{139}\] with zero padding. For \(j_\alpha>0\), the old exponent is \(t-1-(j_\alpha-1)=t-j_\alpha\), as required; for \(j_\alpha=0\), one extra dilation gives exponent \(t\). Old inactive coefficients remain zero. Partitioning by \(Z(\mathbf j)\) and using the radix pull formulas implements this with boundedly many mask operations. For a decrease from \(t>0\), the formula is simply \[ C^{S,t-1}_{F,\mathbf j} =C^{S,t}_{F,(j_\alpha+1)_{\alpha\in S}},\qquad M^{\rm mark,new}_j=M^{\rm mark,old}_{j+1}. \tag{140}\] Its exponent is \(t-1-(j_\alpha+1)=t-2-j_\alpha\) and its support is \(j_\alpha<t-1\). In particular \(t=1\) produces empty stacks and a zero marker. Persistent data remain fixed during these progress transitions.

Critical readings and full-progress edits. At \(t=q-1\), for a critical chart \(F\) with projection axis \(\alpha\), \[ \sum_{j=0}^{N-1}C^{\{\alpha\}}_{F,j} =\sum_{j=0}^{q-2}D_\alpha^{q-2-j}F =F\big|_{Z_\alpha=1}. \tag{141}\] All-ones radix masks perform this sum. A critical output ignores every other native group, so the result is a constant-in-point logical or public rule bit. Lemma 40 therefore determines the edit mask from finitely many such bits.

Fix that mask and direction. For every positive-tier parent \(F\) and every \(S\subseteq A_F\), including \(S=\varnothing\), add the increment \[ \Delta C^S_{F,\mathbf j} =\sum_{r=0}^{N-1} C^{S\cup\{\alpha_{\rm new}\}}_{G_F^\sigma,(\mathbf j,r)}. \tag{142}\] For a positive port parent use its corresponding legacy mask \(\chi\). For active old indices, commuting all inherited-label dilations with projection on the new label gives \[\begin{align*} \Delta C^S_{F,\mathbf j} &=\left(\prod_{\alpha\in S}D_\alpha^{q-2-j_\alpha}\right) G_F^\sigma(c,b;1,Y) \tag{143}\\ &=\left(\prod_{\alpha\in S}D_\alpha^{q-2-j_\alpha}\right) \bigl(F(c,b+h_\sigma(c);Y)-F(c,b;Y)\bigr). \end{align*}\] If any inherited index is inactive, every summand is zero. This is precisely the new stack minus the old one, including the empty stack, which is the persistent chart itself. The recursion supplied the necessary lower-tier derivative for every positive-tier parent, including proof and derivative charts, so all coordinates update simultaneously from old data. Tier-zero charts stay fixed under the Boolean change. The marker is unchanged and the mode changes as prescribed. Reverse edits obey the same calculation with the inverse branch’s coefficients.

Frame change and edge flags. At empty progress all stacks are zero. For frame advance, a rotating persistent chart is pulled back on its one designated variable by multiplication by \(\gamma\); for reverse advance use \(\gamma^{-1}\). A nonrotating persistent chart stays fixed. The empty stacks remain zero, and the mode changes. In particular, an auxiliary with native variables \((R,I,X,U)\) rotates only \(R\); its packing, division, and coefficient formulas are not recomputed by the update.

The successor rules are: pre increases unless full; at full pre perform the enabled edit, or report the absent wrap edge; post decreases unless empty; at empty post advance the frame. The predecessor rules are: full post performs the inverse enabled edit, or reports the absent wrap edge; other post reverses a decrease; positive-progress pre reverses an increase; empty pre reverses the frame advance. Empty must also be distinguished for initialization in (138). These are all finite cases. Comparing the marker with the public zero tensor or the public full tensor uses random separable masks and binary forms, with a constant inequality-detection gap. A fixed number of repetitions makes either comparison as reliable as prescribed. Mode and critical constant bits are read with forms taking \(1\) to \(1\). No progress index scan or proposed-target validity check is needed for edge flags on the valid inner path.

Finally, all point maps in these formulas are identities, full-label dilations (130), or full-label multiplications by \(\gamma^{\pm1}\), and their bounded compositions. They are invertible \(K\)-affine maps. In (142), the child retains the parent’s placements and has an already available extra whole label; the sum projects that label to one and makes it irrelevant to the target coordinate. Thus a requested update has the form \[ L\cdot F^{\rm new}(Y) =P_L(Y)+\sum_{r=1}^{R_*}a_r (L_r\cdot F_r)(T_rY), \tag{144}\] where \(R_*\) is bounded, \(P_L\) is publicly computable, \(a_r\) and \(L_r\) are fixed by the requested masks and branch, and \(T_r\) is an invertible \(K\)-affine map. No \(a_r\) or slot pull depends on \(Y\) or on a later row index. The inherited tags in Lemma 46, and the public fixed branch, give the tag assertions. ◻

Proof. At both labels, \(c=\gamma^{-1}\), work is blank, \(e_1=1\) and other legacy bits are zero, the mode is post, and progress is the public value specified in (106). Tag-\(0\) persistent recipes depend only on these values and public circuit data, so they are computable. Their derivatives might evaluate a translated tape with nonblank work, but every flip vector is then public and the translated work is public too. Such a tape need not be valid: the canonical recipe is evaluated by its finite-array operations, and never by solving for a valid circuit computation. In particular a work-side copy certificate uses its own work primary and public matrix, not a stored sum involving \(s_i\). Recursively, all its derivative and proof arrays remain public. Stack dilations at either fixed progress preserve this conclusion.

Positive persistent recipes and layouts agree by Lemma 47, and their placements agree by Lemma 48. The projection-axis choices, inherited labels, \(q,a,B\), and radix slot conventions also agree. Formula (134) therefore gives identical stacks at each of the two progresses, including every descendant proof stack. This proves a literal map of original algebraic indices, not merely equality up to unspecified isomorphisms or comparable sizes. Applying the same public row extension, restriction to an ordered line, extraction of its coefficients, slot contraction, or basis map to corresponding arrays preserves both values and indices. Later balancing by repeated copies may use different multiplicities; it does not alter this statement about original indices.

At a fixed frame every persistent value and coefficient has assigned degree at most three in the Boolean tape. At the present labels all tape bits except the read inputs are fixed public bits. Fixed-progress stacks are fixed affine pullbacks or zero. Their degree is thus at most three in the read inputs as well. A public linear operation over \(\mathbb F_q\), or over any fixed public extension field followed by prime-field coordinates, is \(\mathbb F_2\)-linear on these functions. It cannot increase multilinear degree. For two degree-three coordinate vectors, a binary bilinear form is a sum of products of two such coordinate functions and hence has degree at most six. Copies do not alter degree. Evaluate the specified canonical bit on supports of size at most six and apply (129); the number of evaluations and each canonical finite-array computation are polynomial. This proves the coefficient-computation assertion. ◻

Proof. The path and endpoint assertions are Lemmas 40 and 42. The linear tool, clock-formula construction, derivative closure, and common placements give the persistent arrays. Lemma 50 gives their stacks. At fixed \(k\), all depths and family counts are fixed, while all dimensions and total mask lengths are \(O(\ell)\). Consequently every domain and mask space has size \(q^{O(\ell)}=\mathop{\mathrm{poly}}(n')=\mathop{\mathrm{poly}}(L)\). Row and coefficient arrays have the same polynomial bounds. Their construction consists of the explicit finite-array operations and bounded-degree interpolation above. In particular, increasing the number of separate calls does not change the already chosen common \(u\).

Lemma 51 proves the exact gap and all point and tag restrictions. Here is its conversion to the asserted binary-form interface. A nonzero element of \(\mathbb F_q\) is detected by a uniformly random additive form \(\mu:\mathbb F_q\to\mathbb F_2\) with probability \(1/2\). Applying \(\mu\) to a field equality turns its public linear terms into additive forms, since \[\mu\left(\sum_r a_r x_r\right) =\bigoplus_r(\mu\circ[a_r])(x_r), \qquad [a_r](x)=a_rx.\] For a product, the requested bit is the binary bilinear form \((x,y)\mapsto\mu(xy)\). Random annihilating forms handle mode membership as already specified. A bounded field test therefore uses a bounded number of such bits and Boolean operations, losing at most a fixed factor in its gap. Prescribed masks and forms can be split by fresh additive randomness. Their public descriptions have polynomial size; even the space of all binary bilinear forms on \(\mathbb F_q\) has cardinality \[2^{(\log_2 q)^2}=\mathop{\mathrm{poly}}(n'),\] since \(\log q=O(\log\log n')\). A bounded sequence of all the displayed random choices consequently has polynomial support.

The invalid-tape assertion follows from the per-primary canonical formulas and the finite-difference construction, not from successful final rows. If a label is invalid, a validity or frame/legacy condition fails and exact soundness rejects; uniqueness of the division certificates prevents a different proof table from canceling the failed condition. Lemma 52 proves all fixed-branch update formulas, including for canonical invalid tapes. Frame changes occur only when stacks are empty, so no commutation between centered dilations and frame scaling is needed. Finally Lemmas 47, 48, and 54 give the exact standardized source correspondence and its Boolean-degree bounds. This proves every part of the interface. ◻

Proof. Here are the two primary group-theoretic inputs and their exact use. Ershov–Jaikin-Zapirain (Ershov and Jaikin-Zapirain 2010, Theorem 1.1) prove property \((T)\) for \(\mathrm{EL}_r(R)\) for every finitely generated associative unital ring \(R\) and \(r\ge3\). Their generating-set bound in Section 6.1 applies to the elementary matrices with entries in a fixed ring-generating set containing 1. In particular, their equations (6.1)–(6.2) give the positive Kazhdan constant \[\kappa_r=\bigl[8(48\sqrt2+2\sqrt{3r})\bigr]^{-1}\] for \(\{e_{ij}(1),e_{ij}(t):i\ne j\}\) in \(\mathrm{SL}_r(\mathbb{F}_2[t])\); the equality with the elementary group holds because \(\mathbb{F}_2[t]\) is Euclidean. No restriction excluding characteristic two occurs in this theorem.

Shalom (Shalom 1999, Theorem 3.4 and Corollary 3.5), applied to the discrete commutative ring \(R=\mathbb{F}_2[t]\), bounds the displacement of every translation in \(R^2\rtimes\mathrm{SL}_2(R)\) by 484 times the maximum displacement on the basis translations and \(e_{12}(1),e_{12}(t),e_{21}(1),e_{21}(t)\). Signs coincide in characteristic two. This is the homogeneous displacement form of the corollary’s tolerance statement, obtained by scaling and taking limits. It bounds the translation sector; it alone does not assert expansion of the full affine group.

Set \(\Lambda=R^r\rtimes\mathrm{SL}_r(R)\) and let \(S\) consist of all basis translations and the elementary matrices just listed for all ordered coordinate pairs. Embed Shalom’s rank-two group on each such pair. Since a translation is a product of \(r\) coordinate translations, every unitary representation satisfies \[\sup_{a\in R^r}\lVert av-v\rVert \le 484r\max_{s\in S}\lVert sv-v\rVert. \tag{\ref{ib:affine-expansion}.1}\] Let \(V_N\) be the translation-invariant subspace. Its orthogonal projection commutes with \(\Lambda\), since the translations are normal. On \(V_N^\perp\), the minimum-norm point of the closed convex translation-orbit hull is zero. The displayed bound therefore gives \(\lVert v\rVert\le484r\max_{s\in S}\lVert sv-v\rVert\) on this subspace. On \(V_N\), a representation without group-invariant vectors is a representation of \(\mathrm{SL}_r(R)\) without invariant vectors, so the preceding Kazhdan bound applies. Orthogonally combining the two bounds gives a positive Kazhdan constant \(\kappa\) for \((\Lambda,S)\). Explicitly, if \(\kappa_r\) is the quoted linear-group constant, one may take \(\kappa=((484r)^2+\kappa_r^{-2})^{-1/2}\).

The set \(S\) generates \(\Lambda\): the third-index elementary commutator multiplies entries, entries in a root subgroup add, and conjugating basis translations gives arbitrary coordinate translations. Choose a field presentation \(K=R/(p(t))\) by a monic irreducible polynomial. Elementary generation over a field shows that the quotient map surjects onto \(U(K)\). Pulling back its mean-zero regular representation preserves the Kazhdan bound. If \(d=\lvert S\rvert\), the half-lazy walk has Dirichlet form \[\langle v,(1-M)v\rangle =\frac{1}{4d}\sum_{s\in S}\lVert sv-v\rVert^2 \ge\frac{\kappa^2}{4d}\lVert v\rVert^2\] on mean-zero vectors, and nonnegative spectrum. On the product group, choose a factor uniformly and take this step there. The commuting tensor-factor operators give another uniform positive gap and nonnegative spectrum. A sufficiently large fixed power has mean-zero norm at most \(1/64\). Keep all walk labels, including identities and coincident group elements, as a symmetric multiset; repeat labels if necessary to ensure \(d_e\ge8\). All matrices have fixed dimensions over polynomial-size fields, so enumeration and every stated computation are polynomial-time finite-array operations. ◻

Proof. Treat the \(2c_ed_e\) matrix entries as indeterminates. The square system matrix on parity labels \(1,\ldots,2c_e\) has nonzero determinant polynomial: specialize left row \(b\) to select label \(b\), and right row \(b\) to select label \(c_e+b\). This gives a permutation matrix, including when some generators coincide. Multiply this determinant by all maximal minors of both local matrices. Each factor is a nonzero polynomial; their product is nonzero and has total degree at most \[2c_e\lvert \mathcal H\rvert +2c_e\binom{d_e}{c_e}.\] Take the least extension \(J/\mathbb{F}_q\) of cardinality exceeding this bound. It has polynomial cardinality. A nonzero polynomial of smaller total degree than \(\lvert J\rvert\) cannot vanish everywhere on \(J^{2c_ed_e}\). Exhaustive search over this constant number of entries, testing the determinant and minors, therefore finds a specialization in polynomial time. Inverting the parity matrix constructs \(E\).

Column independence proves local distance \(c_e+1\), also for vector symbols: a nonzero vector-valued local word supported on at most \(c_e\) columns would contradict that independence after any nonzero coordinate projection. Right shifts permute left stars and right stars in (145)–(146) and preserve the systematic labels. Uniqueness proves \(ER_h=R_hE\). ◻

Proof. First use the full domains. For every \(\alpha\in V^*\), scalar projection and the cited theorem give a polynomial \(p_\alpha\) with \(\mathop{\mathrm{dist}}(\alpha f,p_\alpha)\le2e\). Distinct scalar polynomials in this degree range differ at a fraction at least \(1-D/q\) of points. Consequently, when \(6e<1-D/q\), comparison with \((\alpha+\beta)f\) forces \[p_{\alpha+\beta}=p_\alpha+p_\beta, \qquad p_{a\alpha}=a p_\alpha \quad(a\in\mathbb{F}_q).\] The second identity uses at most \(4e\) disagreement; the assertions with a zero form or scalar follow in the same way. Coefficientwise finite-dimensional duality now gives one \(V\)-valued polynomial \(p\) for which \(\alpha p=p_\alpha\) for all \(\alpha\). A uniform \(\alpha\) detects each nonzero vector with probability \(1-1/q\), so \[(1-1/q)\mathop{\mathrm{dist}}(f,p) =\mathbb{E}_\alpha\mathop{\mathrm{dist}}(\alpha f,p_\alpha)\le2e.\] There is no factor depending on \(\dim V\).

For deleted domains, extend the point function arbitrarily and give every added line any degree-in-bound claim, for example zero. The full incidence disagreement is at most the retained-line disagreement plus the omitted-line fraction. The full-domain conclusion therefore gives vanishing error also on retained points. On any retained line whose claim differs from the restriction of \(p\), a nonzero scalar projection of their difference is a univariate polynomial of degree at most \(D\). The two claims disagree at a fraction at least \(1-D/q\) of its parameters. Averaging the original test error and the point replacement error, using the asserted uniform point marginal, bounds the fraction of such lines by their sum divided by \(1-D/q\). This tends to zero and proves the coefficient claim. ◻

Proof. Suppose first that \(f:G\to A\) fails addition with probability \(e\), where both groups have exponent two. For fixed \(x\) put \(D_x(y)=f(x+y)+f(y)\). The addition identities on the pairs \((x+y,y+z)\) and \((y,y+z)\) imply \(D_x(y)=D_x(z)\). Each pair is uniform when \(y,z\) are independent uniform elements, so the collision probability is at least \(1-2e\), for every \(x\). The most frequent value \(L(x)\) therefore has mass at least \(1-2e\). The identity \[D_{x+y}(z)=D_x(y+z)+D_y(z)\] and three majority bounds imply \(L(x+y)=L(x)+L(y)\) when \(6e<1\): at least one \(z\) realizes all three majority values. If \(f(x)\ne L(x)\), the conditional addition failure at \(x\) is at least \(1-2e\). Thus \(\mathop{\mathrm{dist}}(f,L)\le e/(1-2e)\).

For the field version, transfer the homogeneity test to \(L\). The scalars \(a\) satisfying \(L(ax)=aL(x)\) identically form an additive subgroup of \(\mathbb{F}_q\). If it is proper, at least half the nonzero scalars fail; for each failing scalar its nonzero additive discrepancy is nonzero on at least half the inputs. The homogeneity test with uniform nonzero scalar would then have failure at least \(1/4\). This contradicts failure tending to zero after a vanishing replacement cost. Hence \(L\) is field-linear.

Induct on the number \(j\) of axes. Markov’s inequality, with a threshold tending slowly to zero, makes all but a vanishing fraction of first-axis slices good for the remaining \(j-1\) tests. Replace good slices by multilinear maps and the remaining slices by zero. This changes a vanishing fraction of values. Regard the resulting slices as a map into the vector space of multilinear maps on \(j-1\) axes. A nonzero such map is nonzero on at least \(2^{-(j-1)}\) of uniform inputs: successively contract each axis, using that a nonzero linear map has a kernel of relative size at most \(1/2\). Thus vanishing first-axis test failure on values gives vanishing failure as equalities in this vector-space alphabet. The one-axis result finishes the induction. The same Markov cutoff over any additional parameters proves the mean version. ◻

Proof. Take a positive fixed mixture of the test families described below, including each present block type. Their query counts are bounded, and all requested nonuniform masks are implemented by the splitting operation above. We prove the gap by a sequential replacement argument. Consider any sequence of increasing sizes and words whose rejection tends to zero, allowing the public circuits to vary in the fixed template. We show distance tending to zero from a canonical valid word. A bounded smooth test retains vanishing rejection after a vanishing-distance change, by the union bound over its potential reads; for a branching test use its entire bounded answer tree.

Copies, symbols, and slot tensors. Compare two independent random copies of a uniform original bit. If the fraction of ones among its copies is \(p\), the test rejects with probability \(2p(1-p)\), which is at least \(\min(p,1-p)\). Replacing all copies by their majority costs vanishing distance. In each point or line \(Y\) block test additivity in \(\mu\). Lemma 59 and binary double duality replace the block, in mean over other indices, by Hadamard tables of genuine \(J\)-symbols. Next test addition and \(\mathbb{F}_q\)-homogeneity in every slot-mask axis, including the two coefficient-mask axes for a line. Test symbol equality by uniform \(\mu\), which detects any inequality with probability \(1/2\); pull field scalars onto this form before smoothing its raw accesses. The same replacement lemma makes all these symbols honest multilinear slot tensors at each edge and point or line, at vanishing mean cost. No global polynomial property has yet been asserted.

Point and line polynomials. At a uniform edge, retained ordered line, and parameter, compare the point symbol with line evaluation, using uniform original slot masks and a uniform bit comparison. Split the two specified evaluation masks in (148). A nonzero symbol discrepancy has a constant binary detection probability, so the line–point disagreement tends to zero in mean. For most edge and original-mask tuples apply Lemma 58, with \(V=J\) as an \(\mathbb{F}_q\)-space, to obtain a degree-at-most-\(D\) rectangular polynomial. Use zero on the exceptional tuples. The lemma’s line-coefficient conclusion also replaces the line tables by the restrictions of these polynomials at vanishing cost.

The selected polynomials need not yet be coherent between original mask tuples. Transfer the previous multilinearity identities to them using their mean point error. A false identity between degree-in-bound polynomials is nonzero on at least \(1-D/q-o(1)\) of retained points. Thus the identities fail with vanishing probability as equalities in the vector space of degree-in-bound polynomials. Apply Lemma 59 in that vector-space alphabet, in mean over edges, and use zero on exceptional edges. Changing a vanishing fraction of mask tuples changes a vanishing fraction of point and line bits. We now have genuine polynomial slot families at every row, and their exact line restrictions.

Covariance and common systematic data. Test (147) on point symbols with independent uniform \(g,h,I\), uniform masks, and a bit form. Undo each row’s chart: \[F_{i,g}(I)=Y_{i,g}(g^{-1}I).\] If two such polynomial slot tuples differ, the discrepancy is seen with constant probability, first on a retained point, then by successive nonzero mask contractions, then by the bit form. Since \(g\) and \(gh\) are independent uniform elements, for each fixed label and track the squared frequencies of the uncharted tuples sum to \(1-o(1)\). Their maximum frequency is therefore \(1-o(1)\). Replace other rows by this predominant tuple, charted back. This changes vanishing point and line distance and enforces covariance exactly, including on lines.

Compare uncharted tuples of the finitely many systematic labels, using a shared uniform retained point and masks and independent row groups. The same constant gap forces an exactly common polynomial tuple \(F\) on all systematic labels of a track. Test that its contracted values lie in \(\mathbb{F}_q\) by a random binary form on \(J/\mathbb{F}_q\), pulled back to \(J\) and split. The quotient is an \(\mathbb{F}_q\)-space. If a polynomial coefficient were outside \(\mathbb{F}_q\), its quotient would be a nonzero vector polynomial and would have a constant detection gap. Consequently every systematic coefficient is in \(\mathbb{F}_q\).

Factoring through the target and enforcing parity. Choose uniform \(y\in K^u\) and two conditionally independent generic representations as in (150). Compare their values, with independent row groups. Each individual marginal is smooth; this test is a linear comparison and makes no product query on the correlated pair. For a slot coefficient the uncharted identity tested is \[ F(A,y-Az,z)=F(A',y-A'z',z'). \tag{151}\] The difference has coordinate degree at most \(2D\), and the full-rank restrictions omit an \(o(1)\) fraction. A failed polynomial identity therefore has constant detection probability, also after the bounded slot contractions. Hence (151) holds identically. Fix any full-rank \(A'\) and any \(z'\). Its right side defines a target polynomial \(f(y)\) of degree at most \(D\) with \(\mathbb{F}_q\) coefficients. Substitute \(y=Az+b\) to obtain the exact factorization \(F(P,z)=f(P(z))\).

Test the left and right star equations at uniform stars and retained points, with slot masks and random \(J\)-bit forms; pull row coefficients onto these forms. In an exactly covariant family, a failed polynomial star relation fails on every right-shift translate of that star, with an invertible affine change of argument. Polynomial, mask, and bit detection thus give a constant rejection gap for any failure. All star identities hold once the rejection is sufficiently small. Lemma 57 now forces the exact parity extension of the systematic target data and its line restrictions.

Product blocks. In each present \(Z\) block test additivity in \(Q\) and replace at vanishing cost by exact \(Q\)-linear maps, in mean over all its other indices. Sample a uniform independent pair of edge/point/slot-mask indices and uniform multipliers. Test the product identity for \(Q(x,x')=\alpha(x)\alpha'(x')\), with independent uniform binary forms \(\alpha,\alpha'\) on \(\mathbb{F}_q\). On the \(Z\) side split only \(Q\), keeping these already uniform other indices fixed. On each \(Y\) side pull the multiplier and \(\pi\) into the requested bit form and split that form. Compare with the Boolean product of the two resulting bits.

The \(Y\)’s are already genuine symbols. The difference between a wrong \(Q\)-linear map and their true product is a nonzero binary matrix. A uniform outer-product form detects it with probability at least \(1/4\), by two successive nonzero contractions. The fraction of wrong maps therefore tends to zero. Replace them by (149). This works separately for every compatible pair and never invokes a missing product block.

Algebraic validity. Finally run the algebraic validator of Lemma 55 on the recovered target polynomials, using systematic representations. Linear target probes need only their individual bounded-density marginal. For each product probe that lemma gives compatible tags and independent uniform full target arguments. Represent these independently in rectangular coordinates. The corresponding \(Z\) query therefore has the required joint density. Identity multipliers on \(\mathbb{F}_q\)-symbols and the demanded bilinear form implement the field-level product; split the necessary slot, form, and multiplier axes for its raw reads. The exact algebraic gap forces canonical extended validity. The native linear maps used by the validator, including coordinate packing, need not commute with the row action: they are used here only to specify systematic target arguments.

All replacements have vanishing total binary cost, so the original word is at vanishing distance from a canonical valid word. If the stated fixed-gap conclusion failed, for each integer \(j\) one could choose a size at least \(j\) and a word of distance at least \(a\) with rejection below \(1/j\), contradicting this sequence argument. Each constituent test is perfectly complete for every random choice in its support. All its raw marginals are smooth by the displayed representations and splitting; this also proves the claimed linear upper bound on rejection near a canonical word.

For distance, different logical tapes differ in an order-one grid polynomial. Its difference is nonzero on a constant fraction of uniform target arguments, hence on a constant fraction of systematic row/point positions; a bit form detects the symbol difference with probability \(1/2\). A concerned block has fixed positive weight. If the logical tape agrees, different valid extended labels differ in mode or in the progress marker, because legacy and mode fix the frame. These constant slot tensors likewise have a fixed nonzero-contraction gap. This gives a constant lower bound on relative distance. ◻

Proof. At a star decode to the unique local codeword within \(t_*-1=\lfloor c_e/2\rfloor\) errors, if it exists; otherwise output zero on that star. Distance \(c_e+1\) gives uniqueness. This decoder uses a bounded number of linear symbol operations and symbol-equality decisions: enumerate the information sets of size \(d_e-c_e\), solve using the complementary invertible minor, and count agreements with each candidate. There are constantly many such choices.

On a half-round mark a star bad if it meets at least \(t_*\) currently uncertain edges, and declare all edges incident to bad stars possibly uncertain afterward. Every other star decodes correctly, regardless of the values on uncertain edges. The first bad-star fraction is at most \(\zeta/\vartheta\le8\zeta\). If \(x\) and \(y\) are consecutive bad-star fractions on opposite sides, the new bad stars receive at least a \(\vartheta\) fraction of their incident edges from the preceding bad stars. Expander mixing with multiplicities gives \[ \vartheta y\le xy+\lambda\sqrt{xy}. \tag{152}\] When \(x\le\vartheta/2\), either \(y=0\), or division and squaring imply \[y\le(2\lambda/\vartheta)^2x\le x/16.\] Since \(8\zeta_*\le\vartheta/2\), induction applies at every subsequent half-round. The current edge-support fraction equals the latest bad-star fraction. A constant number of half-rounds therefore gives any prescribed fixed residual density. Every support operation used only sets of uncertain positions, proving the value-independent assertion. ◻

Proof. First-axis slices with uncertainty density greater than \(\zeta_*\) occupy at most a \(\zeta_*/4\) fraction. Keep these whole stripes uncertain. On all other slices use Lemma 61 to make residual density at most \(\delta_1\). In all but \(2\delta_1/\zeta_*\) of the second-axis slices, the additional residual outside these stripes has density at most \(\zeta_*/2\). Such a slice starts with uncertainty at most \(3\zeta_*/4<\zeta_*\). Contract it to \(\delta_2\), leaving all other second-axis slices uncertain. The final density is at most \[2\delta_1/\zeta_*+\delta_2,\] which is arbitrarily small. Intermediate arrays need not satisfy both slice constraints: each phase is compared to the fixed reference and uses its appropriate space structure only.

A fixed number of rounds and constant degree give a finite dependency cone. Extend any consistent assignment in that cone arbitrarily to the other uncertain initial positions, retaining the reference elsewhere. The global support statement applies to this extension and determines the same output. Separate cones may use different values on their uncertain inputs; no common assignment between cones is needed. ◻

Proof. Random-copy agreement and binary addition, or the two-axis binary tests, are perfectly complete. Lemma 59, together with the majority replacement of copies, gives a dimension- and copy-count-independent positive rejection lower bound \(\gamma_2\) at distance greater than a fixed \(\nu_2\) from every legal inner table. If this failed, a sequence of such tables with rejection tending to zero would contradict that lemma. Near a legal table, smoothness bounds rejection by \(C_2\) times distance, with an absolute \(C_2\). Choose \(\nu_1<\min(\nu_2,\gamma_2/(4C_2))\). Estimating rejection from independent trials and comparing with \(\gamma_2/2\) distinguishes the two promised cases with any fixed reliability; Chebyshev’s inequality suffices to choose a bounded sample count. The intermediate annulus may be assigned either flag.

Distinct Hadamard tables differ on half their forms. Distinct bilinear functions differ on at least a quarter of multiplier pairs. Repetition preserves these distances, proving uniqueness within \(\nu_2\). For a specified Hadamard form \(\mu\), choose uniform \(\alpha\), query random copies at \(\alpha\) and \(\mu+\alpha\), and XOR. Each query is uniform in its inner index, so one trial errs with probability at most \(2\nu_2\). For a bilinear table at specified \((b_1,b_2)\), choose independent uniform \(r_1,r_2\) and use \[\begin{align*} F(b_1,b_2)={}&F(r_1,r_2)+F(b_1+r_1,r_2)\\ &+F(r_1,b_2+r_2)+F(b_1+r_1,b_2+r_2). \end{align*}\] Each pair is jointly uniform, with a fresh random copy, and the error probability is at most \(4\nu_2<1/16\). Independent repetition and majority give any desired fixed error. These bounds hold for every specified bit, so remain valid after conditioning on all prior data if the splits and copies are fresh. ◻

Proof. List the cone’s initial positions and deduplicate repeated positions within that cone. Flag each distinct table once by Lemma 63, calling the far outcome flagged, and assign flagged positions the zero symbol. At an unflagged table within \(\nu_2\) of a legal table, assign its unique nearby symbol. Choose the flag reliability so that, except with a prescribed small probability, every table within \(\nu_1\) of its true symbol is unflagged and no table farther than \(\nu_2\) from all legal symbols is unflagged. On this event the assignment is well-defined and consistent inside the cone. Certain inputs receive their true symbols: a competing symbol within \(\nu_2\) would contradict inner distance. The remaining assignments, including arbitrary choices in the gap annulus, are permitted by Lemmas 61 and 62.

There is no need to recover the assigned symbols in full. Unfold the finite symbol-level decision tree for information-set decoding, agreement counts, and fallback-zero outcomes. On each fixed branch every candidate, comparison, and output is a linear expression in the assigned initial symbols. For two axes these expressions are sums of compositions of the two scalar actions (153). Their coefficients are obtained publicly from the fixed local matrices and the finite branch choices.

A false symbol equality is detected by a fresh uniform Hadamard form with probability \(1/2\), or by a fresh uniform multiplier pair with probability at least \(1/4\). Each resulting bit of a linear expression reduces, by additivity and scalar pullback, to a bounded number of specified bits of the initial assigned tables. Use Lemma 63 on unflagged inputs and public zero on flagged inputs. Independent equality trials make the chance of missing a false equality arbitrarily small; an exact equality fails only if one of its input-bit predictions fails. The requested final output bit is handled in the same manner.

The order of choices prevents circular error bookkeeping. First fix the row rounds and the complete finite symbol-level tree. Next choose flag and equality-detection budgets for its bounded number of possible decisions. This fixes the number of initial-bit predictions needed in each tested expression. Then choose their smaller error budgets and their repetitions. Given successful flags, every later specified bit has the uniform worst-request guarantee of the previous lemma conditional on prior answers, using fresh splits after all scalar pullbacks. A union bound, or conditioning successively on the preceding correct symbol-level decisions, bounds total simulation error by \(\sigma\). We do not choose the same budgets by union-bounding over the later amplified bit tree. After all choices that full tree is nevertheless finite and bounded. When a promise fails, the same finite comparisons and fallback-zero rules still define an output; only correctness is relinquished. ◻

Proof. Use the constants \(\nu_1,\nu_2\) already chosen, and put \(\zeta=\min(\zeta_*,\zeta_{**})\). Use the column and inner-table descriptions in Section 8.5: rows are edges for \(Y\) and edge pairs for \(Z\). Call an initial row position uncertain if its received inner table is more than \(\nu_1\) from its reference table.

Each block has error fraction at most \(b_\#\rho\). If \(u_{\rm unc}\) is the uncertain edge fraction in a uniform column, or pair fraction for \(Z\), then \[ \mathbb{E}u_{\rm unc}\le\frac{b_\#\rho}{\nu_1}. \tag{154}\] Call columns with \(u_{\rm unc}>\zeta\) bad. Their fraction is at most \(b_\#\rho/(\nu_1\zeta)\). On every other column, choose enough rounds in the support lemmas to leave uncertainty fraction at most \(\delta'>0\), whose value will be fixed later. No residual-support claim is made on bad columns.

For a \(Y\) request, independently split all its slot masks, including the line coefficient masks, and expand. Keep its specified Hadamard form as the inner bit request. For each expanded term choose independent uniform \(h\in\mathcal H\) and replace the row/outer pair by \[ (i,g,I)\longmapsto(i,gh,h^{-1}I). \tag{155}\] Covariance preserves the true value. For a \(Z\) request split both slot-mask lists and \(Q\), expand, and shift its two row/outer indices independently by (155). Keep the specified multipliers as its inner bit request. Let \(T_0\) be a fixed common upper bound on the expansion count, determined by the template, before any accuracy choices.

For each fixed original request, every term has a uniform column: the relevant \(\mathcal H\)-action is transitive and all its column-mask axes have been independently randomized. In \(Z\) the two independent shifts give the uniform pair of outer points. Choose the radius once and for all so that \[ \frac{T_0b_\#\rho}{\nu_1\zeta}\le\frac1{64}. \tag{156}\] Then, for every individual request, the chance that any term uses a bad column is at most \(1/64\). This conclusion does not assume that the shifted row is independent of the shifted outer point.

For every fixed shift, (155) is a permutation of the complete row/outer index; the independent pair of shifts is a permutation of the complete \(Z\) index. Thus averaging over an outer-density-\(C_{\rm req}\) request law preserves that density bound. Expanded column masks are uniform conditional on the indices. The mean chance of hitting the good-column residual support in any of the terms is consequently at most \(T_0C_{\rm req}\delta'\). By Markov’s inequality, outside an exceptional fraction at most \(8T_0C_{\rm req}\delta'\) of original requests, the conditional sum of those residual-hit probabilities is at most \(1/8\).

Bit-simulate every term’s row cone by Lemma 64, with total simulation error at most \(1/64\). On any nonexceptional request, the full randomized XOR trial therefore errs with probability at most \[\frac1{64}+\frac18+\frac1{64}=\frac5{32}<\frac14.\] Cone-specific assignments are sufficient because the support bounds cover every consistent assignment in each cone. Choose \(\delta'\) so that \(8T_0C_{\rm req}\delta'\le\eta/2\). This determines a constant row-round count. Repeat the entire trial independently at the fixed request, including shifts, flags, and all predictions, and take majority. A bounded number of repetitions makes its error at each nonexceptional request at most \(\eta/2\). Adding the exceptional fraction proves average error at most \(\eta\) from the fixed radius (156). This proves an average guarantee, and makes no assertion of arbitrarily accurate correction at every prescribed outer index. Smoothness is proved in the next lemma. ◻

Proof. First enumerate every potential initial row-cone path slot, including all candidate uses, before deduplication. A term’s initial covariance shift is the joint permutation (155). A fixed row-star path subsequently changes the edge label among finitely many possibilities and multiplies \(g\) on the left by a fixed group element. A right-star move from label \(i\) to \(j\), for example, uses \(g\mapsto u_j^{-1}u_i g\). Each such map is a permutation within a fixed edge-label class, so costs only a fixed label factor in a density bound. In a two-axis cone the same reasoning applies separately to each axis and preserves the joint pair bound. Consequently each enumerated path slot has a fixed density bound.

Deduplication, representative selection, and omission of unused terms only decide whether an already enumerated slot is read. Its resulting unconditioned subdistribution is dominated by the original slot distribution. We never condition and renormalize on the event that this slot was chosen as a representative or that its flag had a specified outcome. Summing the bounds of all potential slots, including unexecuted ones, bounds their complete occurrence count. A flagged, failed, or unused zero value is public zero and requires no placeholder query at a special address.

On a frozen symbolic branch, all information-set interpolation matrices depend only on \(H_L,H_R\) and public graph indices. The relevant inverses exist by their maximal-minor property. The coefficients of all selected linear expressions, including the compositions of (153), can therefore be computed publicly. Hidden work is only the bounded equality and output-bit calls described in Lemma 64. Their specified forms and multiplier pairs may depend on every frozen answer, public coefficient, and preceding random choice. Fresh splits after these pullbacks give uniform raw inner forms or jointly uniform multiplier pairs conditional on all that information. Zero coefficients can be split as well, or omitted. Fresh uniform copies give the required copy marginal. Wrong answers change the selected expression, but introduce no new type of row-cone path.

The tester’s schedules were explicitly smooth before replacements. The neighbor compositions below use finite lists of commuting affine column permutations and changes between fixed block types, so the same argument adds only fixed type factors. Dropping a public operand takes a marginal of a joint law, which also preserves a density bound. Finally freeze all simulation and amplification counts, unfold the full raw bit tree, and sum these finitely many bounds. This tree may be large, but is constant at the chosen accuracy. A later threshold offset that selects its branches changes neither its slot count nor these public address maps. The assertion concerns the unconditioned schedules for all branches, not correctness on unsuccessful branches. ◻

Proof. Reduce \(\rho\) if needed to lie below half the distance of Proposition 60; a nearby valid label is then unique. Use average correction at uniform systematic edge/point positions to read the mode and the needed critical-bit projections of Lemma 55. At full progress the all-ones contraction of the relevant singleton stack is a constant polynomial equal to its critical Boolean read. Use a specified additive form taking 1 to 1; its actual raw queries are smoothed by the corrector. Such uniform systematic requests have bounded outer density even though the logical read itself has a sparse public address.

Compare the progress marker with its public empty and full tensors by uniform separable masks and bit forms at systematic points. On the true constant tensors a false equality has a fixed gap by successive nonzero contractions. Corrected probes and sufficiently many repetitions distinguish these cases with arbitrary fixed reliability. Together with mode and the full-progress critical bits, including the wrap predicate, these are exactly the finite decisions required by the path transition rules. Explicitly, a pre successor increases progress unless full; at full it performs the enabled edit or has a missing wrap edge. A post successor decreases progress unless empty; at empty it advances the frame. For predecessors, full post reverses the edit or has the missing wrap edge, other post reverses a decrease, positive-progress pre reverses an increase, and empty pre reverses a frame advance. An increase also distinguishes empty progress for initialization. There is no scan of the full progress index and no proposed-tape validity test.

Fix the true Boolean transition branch of an existing edge. The algebraic interface expresses every updated contraction as a bounded sum of public terms and public scalar multiples of old contractions at invertible \(K\)-affine pullbacks of the common target. Slot pulls and scalars are independent of the target point and row. The pullbacks commute with the rectangular action, so they commute through the common row encoder as column permutations. Public initialization terms have publicly computable actual parity values. Thus each requested point \(Y\) bit is an XOR of boundedly many input \(Y\) requests with specified masks and forms at bounded-density indices. For line \(Y\), the affine map preserves the line parameter, so the identical argument applies to the separable coefficient contractions (148). The derivative update uses the separately stored child and its summed new-axis stack; it does not recompute native packing, polynomial division, or coefficient extraction from a requested line or parity symbol.

For a \(Z\) bit insert the two \(Y\) update sums into (149) and expand by bilinearity. Two variable terms give an available input \(Z\) block by tag compatibility; absorb public coefficients into multipliers or masks. The two row/point coordinates undergo separate affine column permutations, with their rows fixed. This preserves their joint density even when the two input types coincide: their two positions are still distinct coordinates of the product domain, never identified into a diagonal. A term with one public operand is an arbitrary specified binary linear form of the other \(J\)-symbol, and (157) gives the necessary complete surviving row/point bound. Here the public operand is its actual encoded \(J\)-symbol, including parity values, not an unencoded target value. Two public operands give a public bit.

Apply Proposition 65 to every needed term with a suitably smaller accuracy. Each output type and fixed branch has a bounded list of transformations, including radix pulls and zero terms. Charge their error and density bounds by their sum before selecting a term or branch. Charge the finite decision errors separately, and analyze each relevant correct branch with its true decisions fixed before intersecting the good events. Wrong decisions still select from the same public lists; missing or unused values are public zero. Therefore the all-hypothetical-branch smoothness assertion follows from Lemma 66. ◻

Proof. At every systematic edge/point position in the port’s order-one point block, read the entire Hadamard table including copies and choose a nearest \(J\)-symbol, breaking ties publicly. Whenever the table error is less than \(1/4\), the selected symbol is true. Markov’s inequality bounds the fraction of incorrect systematic symbols by a fixed multiple of balanced word error, accounting for the block weight and the systematic row fraction.

Map these symbols to their represented target arguments using the known row action. All fibers have equal size: for a fixed target \(y\), any full-rank \(A\) and any \(z\) determine the unique offset \(y-Az\), and the number of choices is the same for every row group. Take a plurality in each fiber. Every wrong plurality requires at least half its fiber’s symbols to be wrong, so this loses at most a factor two. Project outputs outside the subfield to any fixed \(\mathbb{F}_q\)-estimate, which cannot spoil a correct symbol, and take another plurality over ignored target coordinates. After reducing the fixed radius, we have an estimate \(\widehat f:\mathbb{F}_q^\ell\to\mathbb{F}_q\) of the native order-one polynomial with symbol error at most a sufficiently small fixed \(\alpha>0\).

For each desired grid point \(x\), enumerate all directions \(z\in\mathbb{F}_q^\ell\). Along the \(q\)-word \((\widehat f(x+tz))_{t\in\mathbb{F}_q}\), the expected number of errors over \(z\) is at most \(1+(q-1)\alpha\): every nonzero \(t\) makes \(x+tz\) uniform. Let \[t_{\rm RS}=\left\lfloor\frac{q-D-1}{2}\right\rfloor.\] For sufficiently small fixed \(\alpha\) and large size, Markov’s inequality shows that a strict majority of directions have at most \(t_{\rm RS}\) errors, since \(D/q\to0\).

Use the Berlekamp–Welch reconstruction method in the linear-system presentation of Gemmell and Sudan (Gemmell and Sudan 1992, Appendix A). Specifically, uniquely decode each line by solving the linear equations \[N(t)=E(t)\widehat f(x+tz)\quad(t\in\mathbb{F}_q),\qquad E\text{ monic of degree }t_{\rm RS},\quad \deg N\le D+t_{\rm RS}.\] On a good direction, the error locator, padded by any monic factor to degree \(t_{\rm RS}\), provides a solution with \(N=Ef_{\rm line}\). Every solution has this equality: the difference \(N-Ef_{\rm line}\) has degree at most \(D+t_{\rm RS}\) and vanishes at at least \(q-t_{\rm RS}>D+t_{\rm RS}\) correct positions. Divide, verify degree and agreement, and use public zero on a failure. The strict majority of returned values at parameter zero is exactly \(f(x)\). Repeat for all port grid indices. All domains, tables, directions, fields, and linear systems here are polynomial-size, so the complete algorithm is deterministic polynomial time. ◻

Proof. The construction and the preceding propositions prove (i)–(iv) and global recovery. For (v), field and row-code choices were made solely from the common point parameters. The positive charts, including per-primary verification auxiliaries and their tagged descendants, have the literal common-index ancestry of Lemma 55. Columnwise linear extension and fixed-parameter line restriction preserve that identity. Passing through an original index and choosing a fresh copy therefore suffices even when balanced multiplicities differ.

At either of the two specified fixed labels, legacy, work, frame, mode, and progress are public, and every positive persistent recipe has Boolean degree at most three in its port input. Public matrix operations, division by fixed monic polynomials, coefficient extraction, slot contraction, fixed affine substitutions, line restriction, \(J\)-linear row extension, coordinate changes, and additive bit forms are all \(\mathbb{F}_2\)-linear in these hidden-data functions. None raises that degree. The one additional binary bilinear operation in (149) gives degree at most six. Finally (156) uses only the template’s \(T_0,b_\#,\nu_1,\zeta\); the later requested density and accuracy affect only row rounds and repetitions. Applying it first to the fixed one-port template proves the last assertion. ◻

Proof. The inner distance assertion applies separately to each half. Distinct inputs give distinct labels already in the order-one input track, so it gives the claimed distance for their concatenation.

For testing, mix the ordinary valid-label testers on the two halves with the following additional checks. At systematic point probes compare the legacy chart with the public stage-zero polynomial, the mode with post, and the progress marker with its specified one-hot tensor, using the source or successor progress value as appropriate. Uniform slot masks and additive binary forms give smooth bit versions of these checks; a specified form can also be split into fresh uniform summands. On exact valid labels, an incorrect location condition has a fixed positive rejection gap by the low-degree or constant-tensor distance. Correct conditions force the blank-work tape, the specified progress and mode, and frame \(\gamma^{-1}\). Finally compare the two order-one input point tracks at identical original systematic edge/point indices and identical uniform bit forms, choosing copies independently in the two halves. Different inputs give a fixed positive discrepancy gap. The two reads have smooth marginals individually; they do not require a product block. Each mixture weight is a fixed positive constant.

Here is the fixed-gap implication explicitly. Let \(g>0\) be a common lower bound for the rejection of any violated location or equality requirement on exact pairs of valid labels, with the mixture weights included. Let \(C\) bound the change in these tests’ rejection under changes to a fraction of the whole port. Given \(a>0\), choose \[0<a_0<\min\{a,g/(4C)\}.\] Ordinary soundness supplies a positive rejection threshold forcing each half within \(a_0\) of an exact valid label. Take the total tester threshold small enough to imply both of these assertions and also smaller than \(g/2\). The pair of nearby exact labels is at distance less than \(a_0\) from the received port. If any required exact condition were wrong, smoothness would make the received rejection at least \(g-Ca_0>g/2\), a contradiction. Thus the exact pair is precisely \(\mathcal D(s)\) and the received distance is less than \(a\). This defines \(\theta_B(a)\). Perfect completeness and the upper bound \(C_Ba\) follow by charging every read whose answer differs from the exact port word. All choices and computations have the bounded, polynomially enumerable properties asserted in the two inner interfaces.

At the two fixed labels all logical inputs except \(s\) are public. Canonical persistent values and their coordinate coefficients have logical degree at most three, even on invalid Boolean tapes. Their verification certificates use public linear maps on one primary array: multiplication by the public test matrix, summation, division by a public monic polynomial, coefficient extraction, and interpolation. These operations preserve degree. Fixed-progress stack formation, restriction to a point or a line, line-coefficient extraction, slot contraction, row extension, and additive bit forms are linear over the prime field. Thus a \(Y\) bit has degree at most three. A \(Z\) bit is a binary bilinear form of two such operands and has degree at most six. Repeating bits for balance changes nothing. The degree bound is independent of the allowance and of all future template choices.

For completeness, the coefficient algorithm need not manipulate a large symbolic expression. For a specified bit function \(b\), evaluate the canonical dummy word on \(1_T\) for all \(T\subseteq[L]\) with \(|T|\le6\). Its coefficient at the squarefree monomial indexed by \(A\) is \[c_A=\sum_{T\subseteq A}b(1_T)\quad\text{in }\mathbb{F}_2, \qquad |A|\le6.\] Boolean multilinear inversion and the degree bound give every coefficient; there are \(O((L+1)^6)\) evaluations, each polynomial-time.

Use the deterministic order-one recovery from Lemma 69 on the first half. A port error fraction \(r\) causes an error fraction at most \(2r\) there, so a fixed sufficiently small \(r\) gives exact recovery of \(s\). Finally choose \(\nu_B<d_{\mathcal D}/4\) with \(2\nu_B\) inside the dummy average-correction radius and, if necessary, the just established recovery radius. A port within \(\nu_B\) corrupts either half by at most \(2\nu_B\). The dummy corrector therefore answers the stated requests from that half; its read density relative to the whole port loses only a factor two. Its radius is independent of the requested accuracy and density constant. Every constant used here belongs to the one-port template. ◻

Proof. Apply Lemma 54 at the two labels in (106). Both have frame \(\gamma^{-1}\), blank work, stage-zero legacy, and post mode; their progresses are respectively \(q-1\) and \(q-2\). At either progress the lemma identifies each positive algebraic array with its one-port counterpart at the same native point, slot, and mask indices. This includes verification auxiliaries and all derivative descendants: Lemma 47 fixes their separate call layouts independently of work destinations, the number of ports, and the actual circuit. The placements and fixed-progress stack formulas are common as well.

The common row field, row matrices, systematic extension, and point/line domains were fixed before \(k\). Applying these same linear operations preserves the equality at the original encoded indices, for the source and its first decrement separately. The actual template may balance its block types with different copy counts. Forgetting its copy index and choosing a fresh uniformly random dummy copy preserves the original index and costs only the fixed actual block-weight factor.

The same source-data lemma makes every tag-zero array public at these labels. Its conclusion includes derivatives evaluated on public shifted work, even when the shifted Boolean tape is invalid: canonical certificate recipes are defined there and do not solve a final validity equation. Thus no work-side certificate needs to evaluate \(f(s)\) or a stored sum with a port-dependent primary. The actual encoded \(J\)-symbols of these public arrays, including their parity values, are computed with the actual template’s common row encoder.

The only remaining case is a product with tags \((i,0)\) or \((0,i)\). Write \(x\) for the positive operand’s entire original edge/point index and \(z\) for the public operand’s entire index. After the indicated contractions and public scalar multipliers its bit is, in one orientation, \[ Q\bigl(\pi(b_i u(x)),\pi(b_0 v_{\rm pub}(z))\bigr) =\mu_{z,b_i,b_0,Q}\bigl(u(x)\bigr), \tag{160}\] where \(\mu_{z,b_i,b_0,Q}\) is a specified additive binary form. The dummy \(Y\) corrector permits precisely such arbitrary forms, including dependence on both requested positions and all the public coefficients. It retains \(x\) at the same original index. If the request law satisfies \[p(x,z)\le\frac{C}{|\mathcal X|\,|\mathcal Z|}, \qquad\text{then}\qquad \sum_zp(x,z)\le\frac{C}{|\mathcal X|}.\] This proves the required density for the dummy \(Y\) request on both its edge and its point. A same-positive-tag \(Z\) request retains both original indices and their joint density; even when its types coincide, no pair is replaced by a diagonal. A \((0,0)\) product is public. There are no products of two distinct positive tags. Proposition 70 now supplies all the answers. Fixing a source/successor choice, orientation, or block type costs a fixed factor. All error and density bounds are summed before any later answer-dependent selection; no density bound is conditioned on that selection. ◻

Proof. Choose \(\rho_{\rm in}\) within the whole-word uniqueness and actual-template correction radii. Estimate rejection of the ordinary tester for the union of all port tuples. For each port \(i\), also sample the order-one point track \(W_{s_i}\) of \(z\) at uniform systematic original edge/point indices and uniform forms, and compare it with the bit at the identical original index of the corrected dummy source half of \(y_i\). Choose a random actual copy for the direct read. This input track is unrotating and uses the same extension at every actual path label.

On an exact valid label the ideal mismatch is zero if its \(i\)th port is \(s_i\), and at least a constant \(p_s>0\) otherwise: the nonzero order-one polynomial differs on a constant fraction of represented arguments, and a uniform additive form detects a nonzero difference with probability \(1/2\). We can choose one \(p_s\) for the fixed templates. A balanced error fraction \(a'\) in \(z\) changes a comparison rate by at most \(C'_k a'\), where \(C'_k\) includes the systematic and block-weight density factors. Choose \[0<a'<\rho_{\rm in},\qquad C'_k a'<p_s/8.\] Use half the ordinary soundness threshold for \(a'\) as the rejection cutoff, and \(p_s/2\) as each mismatch cutoff. Good statistics with fixed positive slack imply that an accepted seed is \(a'\)-close to an exact valid label. The mismatch gap then forces every port of that label to be \(s_i\). Conversely, smoothness of the ordinary tester and of the comparison probes makes all rates lie strictly below their cutoffs when the seed is within a sufficiently small fixed \(\rho_{\rm in,comp}>0\) of a true-path label.

First fix sample counts that concentrate the underlying ideal rates at the required slack; independent samples and Chebyshev’s inequality suffice. Next choose the dummy correction accuracy so that the bounded number of supplied comparison bits fail with the desired total probability. This order leaves \(a'\), \(\rho_{\rm in,comp}\), and \(\nu_B\) unchanged. On good acceptance, the ordinary correction and neighbor procedures of Lemma 69 apply to the fixed unique reference. They return the true incident flags, including the disabled wrap flag, and true encoding bits at existing neighbors with arbitrary average accuracy. Analyze each possible reference of the fixed seed before intersecting with acceptance; one never conditions a smoothness estimate on that event. On unsuccessful branches every routine still has a bounded Boolean output or a fixed default. ◻

Proof. For binary words \(a,b,c\) and \(0\le s\le1\), \[ \lVert (1-s)a+sb-c\rVert\ge\min(s,1-s)\lVert a-b\rVert. \tag{190}\] Indeed on a coordinate where \(a,b\) differ, the chord coordinate is \(s\) or \(1-s\), whose distance from a binary coordinate is at least \(\min(s,1-s)\). Summing squares proves the claim. In particular, a point on this chord within distance \(z\) of a binary word is within distance \(z\) of one of the chord endpoints.

Consider first segments varying the same block. If their distance is less than \(d_*\), all fixed encoding blocks and repeated binary levels agree. For block \(2\), the tail agrees and determines the outgoing edge. For block \(1\), the head agrees and determines the incoming edge. For block \(3\), an upward segment has a fixed unequal pair \((E_u,E_v)\), whereas a downward segment has an equal pair \((E_v,E_v)\); the two types cannot have the same fixed pair. Within either type that pair determines the segment, using uniqueness of the incoming edge for the downward type. There is only one block-\(4\) segment.

For two segments varying different blocks, choose points at distance \(z\). Each varying block of a horizontal segment is within distance \(z\) of a fixed binary block of the other. By (190), its point is within distance \(z\) of an endpoint of its original segment. For the special vertical, its distance from a horizontal segment forces its height to be at most \(z\), so it is within \(z\) of its bottom. The two selected endpoints are therefore within \(3z\). Distinct original endpoints are separated by at least \(d_*\): one of their encoding blocks, binary third levels, or vertical levels differs. Taking \(3z<d_*\) forces the endpoints to coincide.

An unequal ordered pair \((E_u,E_v)\) occurs at the two internal toggle corners of its own edge only, with the third level distinguishing them. An endpoint \((E_v,E_v,1,0)\) belongs to the last internal corner of the unique incoming edge. An endpoint \((E_v,E_v,0,0)\) belongs to at most the incoming final segment and the outgoing first segment. If both exist, they are consecutive. At \(w_*\) there is no incoming graph edge, and the special bottom takes exactly that role. The top belongs only to the special vertical. Thus equality of endpoints of distinct segments implies consecutiveness. For example \(d_{\rm sep}=d_*/4\) is sufficient for the asserted strict-distance argument. The adjacency components are paths and cycles; any cycle contains at least eight segments because the graph has no self-edge. Adding a segment at a path beginning creates no triangle. ◻

Proof. Support a straight point by its original segment, and an arc point by the two segments of its corner. An arc point is within \(a_0\) of each supporting segment. Choose \(\rho_{\rm loc}+2a_0<d_{\rm sep}\). Every across-point pair of supports is then identical or consecutive. Each point’s support set is itself a clique, so their union is a clique and contains at most two segments by Lemma 74. In the one-segment case both points lie on its retained straight. In the two-segment case they lie on the two retained straights and their shared fillet. Opposite-end trims are disjoint by (191). This also rules out unintended identifications or intersections.

Along a two-direction chain, all tangent coefficients in its orthogonal directions \(u_0,v_0\) are nonnegative, and \(\langle T,u_0+v_0\rangle\ge1\). Integrating in the directed order gives \(\Delta\le\langle Z'-Z,u_0+v_0\rangle\le\sqrt2\lVert Z'-Z\rVert\). Reverse the order if necessary. A straight chain has equality between length and endpoint distance.

Compactness gives a minimizer. The endpoint assumption makes every minimizer interior, so differentiating squared distance along its \(C^1\) path gives the asserted perpendicularity. A competitor of the stated excess satisfies \[\lVert Z'-Z\rVert\le4\tau+\sqrt{17}\tau<9\tau.\] Require \(9\tau<\rho_{\rm loc}\). The local chain then has \(|s'|<13\tau\), and integration of (195) gives \[Z'-Z=s'T(Z)+R,\qquad \lVert R\rVert\le(s')^2/(2a_0).\] For \(|s'|/(2a_0)<1\), expansion of squared distance and perpendicularity therefore imply \[\begin{align*} g&=\lVert Z'-Z\rVert^2-2\langle X-Z,Z'-Z\rangle\\ &\ge(s')^2\left[ \left(1-\frac{|s'|}{2a_0}\right)^2-\frac r{a_0}\right] \ge(s')^2/2, \end{align*}\] where, for example, \(\tau/a_0\le1/64\) makes the last inequality hold. Applying this to a second minimizer proves uniqueness. Integrating the unit tangent, its infinity bound, and its two Lipschitz bounds over length \(|s'|\le\sqrt{2g}\) proves (198) and (199). All estimates are independent of \(m\). ◻

Proof. Every nonvertical piece, including the bottom fillet, has fourth height at most \(a_0<1/10\). Its distance to a point in the slab exceeds \(3/10\), by the mean inequality \(\lVert X_4-z\mathbf 1\rVert\ge|\mu-z|\). It cannot be in the \(4\tau\) tube. The retained vertical contains all heights of this slab, and \[m^{-1}\sum_j((X_4)_j-t)^2 =m^{-1}\sum_j((X_4)_j-\mu)^2+(t-\mu)^2\] shows that its nearest line point is \(Z_\mu\). For \(T=-\mathbf e\), the last annulus of (202) is already identically \(\mathbf e\) at every \(r\ge2\tau\). Consequently the same equality holds even where the closest curve piece is far away and the inside field is default. The desired endpoints have fourth height zero and the top has height two, so neither endpoint exception occurs in the slab. Each coordinate of \(Z_\mu-X\) has magnitude at most three and its norm is at most six. Multiplication by \(h_\mu\le2|\mu-1/2|\) proves both bounds. ◻

Proof of the displacement assertion in Theorem 73. Choose \(\beta_0>0\) satisfying all the upper bounds on \(\beta\) used below.

Inside the tube and in the inside default region. First suppose \(\mu\le1/2\) and \(r=\mathop{\mathrm{dist}}(X,\mathcal L)\le3\tau\). For \(r\le\tau\) the raw field is the convex combination of \(T\) and the inward unit normal with coefficients \(1-r/\tau,r/\tau\). For \(\tau\le r\le2\tau\) it is the convex combination of \(-T\) and the inward unit normal with coefficients \(r/\tau-1,2-r/\tau\). The two directions in each combination are orthogonal. At \(r=0\) the field is \(T\). In the third annulus the two unit directions are \(-T,\mathbf e\), whose inner product is nonnegative. Therefore in all three annuli \(\lVert v(X)\rVert\ge1/\sqrt2\).

Write \(v=b+w(Z-X)\), where \(\lVert b\rVert_\infty\le C_t+1\) and \(0\le w\le1/\tau\). All coordinates of \(Z\) lie in \([0,1]\): for a vertical projection its height is at most \(\mu+3\tau<1\), and all other pieces already have this property. Require \(\beta/\tau\le1/2\) and \(\beta(C_t+1)\le1/4\). The preliminary point \(Y=X+\beta w(Z-X)\) lies in the box. If \(|X_i-Z_i|<1/2\), then \(-1/2<Y_i<3/2\), and the additional displacement \(\beta b_i\) causes no clipping. The number of remaining coordinates, divided by \(m\), is at most \(4r^2\le36\tau^2\). At each, the clipping loss is at most \(\beta(C_t+1)\) because \(Y\) was in the box. The norm of all loss is at most \(6\tau\beta(C_t+1)\le\beta/4\). Subtracting it from the raw displacement leaves at least \(\beta/4\).

In the inside default case, let \(p\) be the fraction of fourth coordinates at most \(7/4\). Since all entries are at least \(-1\), \[1/2\ge\mu\ge-p+(7/4)(1-p),\qquad p\ge5/11.\] For \(\beta\le1/4\) these coordinates retain the full upward displacement, giving norm at least \(\beta\sqrt{5/11}\).

Above the mean interface. Now suppose \(\mu\ge1/2\), and abbreviate \(Z=Z_\mu\), \(r=r_\mu\). The fourth coordinates of \(Z-X\) have mean zero, so they are orthogonal to \(\mathbf e\). Write \(v=b\mathbf e+w(Z-X)\), with the scalar table \[ \begin{array}{c|cc} \text{radius}&b&w\\\hline 0\le r\le\tau&-1+r/\tau&1/\tau+h_\mu\\ \tau\le r\le2\tau&r/\tau-1&2/r-1/\tau+h_\mu\\ r\ge2\tau&1&h_\mu \end{array} \tag{204}\] and hence \[ |b|\le1,\quad0\le w\le w_{\max}:=1/\tau+1, \quad b^2+w^2r^2\ge1/2. \tag{205}\] The last assertion follows from the two orthogonal components of the first two radial regimes; adding \(h_\mu\) increases the nonnegative normal coefficient. In the last regime \(b=1\). Require \(\beta w_{\max}\le1/2\). The move toward \(Z\) is a convex move inside the box, and horizontal coordinates undergo no further move or clipping.

If \(b<0\), then \(r<\tau\). The subsequent downward step cannot clip at the upper boundary. Where \(|(X_4)_j-\mu|<1/2\), the preliminary fourth coordinate is nonnegative since \(\mu\ge1/2\), and the following step is at least \(-\beta\ge-1\). Thus lower clipping can occur only on a fraction at most \(4\tau^2\) of the fourth coordinates. Its loss on each is at most \(\beta\), giving norm loss at most \(2\tau\beta\). By (205) this leaves at least \(\beta/4\).

It remains to treat \(b\ge0\). Set \[\sigma^2=m^{-1}\sum_j((X_4)_j-\mu)^2,\qquad H=\lVert (X-Z)_{1,2,3}\rVert,\qquad r^2=H^2+\sigma^2,\] and choose a positive rational \[ \eta\le\min\left\{\frac\tau2,\frac1{4w_{\max}}, \frac12\min\left(\frac12,\frac1{4w_{\max}}\right)\right\}. \tag{206}\] If \(\sigma\ge\eta\), a uniform fourth coordinate satisfies \[\sigma^2\le3\mathbb{E}|(X_4)_j-\mu| =6\mathbb{E}(\mu-(X_4)_j)_+.\] Put \(c=\eta^2/12\). Since the positive part is at most three, \(\mathbb{E}(\mu-(X_4)_j)_+\ge\eta^2/6\) implies that a fraction at least \(\eta^2/36\) have \(\mu-(X_4)_j\ge c\): otherwise its expectation would be less than \(c+3\eta^2/36=\eta^2/6\). On those coordinates the room to the upper boundary is at least \(c\). Also \(b+wc\ge c/12\). Indeed (205) and \(r\le6\) imply that either \(b\ge1/2\) or \(w\ge1/12\); \(c<1\) handles the first alternative. For \(\beta\le1\), clipping therefore retains displacement at least \(\beta c/12\) on that fraction. Its norm is at least \(\beta\eta^3/864\).

Suppose instead \(\sigma<\eta\). If \(wH\ge\tau/4\), the horizontal displacement, which is not clipped, is at least \(\beta\tau/4\). Otherwise (205) gives \[b^2\ge\frac12-w^2H^2-w^2\sigma^2 \ge\frac12-\frac{\tau^2}{16}-w_{\max}^2\eta^2 \ge\frac38,\] so \(b\ge1/2\). If \(\mu\le1\), let \(d_0=\min\{1/2,1/(4w_{\max})\}\). By (206), at least three quarters of the fourth coordinates have deviation from \(\mu\) at most \(d_0\). Their upper room is at least \(1/2\), and their velocity is at least \(b-w_{\max}d_0\ge1/4\). They retain at least \(\beta/4\) for \(\beta\le1\), giving norm at least \(\sqrt3\beta/8>\beta/8\). If \(\mu>1\), then \(h_\mu=1\), \(w\ge1\), and \(b\ge0\) in (204) requires \(r\ge\tau\). It follows that \[wH\ge H\ge\sqrt{\tau^2-\eta^2}\ge\sqrt3\tau/2,\] contrary to the remaining case assumption. This exhausts all outside points, including the upper face. At \((H_*,2)\), \(r=0\) and the formula gives \(v=-\mathbf e\) exactly.

Take positive rational \(c_*\le\min\{1/8,\tau/4,\eta^3/864\}\) and positive rational \(\beta_0\) satisfying all restrictions just made. All coordinate differences used in the formulas have magnitude at most three, so any integer \(B_1\ge C_t+6+3/\tau\) satisfies (187), including the zero convention near inside endpoints. These choices depend only on the previously fixed geometric constants. This completes the proof of Theorem 73. ◻

Proof. For \(u\to v\), its first segment, first fillet, and upward toggle have first block \(E_u\). The fillet from that toggle to the block-\(1\) segment, the block-\(1\) segment, and its fillet to the downward toggle have second block \(E_v\). The downward toggle has both blocks \(E_v\). An ordinary graph-junction fillet at \(u\) changes only blocks \(3\) and \(2\), so its first block is \(E_u\). In each case the stated vertex generates the piece from its incident data. If the piece is within \(4\tau\) of \(X\), its fixed block is within \(4\tau\) of the corresponding physical block. Part [geo:access-validation] of the contract therefore accepts that seed with its true reference. Correct flags include the piece. The two special pieces are included unconditionally. Gray acceptance cannot remove a piece required by this argument; it can only add or remove other actual pieces. ◻

Proof. For the inside prescription, consider the selected mesh entry. Let \(z>0\) bound every squared-distance error, including the parameter, bit, quantization, and scalar-statistic errors just discussed. Suppose first that \(r=\mathop{\mathrm{dist}}(X,\mathcal L)\le3\tau\). By Lemma 81, a minimizing piece is present. A mesh point at arclength at most \(D\) from its projection has squared excess at most \(2rD+D^2\). Every admitted exact entry is on the actual curve, so none has negative excess. The exact point \(Z'\) underlying the approximate winner therefore has \[ 0\le g=\lVert X-Z'\rVert^2-r^2\le2rD+D^2+2z. \tag{211}\] Choose \(D,z\) first small enough that the right side is at most \(\tau^2\), and then still smaller as required. Equations (198)–(199) show that both its point and tangent approach those of the true projection in infinity norm, uniformly. Correct endpoint bits at the final matching coordinate also make its computed point and tangent close to their exact values. Clamping a squared-radius estimate at zero and taking square root is uniformly continuous on the fixed bounded interval. Consequently its estimated radius approaches \(r\).

Each component of (202) is a bounded continuous expression in that radius, the tangent component, and the components of \(Z-X\). The formulas match at \(\tau,2\tau,3\tau\), and the only reciprocal radius is protected by \(r\ge\tau\) in its regime. Safe clamping can be used at approximate regime boundaries. Uniform continuity on these fixed compact ranges proves the desired component error. Crucially, the infinity-norm bounds hold for every good candidate satisfying (211); they therefore also hold when the chosen candidate is correlated with the requested coordinate.

If the true inside radius is \(r>3\tau\), the true field is default. Every actual candidate entry has distance at least \(r\). Good squared distance estimates can yield a nondefault computed expression only arbitrarily near the \(3\tau\) cutoff as \(z\) tends to zero. Near that cutoff the coefficient of \(T\) tends to zero and the coefficient of \(\mathbf e\) tends to one, uniformly on the clamped coordinate ranges. Thus the computed value approaches default. If its radius estimate is at least \(3\tau\), it is already default. Coverage far from the curve is not needed in either case.

For the outside prescription, use the special bits, the estimated mean and outside squared radius in (203). Correct special matching bits and good statistics make all its scalar and coordinate arguments close to their exact values. The same protected denominators and compact-range continuity apply, and \(h_\mu\) is continuous. This includes the special top, where the exact value is \(-\mathbf e\).

Finally consider the choice between the inside and outside computations. If it differs from the side of the true mean, a good estimate forces \(|\mu-1/2|\) to be small. In the interface slab all endpoints remain far, and the only possible close piece is the always included vertical. The inside computation is therefore valid for the inside prescription extended to that slab. The outside computation is valid for its extension using the clamped \(h_\mu\). By Lemma 77, the two target values differ componentwise by at most \(6|\mu-1/2|\). Adding that error proves stability even with the wrong side choice. These cases include exact mean, radius, and minimum ties, without requiring a reliable hidden-real comparison at zero gap. ◻

Proof of Lemma 80. Oracle accuracy with fixed references. Fix a desired \(a>0\). Choose a component error \(e>0\) and failure budget \(p>0\) so that \[ 4e^2+16B_1^2p<a^2. \tag{212}\] First choose the mesh, scalar tolerances, quantization width, and public numerical precision for Lemma 82, with slack for final output rounding. Fix scalar sample counts that give its concentration events a total failure probability below a chosen part of \(p\). The eight word roles, 32 piece roles, five possible length statistics, mean, mesh-distance statistics, and outside-radius statistic now determine a fixed number \(N_{\rm call}\) of high-level completed calls. This count includes all sampled bit requests and all matching final bit requests over the possible relevant true references and flag alternatives.

Make validation and edge-flag errors small enough for their total budget. For every remaining high-level bit call require average error smaller than the allocated part of \(p/N_{\rm call}\). Analyze each call on its possible fixed reference before conditioning on acceptance or on the numerical winner. Parts [geo:access-validation]–[geo:access-statistics] of the access contract and a union bound then charge the event of any required bit, decision, or statistical error by at most \(p\). Independence of these events is unnecessary. A fixed reference does not have to be selected on every good trial; the unconditioned analysis simply pays for its possible calls in advance. Validation failures, including any acceptance with no proper reference, are charged separately. The two special-word roles are charged in exactly the same way when their supply is virtual.

On the complement of the charged failure event, component error is at most \(e\) by Lemma 82 and the planned final rounding. On every outcome clamp the numerical answer to \([-B_1,B_1]\) and round to a sufficiently fine fixed dyadic grid there. Detected invalid numerical inputs may return any fixed bounded default. Undetected incorrect choices are already included in the failure event. The true field satisfies (187), so the component error on an arbitrary outcome is at most \(2B_1\). Hence \[4\mathbb{E}|\widehat v_I(X)-v_I(X)|^2 \le4e^2+16B_1^2p<a^2.\] This proves (208) unconditionally over the output-coordinate and trial law. It does not assert correctness conditioned on a rare selected coordinate or branch. The proof began with arbitrary fixed admissible offsets, so it applies to each such pair, and therefore also after averaging any chosen laws on them.

Finite oracle implementation. Here are the finite implementation and raw-address details. Fix a small rational bin width \(h>0\) and compare each physical scalar read to thresholds \(a+kh+\zeta\) on a fixed interval larger than \([-1,2]\), where \(\zeta\) is an offset modulo \(h\). Clamp at the endpoints. Representatives can depend just on the bin number, on a fixed rational grid, and are within \(O(h)\) of the input for every \(\zeta\). This error was included in the earlier tolerance choice. Comparisons whose answers are forced by the allowed physical range can be public. Seed bits use the common threshold \(\xi\). Each offset may eventually range over a fine finite rational grid. No numerical assertion above requires a continuous offset distribution.

There are now only finitely many bits and bin indices in the geometric computation. Public rational approximations to the fixed mesh sine and cosine values, protected length normalizations, clamped square roots, and all other numerical expressions can be tabulated to the chosen precision. Bounded Boolean lookup implements the resulting answer function. In particular neither an exact curve minimum nor an unbounded hidden vertex name or transcript is processed by the local Boolean computation. Public index arithmetic and any caller-specific field or interpolation calculations are performed when constructing the corresponding fixed branch and its wiring.

Wrong validation, flag, or type answers can invoke a reserved symbolic routine on an unsuitable seed or select another reserved role. Wrong length, radius, side, or minimum answers select a fixed mesh or lookup case. None of these answers supplies a new word-coordinate address: statistical coordinates remain the preallocated coordinates and final data remain at \(J\). Inactive or nonsensical roles may use public-zero defaults, which require no query to a distinguished physical position. Consequently direct scalar reads have the matching or prescribed statistical marginals on every fixed hypothetical oracle branch. This proves the structural assertion of part (iii), without inspecting the physical realization of a supplied oracle answer. A constant number of choices from polynomially enumerable oracle-level public spaces has polynomial support; a constant product of rational probabilities of polynomial bit complexity has polynomial bit complexity. Public indices, oracle descriptions, and bounded answer tables retain the same polynomial construction bound. This proves the oracle-level enumerability assertion of part (iii).

Physical read load under the additional hypothesis. For part (iv), now assume the additional physical-read hypothesis [geo:access-finite]. The supplied routines then have its all-branch primitive bounds, even on unsuitable seeds.

Only at this point, after all requested accuracies and the repetitions implementing them have been fixed, unfold the full lower-level answer tree. Give unused possible nodes their prescribed public random choices as well. It has a fixed finite number \(H\) of potential primitive slots. For a domain of size \(M\), let \(C_\ell/M\) bound the probability that slot \(\ell\) reads any specified position, for its fixed symbolic branch under the unconditioned public law. A slot not using this domain has \(C_\ell=0\). Summing gives \[ \mathbb{E}_{I,\,\mathrm{trial}} [\text{number of potential reads of position }j] \le\frac{\sum_{\ell=1}^H C_\ell}{M} =\frac C M. \tag{213}\] This counts all wired possibilities rather than conditioning on the executed path. Omitting an inactive occurrence only reduces its unconditioned mass. In particular this argument does not require accuracy on wrong branches. The high-level count \(N_{\rm call}\) used for the correctness union bound preceded amplification; the larger count \(H\) is used for raw load and subsequent gate-failure accounting. It is not fed back into the choice of the accuracy that determines \(H\).

Refining offset grids changes the values of thresholds for a fixed finite set of comparisons. It changes neither the bin width and bin count, nor the mesh, nor the symbolic answer-tree slots, nor a fixed branch’s address primitive. Thus \(H\) and \(C\) remain uniform under that refinement. Under the stated polynomial enumerability premise for the physical routines, a constant number of their public choices, also at unused tree nodes, again has polynomial support and rational-probability bit complexity. Their public addresses and bounded answer tables are constructed in polynomial time. This proves the physical enumerability assertion of part (iv) and completes the proof. ◻

Proof. Let \(\varepsilon_c,\delta_c\) be the constants in Theorem 3, and let \(G=(V,T)=R(I)\).

Removing Boolean gates. First give every used node a defining gate, if necessary. A node used as an input but not defined by a gate can be given the self-copy gate \(\mathrm{Copy}(v;v)\), which every assignment satisfies. There are at most \(2|T|\) such nodes, because the original gates have at most \(2|T|\) input positions. Thus the new gate count is at most \(3|T|\); reducing the permitted failed-gate fraction by a factor three compensates. Unused nodes may be omitted and later assigned zero.

On this gate list, use the strong-Boolean relation of Schuldenzucker and Seuken at the same tolerance \(\varepsilon_c\). Their Proposition 2 shows gatewise that a strong-Boolean \(\varepsilon_c\) solution satisfies the weak-Boolean relations in Definition 2, since \(\varepsilon_c<1/10<1/4\). Their Lemma 1 replaces each Boolean gate by a constant-size gadget with no Boolean gates, such that an \(\varepsilon_c/2\) solution restricts to a strong-Boolean \(\varepsilon_c\) solution. Their Section 6 records the same reduction with a positive failed-gate fraction: the constant-size gadgets lose only a constant factor in that fraction (Schuldenzucker and Seuken 2019, Proposition 2, Lemma 1, and Section 6). The comparison gate in that paper has the opposite orientation from \(\mathrm{Less}\) here, so we swap its two inputs. The new parameters remain bounded rationals.

Consequently there are fixed positive rationals \(\eta=\varepsilon_c/2\) and \(\gamma\) and a polynomial-time constructed circuit \(G_{\rm nb}\) using only Constant, Scale, Copy, Add, Subtract, and Less such that any assignment satisfying its gates at tolerance \(\eta\) with at most a \(\gamma\) fraction of failures yields an assignment of \(G\) satisfying the original \(\varepsilon_c,\delta_c\) bounds. All scale factors are at most one. This no-Boolean relation is monotone in its numerical tolerance. We use that monotonicity only after this conversion; at no point is a weak-Boolean gate reclassified at a larger tolerance.

Fan-out reduction with fixed slack. We spell out the precision and failure accounting in the fan-out steps of (Babichenko et al. 2016, proof of Theorem 2, pp. 4–5). Suppose \(G_{\rm nb}\) has \(m\) gates, put \(\gamma_0=\min\{\gamma,1/4\}\), and set \[D=\lceil 8/\gamma_0\rceil,\qquad \eta_1=\eta/3,\qquad \gamma_1=\gamma_0/4.\] There are at most \(2m\) outgoing wire occurrences in total, hence at most \(\gamma_0m/4\) gates with fan-out at least \(D\). Delete those gates. For each wire from a deleted output into a retained gate, supply an independent \(\mathrm{Constant}(0)\) gate. The resulting circuit has at most \(3m\) gates and fan-out less than \(D\).

Given an assignment to this circuit, restore each deleted output as zero. A failed new constant can spoil only its one receiving gate. A new constant satisfied at tolerance \(\eta_1\) changes its receiving input by at most \(\eta_1\) under restoration. For a retained arithmetic gate satisfied at tolerance \(\eta_1\), the residual after changing its two inputs increases by at most \(2\eta_1\); this uses the scale bound one. For Less, an original input gap greater than \(3\eta_1\) remains greater than \(\eta_1\) after those two changes, so its required output also remains valid at tolerance \(3\eta_1=\eta\). Therefore, if \(f_1\) gates failed before restoration, at most \(\gamma_0m/4+f_1\) original gates can fail at tolerance \(\eta\). The bound \(f_1\leq\gamma_1(3m)\) makes this at most \(\gamma_0m\). This also shows why a smaller numerical tolerance is used when the replacement constants are made exact. The large-multiplier step in the cited construction is unnecessary for our bounded scale factors.

Next route the \(d>2\) outgoing wires of each remaining gate through a balanced binary tree of Copy gates. One may use at most \(2d\) new gates and depth at most \[h=\lceil\log_2 D\rceil+1.\] If the preceding circuit has \(m_1\) gates, there are at most \(2m_1\) wire occurrences, so the new fan-out-two circuit has at most \(5m_1\) gates. Use the fixed parameters \[\tau=\frac{\eta_1}{2(2h+1)},\qquad \gamma_2=\frac{\gamma_1}{5D}.\] When every Copy gate on a route is \(\tau\)-satisfied, its leaf differs from the root by at most \(h\tau\). The same arithmetic and comparison check shows that a retained gate satisfied at tolerance \(\tau\) becomes satisfied at tolerance at most \((2h+1)\tau<\eta_1\) when its inputs are restored to the roots. A failed Copy gate has fewer than \(D\) descendant receiving gates. Charging these receivers, and charging each failed retained gate to itself, loses at most \(D\) retained gates per failed gate. Thus at most a \(\gamma_2\) fraction of failures in the new circuit produces at most a \(\gamma_1\) fraction in the preceding one. All depths, blowups, and tolerance losses are fixed independently of \(I\).

Denote the final fan-out-two circuit by \(G_2\). All instance maps have polynomial bit cost: they copy bounded rational parameters and introduce only fixed rational constants. Their solution maps restrict assignments, restore zero values, or copy existing coordinates, so they also have polynomial bit cost on rational inputs.

The resulting assignment of \(G\) need not obey the particular witness polynomial \(p(M)\) in Definition 2. This causes no restriction on the decoder. The argument after (97) proves soundness for every real assignment meeting the gate-failure budget, and gives a deterministic decoder for rational assignments in time polynomial in \(N\) plus their total encoding length. Applying it proves the stated interface. ◻

Proof. Use the fan-out-two circuit of Lemma 84, with numerical tolerance \(\tau\) and failure allowance \(\gamma_2\).

The game reduction. For a fan-out-two generalized circuit, the gate construction in Rubinstein (Rubinstein 2018, sec. 7), used in the forward reduction of (Babichenko et al. 2016, Theorem 2), has two actions per player and maximum degree at most three. If the players of a gate gadget use only actions within \(\xi_0\) of a best response, their node probabilities satisfy that gate at tolerance \(2\xi_0\). Choose a fixed positive rational \(\xi_0<\tau/2\). These bounds imply our no-Boolean gate relations at tolerance \(\tau\): an antecedent for Less at tolerance \(\tau\) is also an antecedent at tolerance \(2\xi_0\), and the arithmetic and output bounds are stronger. The scale gadget’s output \(\min\{\alpha x,1\}\) equals \(\alpha x\) here because \(\alpha\leq1\). Each gate uses a fixed number of players, and a player belongs to only a fixed number of gate gadgets. Hence there are fixed integers \(C_1,C_2\) such that the game has at most \(C_1\) times as many players as circuit gates and each player not meeting the well-supported condition can spoil at most \(C_2\) gates. Choose a fixed positive rational \[\delta_{\rm w}\leq\frac{\gamma_2}{C_1C_2}.\] The decoded circuit assignment then meets its failure budget whenever all but a \(\delta_{\rm w}\) fraction of players meet that condition.

The gadget matrices have rational entries bounded in absolute value by a fixed rational \(B\geq1\): their variable scale parameters lie in \([0,1]\), and all other gadget constants are fixed. Replacing every payoff entry \(a\) by \((a+B)/(6B)\) puts the entries in \([0,1/3]\). For each player this adds an action-independent constant and scales every deviation gain by \(\lambda=1/(6B)\). Put \(\xi=\lambda\xi_0\). Thus the needed well-supported tolerance in the normalized game is the fixed positive rational \(\xi\).

Choose a fixed rational \(t>0\) such that \(t(t+13)<\xi\), and put \(\varepsilon_{\rm w}=t^2\). We use the local pruning argument of Rubinstein (Rubinstein 2018, Lemma 5); this is the lemma cited with an earlier number in the proof of BPR’s Theorem 2. For every player whose regret is at most \(t^2\), remove actions whose payoff is more than \((1+1/t)t^2\) below its best response and renormalize. Leave the other players unchanged. The regret bound ensures that the removed probability is less than one. The lemma’s calculation, with incoming degree at most three and total payoffs in \([0,1]\), shows that every retained action of each formerly happy player is within \[t(t+1+4\cdot3)=t(t+13)<\xi\] of a best response after all these changes. Unchanged unhappy neighbors contribute no change to that calculation. The fraction of players not meeting the well-supported condition therefore does not increase. This gives the required circuit assignment from any profile satisfying (214).

Rational witnesses and decoding. All instance maps above have polynomial bit cost. The auxiliary constants are fixed rationals, and the game matrices copy bounded rational gate parameters through fixed-size gadgets. For a rational profile, its regrets require only a fixed number of rational operations per player. The pruning threshold is rational, so exact comparisons, deletion of actions, and renormalization have polynomial bit cost. The extracted node probabilities, restrictions, and restored zero values consequently form a rational assignment of polynomial total encoding length.

Lemma 84 decodes this assignment in its total encoding length, so the particular witness polynomial \(p(M)\) of Definition 2 imposes no additional condition here.

Finally, the finite target search relation has a polynomial witness bound. Round the probabilities of a mixed Nash equilibrium to a grid of denominator \(q\), where the fixed integer \(q\) is greater than \(3/\varepsilon_{\rm w}\). With entries in \([0,1/3]\) and degree at most three, each pure-action payoff changes by at most \(1/q\) when the neighboring probabilities are rounded. Changing the player’s own probability changes its payoff by at most another \(1/q\). Its resulting regret is therefore at most \(3/q<\varepsilon_{\rm w}\). A fixed polynomial \(p_{\rm w}\) can encode these \(n\) rational probabilities. Satisfaction of (214) is checked by rational arithmetic in polynomial time. The composed instance map and solution decoder establish the stated search reduction. ◻

Proof. Apply the implication from Conjecture 2 to Theorem 3 in (Babichenko et al. 2016, sec. 4). This published chain passes through a bipartite degree-three family of weak approximate Nash instances. Theorem 3 supplies its fixed-tolerance circuit premise on a bounded-rational subclass, and Lemma 84 makes the gate-basis and fan-out preparation explicit. No change of weak-Boolean tolerance is needed. The remaining polynomial reduction gives hardness for a fixed positive relative error; choosing a smaller positive rational error only strengthens the requirements. Its marginal and conditional-probability decoder uses polynomial-time rational arithmetic. Composing with the circuit decoder after (97), which is polynomial in the total rational assignment length, gives the required search reduction.

For membership, an exact Nash equilibrium of the same game satisfies (215). Exact rational bimatrix Nash belongs to PPAD, and every rational bimatrix game has an exact equilibrium of polynomial encoding length (Chen et al. 2007, Theorem 1.1 and Section 2). Choose \(p_{\rm r}\) to accommodate that bound. The displayed inequalities are checked by polynomial-time rational arithmetic, so the stated finite search problem is total and belongs to PPAD. ◻

Proof. Use the no-Boolean, fan-out-two circuits of Lemma 84, with their fixed positive numerical and failed-gate tolerances. The published reduction in (Babichenko et al. 2016, Appendix B.2–B.3) applies to this bounded-rational subclass: after common normalization of prices and budgets, any invalid circuit decoding forces the Gini coefficient to be at least a fixed positive constant. Choose \(\gamma_{\rm c}\) strictly below that bound. Median normalization and price extraction have polynomial bit cost on rational outputs. Composing with the circuit decoder after (97) therefore gives the hardness reduction, with time polynomial in the input and total witness length.

For membership, Othman, Papadimitriou, and Rubinstein (Othman et al. 2016, Appendix A, Remarks 1–2) prove that computing an allocation at this clearing threshold with budgets in \([1,1+\beta]\) belongs to PPAD in the explicit-list model, for every fixed rational \(\beta>0\). Choose a rational \(0<\beta<\gamma_{\rm c}\). Such budgets have Gini coefficient at most \(\beta/2<\gamma_{\rm c}\); existence is guaranteed by (Budish 2011, Theorem 1). The budget interval selects solutions for membership and is not an additional requirement of the target problem.

Polynomial-size rational witnesses can also be seen directly. Fix such an allocation and its zero-price pattern, and cap prices at \(2+\beta\) without changing demands. Keep the budget interval, these price bounds and affordability of the chosen bundles. Introduce a common slack \(s\in[0,1]\) for the unaffordability of every strictly preferred listed bundle and for the positivity of every positive price. Maximizing \(s\) over the resulting bounded rational polytope has a positive optimum and a rational vertex optimum of polynomial bit length. Demands and the price-sign pattern, hence clearing error, are preserved. All target conditions are checked by rational arithmetic and enumeration of the explicit lists; the clearing test is equivalently \(4\sum_jz_j^2\leq M\min\{2k,M\}\). ◻

Proof. Apply (Deligkas et al. 2026, Theorem 2.2 and Lemma A.2) to the no-Boolean, fan-out-two circuits of Lemma 84. The published bridge gives a fixed positive failure allowance and makes every node an input to exactly one gate. Its solution decoder returns rational unary-count values, to which the decoder in Lemma 84 applies. All comparisons and arithmetic have polynomial bit cost. No change of tolerance for a weak-Boolean gate is required. ◻

Proof. Use the circuits of Lemma 88. For each fixed \(\varepsilon_{\rm m}<1/9\), (Deligkas et al. 2026, Proposition 4.4) supplies a fixed positive \(\delta_{\rm m}\) and a polynomial-time reduction to the stated Fisher markets. Composing its solution decoder with the circuit decoders proves the Fisher assertion of (Deligkas et al. 2026, Theorem 4.1) without its conjectural premise. For rational \(\varepsilon_{\rm m}\), the other constants may be chosen rational within the reduction’s strict margins. For a nonrational fixed \(\varepsilon_{\rm m}\), choose a rational clearing tolerance strictly between \(\varepsilon_{\rm m}\) and \(1/9\) and use its reduction: every solution with the smaller clearing error also satisfies the larger one. The Pure-Circuit bridge returns rational unary-count values; for rational market witnesses, all comparisons and decoding have polynomial bit cost. The decoder after (97) applies in the total length of the resulting rational assignment, without requiring the particular bound \(p(M)\) in Definition 2.

For the exchange markets, normalize prices so that \(\sum_jp_j=|B|\). Every buyer’s endowment then has value one, so the same prices and bundles give a Fisher equilibrium with precisely the same two errors. The positive-slope uncapped terms ensure that the price sum is nonzero at any approximate equilibrium. This is the transfer in (Deligkas et al. 2026, Appendix B and Theorem B.1); normalization also preserves polynomial rational encoding length. ◻

Proof. Use the no-Boolean circuit \(G_{\rm nb}\) of Lemma 84, with its fixed positive rational tolerance \(\eta\) and failure allowance \(\delta_{\rm nb}\) (the constant \(\gamma\) of that lemma). The target basis in (Daskalakis et al. 2023, Definition 8 and Appendix D) consists of exact zero/one constants, clipped linear gates, and comparison gates. For Scale and Copy, repeat the input with coefficient pairs \((\alpha/2,\alpha/2)\) and \((1/2,1/2)\), respectively; Add and Subtract use \((1,1)\) and \((1,-1)\). A Constant\((\alpha)\) uses its own exact-one node followed by the scaled linear gate. Retain Less: each strict source comparison antecedent implies the corresponding weak target antecedent, and the target output error is smaller. Choose a positive rational target tolerance below \(\min\{\eta,1/12\}\). Each original gate uses at most two target gates, and each failed target gate can spoil only its own original gate. A target failure fraction at most \(\delta_{\rm nb}/2\) therefore suffices. This proves the positive-gap premise in (Daskalakis et al. 2023, Conjecture 10); no weak-Boolean tolerance is changed.

Apply the second assertion of (Daskalakis et al. 2023, Theorem 4). Its turn-based construction has the stated discount, reward bounds and binary choices. Taking statewise marginals of a joint policy in such a game gives a product policy with the same values and unilateral deviation gains, so its approximate stationary CCE decodes to an approximate stationary Nash equilibrium with the same error. Choose a smaller positive rational error if needed. The fixed reduction parameters can be chosen rational with slack. For rational policy tables, policy evaluation solves rational linear systems, and the gate decoder and restrictions have polynomial bit cost. The decoder after (97) then applies in the total rational assignment length. Polynomial-size rational approximate policy tables exist by rounding stationary Nash policies at this fixed discount, as in (Daskalakis et al. 2023, sec. 2.5). ◻

Proof. Apply the triangle construction in (Park et al. 2023, Appendix C, Case 1) to Corollary 90. Write \(c(s)\in\{1,2\}\) for the state controller and suppress inactive actions. Add a one-action third player and retain states, transitions and initial distribution. Specify oriented edge rewards before scaling by \[(b_{12},b_{13},b_{23})= \begin{cases} (-r_2,r_1+r_2,0),&c(s)=1,\\ (r_1,0,r_1+r_2),&c(s)=2, \end{cases} \qquad b_{ji}=-b_{ij}.\] Each term depends only on the actions at its edge. Divide every edge reward by two. The resulting total rewards are \((r_1/2,r_2/2,-(r_1+r_2)/2)\), lie in \([-1,1]\), and sum to zero. For every test function \(V\), the continuation term in \(Q_i^V\) depends only on \(a_{c(s)}\). Allocate it to edge \(\{i,c(s)\}\) when \(i\ne c(s)\), and to any incident edge when \(i=c(s)\). This proves the required separability on \(K_3\) for every player and every \(V\).

The state process of any new-game policy agrees with that of its first-two-player restriction in the original game. Each original player’s normalized value and deviation gain in the new game is half the corresponding quantity in the original game; the dummy has no deviation. Thus error \(\varepsilon_{\triangle}=\varepsilon_{\rm s}/2\) suffices at the unchanged initial distribution. The primary source uses unnormalized values, which are twice our normalized values at discount \(1/2\); the stated error calculation uses our convention throughout. All new data use only rational addition and halving, and restriction has polynomial bit cost. Polynomial-size rational witnesses follow by the same fixed-discount rounding argument as above. ◻

Proof. Lemma 88 supplies input-once NAND/PURIFY circuits with a fixed positive failed-gate allowance \(\delta_F\). Convert each NAND\((u,v;w)\) to \[\mathrm{NOT}(u;a),\qquad \mathrm{NOT}(v;b),\qquad \mathrm{OR}(a,b;w),\] using fresh private nodes \(a,b\), and keep PURIFY unchanged. These are the ternary relations on \(\{0,1,\bot\}\) of (Farina et al. 2026, Definition 2.6): if \(u=v=1\), the NOT outputs are both zero and OR forces \(w=0\); if either input is zero, its NOT output is one and OR forces \(w=1\), even when the other input is \(\bot\). In all other cases NAND imposes no condition. PURIFY has the same relation in both bases. Every node remains the input of exactly one gate, and outputs remain uniquely defined. An original failed gate charges a failure in its own disjoint replacement block. Since \(m\) original gates give at most \(3m\) new gates, a failed-gate allowance \(\delta_F/3\) suffices. No numerical tolerance of a weak-Boolean gate is changed.

This establishes the premise of (Farina et al. 2026, Conjecture 1). Apply its Theorem 5.5, choosing the fixed reduction parameters and a positive rational equilibrium error within the strict bounds in its equations (23)–(24). Its states consist of circuit-variable states and constantly many absorbing sinks; the initial law is uniform precisely on the output-variable states. For a rational joint policy, equation (8) of that paper decodes a node from the reward player’s marginal \(p\): output zero for \(p\leq1/4\), one for \(p\geq3/4\), and \(\bot\) otherwise. Marginalization, comparison and restriction have polynomial bit cost. Follow these by the Fisher unary-count decoder and the decoder after (97). At fixed discount, rounding stationary equilibrium policies with slack gives polynomial-size rational witnesses; policy evaluation and best-response optimization are rational finite-state discounted MDP computations. No collapse of correlated policies to Nash policies is used in this reduction.

Finally, the extension in (Farina et al. 2026, Remark 5.7) preserves the normalized incentive inequalities exactly. Put \(\beta=1/16\) and, for a fixed rational \(\gamma\in[\beta,1)\), set \[\tau=\frac{\beta(1-\gamma)}{\gamma(1-\beta)},\qquad \widetilde P=(1-\tau)I+\tau P.\] For every stationary joint or unilaterally deviated policy \(\pi\), \[I-\gamma\widetilde P^\pi =\frac{1-\gamma}{1-\beta}(I-\beta P^\pi).\] Thus \((1-\gamma)(I-\gamma\widetilde P^\pi)^{-1}r_i^\pi\) equals \((1-\beta)(I-\beta P^\pi)^{-1}r_i^\pi\). Rewards, actions and initial law are unchanged, and the lazy transition remains rational and single-controller with polynomial encoding length. ◻

Proof. Use the fan-out-two circuit of Lemma 84, with its fixed positive numerical tolerance \(\tau\) and failure allowance \(\gamma_2\). Its no-Boolean gate relations agree with (Braverman et al. 2026, Table 1), so no Boolean tolerance is changed. The reduction underlying (Braverman et al. 2026, Theorem 3.2) has two stages: Lemma 3.4 of that paper converts these circuits to bounded-degree threshold games, and Lemma 3.25 converts those games to HZ instances. The construction uses a fixed integer \(m\) and rational market data, with HZ error \(m^{-40}\). In that construction, each threshold-game vertex \(v\) has an associated group \(G_{v,1}\) of goods. The first decoder assigns \(v\) the value \(\min\{1,m^2p(G_{v,1})\}\), where \(p(G_{v,1})\) is the minimum price in that group. This decoder, the threshold-game-to-circuit decoder, and the subsequent circuit decoders have polynomial bit cost on rational witnesses. Composing with the decoder after (97) therefore gives an End-of-Line solution in time polynomial in the input and total rational witness length.

For completeness, polynomial-size rational HZ witnesses preserve the exact equalities above. Start from a normalized exact equilibrium \((x,p)\), as in (Braverman et al. 2026, Lemma B.2); summing budgets and column sums gives \(\sum_jp_j\leq n\). Round prices upward on a rational grid of mesh at most \(\varepsilon_{\rm h}/4\), retaining zero prices. Express \(x\) as a convex combination of at most \(n^2\) permutation matrices and round its weights, preserving nonnegativity and total weight one, so each row changes in \(\ell_1\) norm by at most \(\varepsilon_{\rm h}/[4(n+1)]\). A denominator of order \(n^3/\varepsilon_{\rm h}\) suffices. Row and column sums remain exact, expenditures increase by less than \(\varepsilon_{\rm h}\), and utilities decrease by less than \(\varepsilon_{\rm h}\). Since prices only increase, the comparison optimum cannot increase. These rational witnesses have a fixed polynomial encoding bound; their utility conditions are checked by rational linear programming. ◻

Proof. Cyclic schedule and Boolean validity. Use the normalized transcript positions and the two orders of Section 2.1, renaming their length \(T=O(N)\). For this variant keep two content tapes \(A,B\); their occupied prefix lengths are specified by the public stage, so no occupation coordinates are needed. With the notation \(Q_x,U_y,V_y\) from that section, use the following four stage conditions: \[\begin{array}{c|l} 0\le s\le T & A=Q_x,\quad B\text{ a forward prefix of length }s \text{ from }S(x),\\ T\le s\le2T & B=Q_y,\quad A\text{ a reconstruction prefix of length }2T-s \text{ from }y,\\ 2T\le s\le3T & B\text{ a valid full transcript},\quad A=\operatorname{pref}_{\pi_{\mathrm f},s-2T}(B),\\ 3T\le s\le4T & A\text{ a valid full transcript},\quad B=\operatorname{pref}_{\pi_{\mathrm f},4T-s}(A). \end{array}\] The boundary descriptions agree. At \(s=T\), the first gives \(A=Q_x,B=Q_y,y=S(x),P(y)=x\); hence reconstruction from \(y\) gives exactly \(A\). Conversely, a complete valid reconstruction from \(y\) gives \(x=P(y)\), \(S(x)=y\), and the same pair. At \(2T\), \(3T\), and \(4T\) the descriptions respectively say that \(A\) is empty, that \(A=B\) is full, and that \(B\) is empty. The last is the stage-zero hub condition.

Choose a fixed polynomial scale \(n_G=C_G(N+2)^2\), with \(C_G\) large enough that \(n_G\ge4T+3\) and all fixed lower cutoffs and degree inequalities below hold, and use (99)– (102) with \(n'\) replaced by \(n_G\). In particular \(h^\ell\ge n_G^3+3\), \(M=h^\ell-1\), and \(C=K_1^\times=\langle\gamma\rangle\). Pad stages \(4T,\ldots,M-1\) by the hub condition, and identify stage \(s\) with \(c=\gamma^s\) by enumerating the group. No discrete logarithm is needed. All hub-to-hub steps, including the wrap to stage zero, are allowed.

The forward tape proposals are, in order: fill the next forward \(B\) position; erase the last reconstruction \(A\) position; copy the next \(B\) position into \(A\); erase the last copied \(B\) position; or do nothing at a padded hub. The reverse proposals are respectively erasure, local reconstruction, erasure, copying, and the identity. A fill uses its computed bit even if the new terminal comparison fails. An actual edge is exactly a proposed pair whose two stage conditions hold. Prefix uniqueness from Section 2.1 makes the operations reciprocal on such pairs: earlier operands or the unchanged full tape determine each erased bit. Thus both degrees are at most one.

Add a legacy vector \(e\) on \(C\), one-hot at \(c^{-1}\), and write \(b=(A,B,e)\). Impose bitness, the one-hot equations (103), and, for each stage \(c\), multiply every tape constraint at that stage by \(e_{c^{-1}}\). Gate constraints have degree at most two; blank, copy, and terminal-comparison constraints are linear. The resulting \(O(MT+M^2)\) rows have degree at most three and describe exactly the union of valid stage tapes. Their row and column index sets are polynomial in \(N\), hence require only \(O(\ell)\) digit coordinates in the linear verification tool. Padding other tape coordinates by zero to full digit grids preserves these bounds. A proposal changes at most one content coordinate and the two legacy coordinates \(c^{-1},(\gamma c)^{-1}\). Use these three unit vectors, or a zero content vector at hubs, as a fixed binary flip alphabet. The coefficient of the content flip is the old bit plus its required new value. Either direction needs only the old bit, at most two operands or one copy bit, and finitely many public phase and rule bits. The same rule defines proposals on every Boolean tape, without a validity call.

Endpoints and progress paths. A forward prefix can always be shortened, so a missing successor is its first failed terminal comparison. With \(A=Q_x\), put \(y=S(x)\). Then \(P(S(y))\ne y\) and \(P(y)=x\). If \(y=0\), the source promises would give \(x=P(0)=0\) and \(S(0)=0\), a contradiction. A reconstruction prefix can always be shortened in the forward direction; a missing predecessor gives \(y=\operatorname{in}_S(B)\) and \(S(P(y))\ne y\). Copy and hub stages have both neighbors. Thus there are no isolated vertices. The only zero exception is \(B=Q_0\) with its longest valid reconstruction prefix from zero. This transcript exists because \(P(S(0))=0\), and its maximal length \(k_*<T\) follows from \(S(P(0))=S(0)\ne0\). Its stage is \(2T-k_*\), and its successor shortens the prefix or starts copying if \(k_*=0\). Direct circuit evaluation computes this source and successor.

For each macro tape at stage \(c\), introduce the path \[(\gamma^{-1}c,b,1,q-1),\ldots,(\gamma^{-1}c,b,1,0), (c,b,0,0),\ldots,(c,b,0,q-1).\] Attach each actual macro edge from the full pre end of one path to the full post start of the next. This is the four-operation extension of Definition 41, with actual macroedge validity in place of that definition’s disabled-wrap rule. The replacement paths are disjoint, so they preserve all components, endpoints, and degree bounds. Every edge changes a mode or progress coordinate. If the exceptional macro source is \((c_*,b_*)\), its extended source and successor are \((\gamma^{-1}c_*,b_*,1,q-1)\) and \((\gamma^{-1}c_*,b_*,1,q-2)\). At another endpoint, scanning the legacy vector and transcript gives the appropriate nonzero vector above in polynomial time.

Canonical arrays without positive tags. Use the ordinary order-one lifts for \(A,B\), the cyclic lift of Lemma 43 for \(e\), and the constant chart. Include every ordered monomial type list of length at most three in these groups, with independent argument groups even for repeated types. There are constantly many lists. Recursive factorization fixes the monomials from the order-one charts. Apply Lemma 44 to their extension, zero-padding, bitness, and cubic validity rows. A coincident-grid product in a validity row is a linear condition on a tensor entry, so its verification uses that lemma rather than a diagonal unknown-product query. This fixes all its canonical certificates uniquely.

Adjoin \(J_c\), the clock-times-monomial charts, and the clock/legacy identity (122). The clock-indexed construction of Lemma 45 provides every critical logical bit and every public rule bit for both proposal directions. Their addresses are indexed by the absolute frame \(cz\); they do not require reading the unknown frame as a binary word. All these canonical formulas are defined for arbitrary Boolean \(b\), even when a final validity row fails.

For every persistent chart of positive assigned Boolean degree, including every verification auxiliary, and each of the eight flip masks, apply the derivative construction (126) using the same frame in both terms. The top Boolean degree cancels, so the derivative and all certificates introduced to verify it have degree at most one less. Construct the coefficient maps from the parent’s specified canonical recipe by (129), and repeat on every new positive-degree family. After at most three drops the process stops. It updates the certificates themselves and does not assume their validity. The number of families is fixed. Each persistent family has at most one \(O(\ell)\) slot axis, and finitely many applications of the degree estimate (117) leave coordinate degree \(O(\ell h)<D\). Give all inherited projection axes consistent full \(K\) labels and reserve a new label for each derivative axis; a fixed common \(K^u\) suffices. No positive-tag reuse or one-port identification is needed.

Validation, affine updates, and size. Use exactly the mode, radix marker, and projection stacks of Lemma 50. Their triangular recurrences uniquely fix all coefficients. At full progress, the singleton-stack sums (141) supply the constant-polynomial critical values for the finite proposal rule. For every persistent chart and every stack subset, the summed derivative stack in (142) gives its exact change at the fixed frame. These simultaneous identities hold on every Boolean tape. Increasing and decreasing progress use (138)– (140); frame advancement occurs only with empty stacks and uses the designated scaling by \(\gamma\). Thus the complete proposed target, including every proof chart, obeys the bounded affine formulas. Public coefficients and mask pulls are independent of target point and row; a common linear row extension and line-coefficient extraction commute with them.

The exact-gap argument of Lemma 51 now applies to this finite family: first enforce shape, independence, and linearity, then monomial and clock identities, then all unique linear certificates, and finally the marker and stack recurrences. If every identity holds, there is one valid tape and its canonical tuple. Otherwise a nonzero polynomial discrepancy, after the stated earlier linearity conditions, is detected with a fixed positive probability by uniform points, separable masks, and binary forms. Products of nonconstant monomial factors use their independent argument groups; clock products use a fresh independent group; marker products are sampled at independent points after constancy is enforced. Ignored coordinates are filled independently. Hence all unknown products have independent full point marginals, and all linear probes retain the smoothness of the linear tool. On an invalid Boolean tape the recipes, covariance, and degree bounds still hold, but some final identity fails with the same gap.

Finally, \(M,|K|,q^{O(\ell)}\), the validity matrices, and all mask spaces have polynomial size in \(N\). More explicitly, \(T\le M\), the stage rows number \(O(M^2)\), and the logical monomials of degree at most three number \(O(M^3)\). All later row and column sets have size a fixed power of these quantities or of \(|K|\); their base-\(h\) digit dimensions are therefore \(O(\ell)\). The fixed-depth degree estimates remain \(O(\ell h)<D\) after the chosen cutoff. Boolean interpolation through degree three, every array operation, and every fixed-depth certificate construction consequently take polynomial time. No step enumerates Boolean assignments or graph vertices. This proves all the asserted costs and interfaces. ◻

Proof. There are still only constantly many blocks, each of polynomial size, so the balancing product remains polynomial. The point and line construction, rectangular action, and common row extension do not use tags. In the proof of Proposition 60, all replacements before the product step concern individual \(Y\) tracks. For each added product block, the additivity test in \(Q\) and the two independent uniform operand positions give exactly the same product replacement: a false binary matrix is detected by a uniform outer-product form with probability at least \(1/4\). Taking a positive fixed mixture over the enlarged finite block list therefore gives the same vanishing-rejection replacement argument. The algebraic validator is then applied to the common target tuple; every requested point product is now present. Its exact gap forces validity. On an invalid structurally canonical word, no replacement is necessary: the final validator component already rejects with a fixed positive probability. Its mixture weight and the fixed losses in binary-form simulation define \(\theta_{\rm inv}\). Distinct logical or mode/marker data retain the positive distance witnessed by their \(Y\) blocks, with the new fixed block weights.

For correction, the two-axis support and inner-table arguments apply to any ordered pair of point tracks. They use independent row coordinates and the two row-code actions, not tag compatibility. Use the new block count in (154) and choose one radius satisfying (156) for this block list. The bad-column bound, support contraction, finite-cone consistency, and amplification then prove the same average guarantee. Each pair of affine shifts remains a permutation of the full pair domain, even for a repeated type. The proof of Lemma 66 consequently applies to every added block, with a new finite summed density bound. In particular, no product request is converted to a diagonal pair.

For full recovery, apply the proof of Proposition 68 to each order-one chart \(W_w,W_e,W_{s_i}\). The work and port charts use ordinary grid extensions, and the legacy chart uses its degree-in-bound cyclic lift. In each case nearest Hadamard symbols, equal-fiber plurality, and plurality over ignored coordinates produce a native polynomial estimate of sufficiently small constant symbol error. For each logical grid point, the complete enumeration of lines and the verified Berlekamp–Welch systems in that proof recover its exact value by a strict majority. The argument uses degree and table structure, not the final validity equations. There are polynomially many grid points and a fixed number of charts. Reducing the radius by the fixed block-weight factors makes all these decodings valid simultaneously. The same proof applies to the supplied general chart template under the stated separation and grid hypotheses. ◻

Proof. Fix the true decision branch of the nearby current label, charging the selector’s error separately. For a point or line \(Y\) request, commute the proposed update through the common row encoder and, for a line, through restriction and coefficient contraction. This gives a bounded XOR of old \(Y\) requests with publicly pulled-back forms, plus public bits. Each map in the fixed public list induces a commuting column permutation on the retained point and ordered-line domains, preserving bounded outer-index density. If masks select among these maps, sum their unconditioned slot bounds before selection; the list is bounded independently of the request. Apply average correction with the error divided among these boundedly many slots.

For a proposed \(Z\) bit, expand both updated symbols by bilinearity. Every two-variable term is present because all ordered point-track pairs were included. Each side undergoes its own affine column permutation, preserving the joint density of the pair. A term with one public actual \(J\)-symbol is an arbitrary linear form of the other symbol, and (157) supplies its complete surviving row/point density. Two public operands give a public bit. Thus the proposal is predicted using only the current close word; its target need not be valid or supplied as a received word.

Now simulate the tester on the proposed word by supplying each bit from this predictor with fresh internal randomness. First fix the selector error below \(\theta_{\rm inv}/16\) and its complete bounded tree. Unfold that tree and the bounded tester tree. Each fixed hypothetical tester request has bounded density, so next choose the per-prediction errors to sum to less than \(\theta_{\rm inv}/16\) over all these slots. The simulated rejection probability differs from the true one by less than \(\theta_{\rm inv}/8\). A valid proposal has true rejection zero; an invalid structural proposal has rejection at least \(\theta_{\rm inv}\). Independent repeated simulations and the threshold \(\theta_{\rm inv}/2\) therefore give any specified fixed reliability. Include the stated guards separately when interpreting the result as an edge flag.

All error estimates use the unconditioned request law on each fixed branch, followed by a union bound over the complete bounded tree. They do not renormalize after a successful comparison or condition on a rare selected branch. Wrong decisions and failed comparisons still select only from the supplied finite lists; public-zero defaults and fresh splitting preserve the raw-read bounds of Lemma 66. At fixed accuracy, the number of simulations and all their supports are bounded and polynomially constructible, as required. ◻