README.md

Nine calls are necessary in the abelian three-register bit model

Eight rational rank-one calls cannot produce three dimension-three bit interchanges in the model below. Nine calls are necessary and sufficient. The proof combines algebraic reductions with a complete finite calculation. It checks 2,276 scalar multiplicity families and all 21,317,520 distinct orders. An adaptive exact search excludes every rational frame relation space. There is no bound on frame numerators or denominators.

This is a computer-assisted theorem for three registers. It does not cover extra registers or arbitrary free address maps between paid calls. It gives no improvement in $\kappa$ or the integer-multiplication exponent. It is not a proof-assistant verification.

1. Model, attribution, and statement

The additive group $M_3(\mathbb Q)$ has formal symbols $[A]$ with $[A][B]=[A+B]$. Work in its group algebra over $\mathbb F_2$. A paid call is

$$ D_N([A])=I+([A]-1)N,\qquad \operatorname{rank}_{\mathbb Q}A=1,\qquad N=xy^T,\quad x,y\in\mathbb F_2^3,\quad y^Tx=1. $$

There are 28 possible binary rank-one idempotents $N$. We ask whether

$$ \prod_{j=1}^{8}D_{N_j}([A_j]) =\operatorname{diag}([C_1],[C_2],[C_3]), \qquad C_w\in M_3(\mathbb Q) \text{ invertible and lower triangular}. \tag{1} $$

Factor order matters. Rational frame entries are not reduced modulo two. Equation (1) requires equality of every formal coefficient. An identity at one finite address size does not suffice.

This is the scalar-idempotent abelian register model in eumemic's PR #288, section 1.2, pinned at 475a088b5862f75f0b10596cfd6842d19531a5ec. That source also gives the dimension-two flag bound used below. Free scalar XOR maps are represented by the choices of $N_j$. A final output permutation can be removed by relabeling roles. In the normalized identity, augmentation $[A]\mapsto1$ forces the remaining scalar output map to be the identity. Arbitrary free address maps between calls are outside this model.

Theorem. For three registers over $\mathbb F_2$, nonzero rational rank-one paid frames, binary rank-one scalar idempotents, and three invertible lower-triangular rational frame targets, the minimum number of paid factors is nine.

The pinned PR #288, section 1.2(f), leaves the three-register cases with seven or eight calls open after symbolic bounds and bounded searches. This note excludes both cases for the stated model, with no bound on the rational frames. A related earlier result is huxint's PR #203, at commit d2873e20750d0949d2ad75cbc4cd82b5b1a74e84: paid frames with a common triangular flag cannot save rank. Our paid frames need not have such a flag. We use the flag and projection methods of these predecessors in the reductions below and do not claim those methods as new. This comparison concerns the pinned sources; no broader claim of literature priority is made. The proof, implementations, and checks were prepared with substantial OpenAI Codex assistance.

2. Projection and rank tools

Restrict each group-algebra argument to the subgroup generated by its finitely many exponents. This group is free abelian. Its group algebra is a Laurent polynomial domain and has a fraction field.

For $k$ nontrivial factors, write $N_j=x_jy_j^T$. Over that fraction field, the ordered product has the form

$$ \prod_{j=1}^k(I+a_jx_jy_j^T)=I+XTY^T, \qquad X=(x_1\ \cdots\ x_k),\quad Y=(y_1\ \cdots\ y_k), $$

where $T$ is upper triangular with nonzero diagonal $a_1,\ldots,a_k$. If the product is $I$, the rank inequality gives

$$ \operatorname{rank}X+\operatorname{rank}Y\le k. \tag{2} $$

If the difference from $I$ instead has rank $W$, both active scalar spans have dimension at least $W$. Rational linear projections of the frames give group-algebra homomorphisms, so these bounds apply after projection.

3. Frame span at most four

Low-span lemma. In address dimension $m$ with $W$ registers, if the paid rank-one frames have rational span dimension at most $m$, invertible targets require at least $mW$ calls.

Choose a basis $B_i=u_iv_i^T$ of that span from the paid frames. Every target belongs to the span because it occurs in the expanded product's support. A span dimension below $m$ cannot contain a rank-$m$ matrix. At dimension $m$, write one invertible target as $C=\sum_i c_iB_i=X\operatorname{diag}(c_i)Y^T$. Both $X,Y$ are invertible and each $c_i$ is nonzero. In these left and right bases, the frame span is diagonal. Each paid rank-one frame is on one basis line. Each target has a nonzero coefficient on every line. Projection onto one coefficient gives target-minus-identity rank $W$, so that line needs at least $W$ calls. The $m$ sets of calls are disjoint.

Span-four lemma. In dimension three, a paid frame span of dimension at most four requires at least $3W$ calls for $W$ invertible lower-triangular targets.

Let $S$ be the frame span and choose its basis from paid rank-one matrices. The determinant of a linear combination is a nonzero homogeneous polynomial of degree three. It has a nonzero mixed coefficient at three distinct basis matrices: a repeated rank-one summand gives zero in the determinant expansion. The left vectors of those three matrices are independent, as are their right vectors. Common invertible rational row and column maps make them $E_{00},E_{11},E_{22}$. The low-span lemma handles dimension three. At dimension four, the last basis matrix is $B=uv^T$, and every matrix in $S$ has the form $D+tB$, with $D$ diagonal.

Suppose all coordinates of $u,v$ are nonzero. For distinct $i,k,l$, the minor of $D+tB$ on rows $i,k$ and columns $i,l$ is $D_{ii}t u_kv_l$. Thus a rank-one matrix with $t\ne0$ has $D=0$. All paid frames lie on the four independent lines $E_{00},E_{11},E_{22},B$. Project onto one line's coefficient. Target-minus-identity rank equals the number of targets with nonzero coefficient there, and each retained call contributes at most one. Every invertible target needs at least three nonzero coefficients, by rank subadditivity. The sum of the four line bounds is therefore at least $3W$.

Otherwise $u$ or $v$ has a zero coordinate. In the directed graph of $B$, each vertex of a cycle lies in $\operatorname{supp}(u)\cap\operatorname{supp}(v)$. Each strongly connected component consequently has size at most two. A simultaneous row and column permutation makes $S$ block upper triangular with diagonal blocks of size at most two. A rank-one matrix in this space has at most one nonzero diagonal block. Two such blocks would force a nonzero block below the diagonal. Assign each paid call to its nonzero diagonal block, if any.

Every target has invertible diagonal blocks. The original ratios $C_1^{-1}C_w$ are simultaneously lower triangular. After the common row and column maps, the ratios are conjugate to these matrices and are block upper triangular. Each diagonal block is an invariant subquotient of a family with a complete common rational flag. Intersect that flag with the invariant subspaces, pass to quotients, and remove repeated spaces. Each block retains a complete common flag. Common invertible row and column maps within that block then make all its targets lower triangular.

Here is the dimension-two flag bound. Let $E_2$ count calls assigned to one two-dimensional block, and let $U_2$ count its frames with nonzero upper entry. Write $r_X,r_Y$ for their scalar ranks. Upper-entry projection has zero target and gives $r_X+r_Y\le U_2$ by (2). For diagonal coordinate $i$, let $l_i$ count lower frames with nonzero entry there. Diagonal projection gives $W\le r_X+l_i$ and $W\le r_Y+l_i$. A lower rank-one frame has at most one nonzero diagonal entry. Adding the four inequalities gives

$$ 4W\le2(r_X+r_Y+l_0+l_1)\le2E_2. $$

A one-dimensional block needs $W$ calls by target rank. Block dimensions sum to three and assignments are disjoint, which proves the lemma. This step uses the lower-triangular target hypothesis.

4. Frame span at least seven and scalar irreducibility

At-most-one-relation lemma. Eight paid frames of span dimension seven or eight cannot give three invertible targets. Lower-triangular targets are not needed for this lemma.

Introduce independent invertible variables $t_j$ and set $P(t)=\prod_j(I+(t_j-1)N_j)$. Each entry is multilinear. For independent frames, all subset sums differ. Every off-diagonal coefficient of $P$ must therefore vanish. Differentiation at $t=(1,\ldots,1)$ makes each $N_j$ diagonal. Each paid frame is assigned to one target, and rank subadditivity gives the contradiction $9\le8$.

At span seven, the integer relation lattice has a primitive generator $r\in\mathbb Z^8$. If some $|r_j|\ge2$, subset sums still cannot collide. Otherwise $r_j\in{-1,0,1}$. Set $S={j:r_j\ne0}$. The substitution $t_j\mapsto[A_j]$ has Laurent ideal kernel generated by

$$ g=\prod_{r_j=1}t_j-\prod_{r_j=-1}t_j. $$

A primitive vector extends to an integer basis, which proves this kernel description. Each off-diagonal entry of $P$ is a multiple of $g$. Differentiation at one shows that all projectors on $S$ have one common off-diagonal pattern; all others are diagonal.

For $N=xy^T$ with $y^Tx=1$, the supports of $x,y$ meet in one or three coordinates. In the latter case $N=J$, the all-ones matrix. In the former, its directed off-diagonal graph has no cycle, since each cycle vertex would lie in both supports. Unless the common pattern is that of $J$, one coordinate order makes every projector triangular. Each projector has exactly one nonzero diagonal entry, so the disjoint rank bound applies.

For the pattern of $J$, all projectors on $S$ equal $J$. Set outside variables to one; the sole relation permits this. The remaining product is $I+([\sum_{j\in S}A_j]-1)J$. Diagonality forces this sum to vanish. The primitive relation thus has all plus signs on $S$, up to overall sign. Keep one outside factor $E_{kk}$, and let $B$ be the sum of the support frames before it. With $z=[B]$, the conjugated projector is

$$ (I+(z-1)J)E_{kk}(I+(z^{-1}-1)J). $$

For distinct $a,b\ne k$, its $(a,b)$ entry is $z+z^{-1}$ and must vanish. The rational address group is torsion-free, so $B=0$. The only zero-sum subsets of $S$ are empty and full. Every outside factor is before or after all support factors. The support forms an identity block, and the remaining coordinate factors give the same rank contradiction.

Two-register lemma. Two invertible rational $3\times3$ targets require at least six calls over $\mathbb F_2$.

For at most five calls, span at most three is excluded by the low-span lemma. Higher span has at most one relation. The preceding Laurent argument forces diagonal projectors, or one common off-diagonal pattern on the relation support. A binary $2\times2$ rank-one idempotent cannot have both off-diagonal entries equal to one: rank one would force both diagonal entries to one, but that all-ones matrix squares to zero. Thus all projectors are triangular in one order. Each frame belongs to one target, whose ranks sum to six.

Irreducibility lemma. The projectors in an eight-call solution have no common proper nonzero binary invariant subspace.

Suppose they preserve $V$. The diagonal target preserves $V$ too. Group coordinate axes by equal $C_w$. Each distinct target monomial has the coordinate projection onto its group as coefficient. Independence of monomials shows that these projections preserve $V$. Choose bases within the groups adapted to their intersections with $V$. The target stays diagonal, and the projectors become block triangular with block sizes one and two. For a rank-one idempotent, exactly one diagonal block is a rank-one idempotent and the other is zero; this follows from $N=xy^T$ and $y^Tx=1$. The one-register block needs three calls by rank subadditivity. The two-register block needs six. These assignments are disjoint.

5. Frame span six

5.1. Common-$J$ calculation

Consider projectors in ${J,E_{00},E_{11},E_{22}}$ with at most two independent rational frame relations. Suppose the output is diagonal or has only one possible off-diagonal entry, at $01$. We show that the $J$ frames make zero net contribution to the target diagonals.

Put $y_j=t_j-1$. For the generated free abelian group $H$, the associated graded algebra at the augmentation ideal is the polynomial algebra on $H/2H$. The integer relation lattice is saturated, so the kernel from $\mathbb F_2^E$ has the rational relation dimension. The degree-one off-diagonal term is $J_{\rm off}L$, where $L=\sum_{N_j=J}y_j$. If $J$ occurs, the output condition forces the nonzero form $L$ to vanish on $H/2H$.

Set $K_i=\operatorname{offdiag}(JE_{ii}+E_{ii}J)$. The matrices $K_0,K_1$ are independent modulo $\operatorname{span}(J_{\rm off},E_{01})$: $K_0,K_1,J_{\rm off}$ are symmetric and independent, whereas $E_{01}$ is not symmetric. Define

$$ q_i=\sum_{j:N_j=E_{ii}}y_j\sum_{k<j:N_k=J}y_k. $$

After imposing $L=0$, the degree-two conditions are $q_0+q_1=q_0+q_2=0$. In this matrix quotient, a group relation gives no second-order correction because its first-order term is already zero. At most one additional linear relation remains. Thus the nonzero quadratics must have one common linear divisor.

Eliminate the last $J$ variable by $L=0$. If there are $h$ such factors, their $h-1$ proper prefix sums $p_a$ are independent. Each displayed quadratic is bilinear between the remaining $J$ variables and the coordinate-factor variables. A nonzero bilinear polynomial with a linear divisor has rank one, with one factor in each variable set. Compare bidegrees $(2,0)$ and $(0,2)$ to see this. Its nonzero columns here are prefix vectors $p_a$, so all contributing coordinate factors occupy one internal gap between $J$ factors.

If both quadratics are nonzero, an internal $E_{00}$ makes their gaps equal. Without one, they use disjoint nonempty sets of $E_{11}$ and $E_{22}$ variables; different gaps would leave no common linear divisor. If one quadratic is zero, the other gives the same single-gap conclusion. If both vanish, there is no internal coordinate factor. There are therefore at most two $J$ runs separated by a diagonal block.

Combine the runs and remove exterior diagonal factors. The product is $U(b)DU(c)$, where $U(z)=I+(z-1)J$, $D=\operatorname{diag}(d_0,d_1,d_2)$, and $b,c,d_i$ are monomials. Its off-diagonal entry $ij$ is

$$ (b-1)d_j+(c-1)d_i+(b-1)(c-1)(d_0+d_1+d_2). $$

If $b=1$ or $c=1$, the required zero entries force both to be one. Otherwise entries $10,20$ give $d_1=d_2$, and entries $02,12$ give $d_0=d_1$. Any required zero entry then gives $bc=1$. The output equals the product of the coordinate factors. The possible $01$ entry also vanishes. Target exponents are disjoint sums of coordinate frames.

5.2. Two relations and the finite classification

At span six the saturated integer relation lattice has rank two. Call a relation a cube relation if all its entries belong to ${-1,0,1}$. Cube relations span the full rational relation space. Otherwise quotient $\mathbb Z^8$ by their saturated span, of dimension at most one. This lift preserves every equality of subset sums, hence every coefficient of the product. Lift each target by a subset with its nonzero coefficient. The algebraic at-most-one-relation argument assigns disjoint frame sets to the lifted targets, possibly after canceling a $J$ block. Map back to the actual rank-one frames to obtain $9\le8$.

Choose independent cube relations $r,s$. If their reductions modulo two are independent, some minor is odd. A $2\times2$ cube minor has absolute value at most two, so that minor is $\pm1$ and the basis is saturated. Otherwise the reductions agree. Replace $r,s$ by $(r+s)/2,(r-s)/2$. These are independent cube vectors with disjoint nonempty supports; again they have a unit minor. Thus a saturated cube-valued basis exists.

First-order off-diagonal coefficients have the form

$$ \operatorname{offdiag}(N_j)=(r_j\bmod2)B+(s_j\bmod2)C. $$

Pattern dimension zero gives coordinate projectors. Dimension one gives an acyclic common pattern or $J$; triangularity or section 5.1 excludes it. At dimension two, $B,C$ are independent. A zero pattern then means $r_j=s_j=0$ over the integers. Let $S$ index nonzero patterns and $T$ the remaining coordinate projectors. Both complete relations are supported on $S$, so the actual group splits as $H=H_S\oplus\mathbb Z^T$.

The finite classification enumerates all 512 binary matrices, selects the 28 rank-one idempotents and their 19 nonzero patterns, and forms all 129 two-dimensional pattern spaces. For each nonzero-pattern pool it checks all 21 complete binary flags. There are 123 pools with a common flag and six exceptions. The exceptions are exactly the coordinate permutations of

$$ P=\begin{pmatrix}1&1&0\0&0&0\0&0&0\end{pmatrix},\qquad Q=\begin{pmatrix}0&1&0\0&1&0\0&0&0\end{pmatrix},\qquad R=\begin{pmatrix}0&0&0\1&0&1\1&0&1\end{pmatrix}. $$

Every proper subset of an exception has a common flag. Two independent occurring patterns generate every dimension-two case, so this enumeration is exhaustive. A separate implementation with tuple matrices and actual vector subspaces reproduces the classification.

For a common-flag pool, project onto $H_S$ and use its scalar flag basis. Each rank-one idempotent has exactly one nonzero diagonal entry. Product diagonals therefore assign disjoint sets of $S$ frames. Conjugation preserves the characteristic polynomial. Unique factorization over the fraction field identifies these diagonal monomials, with multiplicity, with the three original projected target monomials. Their rational matrix ranks sum to at most $|S|$.

For an exceptional pool, put

$$ S_0=\begin{pmatrix}1&1&0\0&1&0\0&0&1\end{pmatrix}. $$

Direct multiplication gives $S_0PS_0=E_{00}$, $S_0QS_0=E_{11}$, and $S_0RS_0=J$. The conjugated target has only a possible $01$ off-diagonal entry. Section 5.1 assigns disjoint $S$ frame sums to its diagonals. The same characteristic-polynomial argument gives the rank bound $|S|$.

Project onto each free $T$ generator. Only its coordinate-projector factor remains, so that frame belongs to one original target. With $C_w=C_w^S+C_w^T$, rank subadditivity now gives

$$ 9=\sum_w\operatorname{rank}C_w \le\sum_w\operatorname{rank}C_w^S+\sum_w\operatorname{rank}C_w^T \le |S|+|T|=8. $$

This excludes span six. Sections 3–5 leave exactly span five.

6. Scalar distance

For each nonzero binary row $r$, at least three indices have $rx_j\ne0$. For each nonzero binary column $v$, at least three have $y_j^Tv\ne0$.

Suppose at most two indices meet a row $r$, and let $V$ be the rational span of their frames. Each matrix in $V$ has rank at most two, so none of the invertible targets lies in $V$. Choose a rational linear functional $\ell$ that kills $V$ and is nonzero on every target. Such a functional exists: a finite union of proper subspaces cannot cover the annihilator of $V$ over $\mathbb Q$.

Under this projection the selected factors become $I$. Each other factor fixes $r$ on the left because $rN_j=0$. Their product fixes $r$, but the projected diagonal target cannot: all its diagonal entries differ from one. This contradiction proves the row claim. Transpose and reverse the word to obtain the column claim.

7. Complete scalar catalogue for span five

Let $L\subset\mathbb Z^8$ be the saturated relation lattice, of rank three. Cube relations span $L$ rationally. Otherwise let $L_0$ be their rational span intersected with $\mathbb Z^8$; its rank is at most two. Lift the word to $\mathbb Z^8/L_0$. Every subset equality, and thus every coefficient, is preserved. The low-corank arguments of sections 4–5 assign the lifted target exponents to disjoint frame sets, possibly after canceling common-$J$ factors. Mapping back gives total target rank at most eight, a contradiction.

Three independent cube vectors can be chosen whose reductions form a basis of $L/2L$. Start with any independent cube triple. If its integer span has even index in $L$, a nonempty subset has an even coordinate sum. It has two or three members: a nonzero cube vector is not itself even. Half the sum is an integral cube vector in $L$. Replace one member by that half-sum. Independence is retained and the index is halved. Repetition ends at odd index. Saturation embeds $L/2L$ into $\mathbb F_2^8$, so the three reductions are independent. This is a parity basis, not necessarily an integer basis of $L$.

Writing the cube vectors as $r_1,r_2,r_3$, the first-order condition is

$$ \operatorname{offdiag}(N_j)=\sum_{a=1}^{3}(r_{aj}\bmod2)B_a. $$

Thus the off-diagonal pattern span has dimension at most three. If its dimension is three, the $B_a$ are independent. At each zero-pattern index, all three cube entries are zero over $\mathbb Z$. Every relation therefore vanishes at these indices. With $S$ the noncoordinate indices and $T$ the coordinate indices, $H=H_S\oplus\mathbb Z^T$.

In this dimension-three case, the noncoordinate projectors cannot have a common complete binary flag. Such a flag, followed by projection onto $H_S$, would assign disjoint $S$ frame sums to the diagonals. The characteristic-polynomial argument identifies them with the projected target monomials. Each free $T$ frame belongs to one original target, so the same rank budget would give $9\le8$. This filter is used only at off-diagonal dimension three.

Enumerate the 28 projectors and 19 nonzero patterns. Closing subsets of these patterns under addition gives $1,19,129,363$ possible pattern spaces of dimensions $0,1,2,3$. Coordinate permutations and transpose reduce their projector pools to 67 classes. Coordinate permutations relabel target registers. Transpose reverses factor order and preserves a diagonal target; it is valid because every order is checked. Arbitrary changes of scalar basis are not used to identify full target problems.

For each pool, enumerate all eight-factor multiplicity vectors whose support has that pool's actual off-diagonal span. Retain irreducible supports, row and column distance at least three, and the dimension-three common-flag condition. Identify multiplicities only under the pool's stabilizer. This leaves 2,276 records: 4 in pattern dimension one, 137 in dimension two, and 2,135 in dimension three. No additional subquotient or noncoordinate-count filter is used.

The included catalogue.py selects projectors from all 512 binary matrices. It uses tuple matrices, explicit invariant subspaces, and sorted multisets. Its catalogue was checked against a separate implementation with bit-matrix rank and integer-composition routines. Every record agrees, not only the count; the replay checks the regenerated catalogue digest. Multiplicities $m_1,\ldots,m_k$ have $8!/\prod_i m_i!$ distinct orders. Their total is 21,317,520. This is a complete catalogue of scalar cases after proved reductions, not a bounded search over physical frames.

8. Exhaust all rational frame relation spaces

Fix one ordered scalar word. Expand

$$ P(t)=\prod_{j=1}^{8}\bigl((I+N_j)+t_jN_j\bigr) =\sum_{a\in{0,1}^8}M_a t^a. $$

There are at most 256 subset exponents with ordered binary matrix coefficients. The unknown physical relation space is a rational subspace $R\subset\mathbb Q^8$ of dimension three. A search state is $R_0\subseteq R$, initially zero, generated by at most three cube vectors. Group subset indicators $a,b$ exactly when $a-b\in R_0$ and add their matrix coefficients over $\mathbb F_2$. This gives the image in the group algebra of $\mathbb Z^8/(R_0\cap\mathbb Z^8)$.

If a current exponent group has a nonzero off-diagonal bit, any valid diagonal completion must merge it with another group containing that bit. Branch over every such partner and add the difference of their subset representatives to $R_0$. At least one branch follows every valid completion. Distinct groups have difference outside $R_0$, so each branch raises its dimension. The depth is at most three. Equal canonical relation spaces need be checked only once per word.

Reject a branch if $e_j\in R_0$, since then $A_j=0$. Also reject it when the binary span of its primitive integral relation rows and the first-order off-diagonal coefficient rows has dimension greater than three. Each such row lies in $L/2L$: saturation makes every integral vector of $R$ a member of $L$. This test reduces integral relation vectors, not rational physical frame entries. At dimension three, a remaining off-diagonal coefficient rejects the branch.

When all off-diagonal coefficients vanish, each diagonal entry is a single monomial. Every factor has monomial determinant, so the diagonal entries multiply to a unit. Laurent polynomial units over $\mathbb F_2$ are exactly group monomials. Choose a subset representative $c_w$ of each diagonal target. For every pair of coordinates $i,j$, test whether

$$ c_w\in R_0+\operatorname{span}_{\mathbb Q}(e_i,e_j). \tag{3} $$

If (3) holds for any target, its physical matrix lies in the span of two paid rank-one frames and has rank at most two. Additional relations cannot remove this obstruction. Reject that terminal. A terminal that passed this check would only be a candidate, not a construction.

The rational engine uses primitive integer echelon rows. Their entries are signed minors of at most three cube rows, divided by a common divisor, so their absolute values are at most four. The common denominator in a quotient key divides $\operatorname{lcm}(1,2,3,4)=12$. The terminal test adds two coordinate rows and then one subset row. After reduction, the first added coordinate row has entries at most four in absolute value; the second has entries at most 32. Reducing the subset row by the three original rows gives a coarse bound $8^3$. Reduction by the two added rows gives $8^3\cdot8\cdot64=262{,}144$. Normalization cannot increase these bounds. These bounds also cover search-row insertion and keep all products and differences within signed 32-bit range. No floating-point arithmetic is used.

The rational run checks all 21,317,520 words. It visits 94,392,894 relation states and reaches 415,398 diagonal terminals. Every terminal has the rank-at-most-two obstruction. There are zero candidates. The branching argument therefore excludes every admissible rational relation space for every retained scalar word.

9. A second full implementation with exact finite-field arithmetic

The independent full implementation uses elimination over $\mathbb F_{101}$. In these tests this is an exact representation of the rational calculation, not a probabilistic evaluation.

Each tested matrix has at most three original cube rows, possibly one further cube or binary target row, and at most two coordinate rows. Expand a minor along the coordinate rows. At most four rows with entries of absolute value at most one remain. Hadamard's bound makes the determinant at most 16 in absolute value. Thus it vanishes over $\mathbb Q$ exactly when it vanishes modulo 101. This proves exact ranks and membership for subset collisions, zero frames, and two-frame target spans.

Parity pruning first recovers the rational reduced-echelon rows. Cramer's rule bounds each entry, in lowest terms, by $a/b$ with $|a|\le4$ and $1\le b\le4$. For three cube rows, the determinant bound four follows by maximizing the multilinear determinant at sign matrices: their determinants are divisible by four and bounded by $3\sqrt3$. Smaller minors obey the same bound. Permitted fractions have distinct residues modulo 101, since $|ad-bc|\le32&lt;101$. Clear the recovered denominators and divide by the row gcd to obtain its primitive integral parity. Taking the parity of a finite-field residue itself would be invalid.

The two full implementations each check 2,276 records and 21,317,520 orders. Each reaches 415,398 diagonal terminals and zero survivors. Every per-record word and terminal count agrees. The finite-field engine reports no nonmonomial-diagonal anomaly. It has separate matrix expansion, quotient grouping, and arithmetic representation.

10. Minimum nine and verification scope

Span five was the last possible case, so eight calls are impossible. Fewer calls are excluded by splitting any nonzero rank-one call:

$$ D_N([A])=D_N([A/2])D_N([A/2]). $$

Both new frames remain nonzero and rank one. Repeated splitting would turn any shorter positive-length circuit into an eight-call circuit. Zero calls cannot give invertible frame targets.

Nine calls suffice for every allowed target triple. For each $w$, write

$$ C_w=\sum_{i=0}^{2}(C_we_i)e_i^T $$

and use these three nonzero rank-one frames with scalar projector $E_{ww}$. They combine to the $w$-th target and fix the other registers. This proves the theorem.

The proof depends on the symbolic reductions, complete catalogue, exact collision branching, and completed replay. Neither rational frames nor their coefficient sizes are sampled. The lower-triangular target condition is used in the span-four reduction. The theorem makes no claim for extra registers, other paid primitives, or arbitrary free address maps between calls, and it does not improve the multiplication exponent.

11. Replay

From this directory, run:

python3 replay.py

To retain the generated input and per-case results, run:

python3 replay.py --work-dir /tmp/bit-three-register-replay

The replay requires Python 3.10 or later and Clang or GCC with C++17 and at least 32-bit int. Python uses only the standard library. It regenerates the finite catalogue, compiles and runs both complete relation engines, checks the per-family results, and runs the included controls. The required result is 2,276 scalar families, 21,317,520 orders, 415,398 diagonal terminals, and zero survivors in each full engine.

The nine-call fixture checks $C_1=C_2=C_3=I$. A separate eight-call fixture has noncommuting scalar factors and rational frame span five, but rank-two targets. The Python controls check its exact formal product and these matrix ranks. Another Python control detects an invalid reduction of rational address entries modulo two. The finite-field search core separately accepts a constructed positive control and rejects its one-factor mutation, which forces a rank-two target. The positive core control deliberately uses a rank-two scalar projector. It checks the search core's acceptance path and is not an admissible construction in the theorem's model.

Separate implementations and source review support this computer-assisted proof. They are not Lean verification or a formal verification of the full integer-multiplication theorem.