propositionroutine

Bit network matrix interface and rank sum

Bit network swaps via XOR gates with rank sum sb<Wbms_{\rm b}<W_{\rm b}m
supplies bit circuit with rank sum for shear interchange
Proposition·prop:bit-motif-interface·§3.4 The rational matrix interface

Statement (paper)

The bit network has WbW_{\rm b} wires, uses only pointwise XOR gates, and sends its input vector to the permutation ρ\rho of that vector. Its rational matrices are common to all incidences of a gate and obey Msink(ρ(w))−Msource(w)=Imfor every input role w. M_{\mathrm{sink}(\rho(w))}-M_{\mathrm{source}(w)}=I_m \quad\text{for every input role }w. The sum of the rational ranks of all edge differences is sb=∑erank⁡Q(Mhead(e)−Mtail(e))=Wbm−N+2Lb=177176569088785861287000000<Wbm.\begin{aligned} s_{\rm b} &=\sum_{e}\operatorname{rank}_{\mathbb Q} (M_{\mathrm{head}(e)}-M_{\mathrm{tail}(e)})\\ &=W_{\rm b}m-N+2L_{\rm b} =177176569088785861287000000<W_{\rm b}m. \end{aligned}

In plain English

The bit network has WbW_{\rm b} wires, uses only pointwise XOR gates, and maps its input vector to the permutation ρ\rho of that vector. Its rational matrices are shared across all incidences of a gate, satisfy Msink(ρ(w))−Msource(w)=ImM_{\mathrm{sink}(\rho(w))}-M_{\mathrm{source}(w)}=I_m for every input role ww, and the total rational rank of the edge differences is sb=Wbm−N+2Lb=177176569088785861287000000<Wbms_{\rm b}=W_{\rm b}m-N+2L_{\rm b}=177176569088785861287000000<W_{\rm b}m.

Why it's here

This packages the bit network into the form the rational-matrix framework needs: the net effect is the swap permutation from the scalar motif lemma, with identity differences along the input-to-output pairing. The rank sum comes from the edge residual lemma's rank-budget identity, and the strict bound sb<Wbms_{\rm b}<W_{\rm b}m is the numerical fact that later steps, such as the shear-frame circuit argument, rely on.}
Classified routine:
Direct packaging of the scalar motif lemma (three-stage XOR swap) and the edge residual rank-budget identity into the rational-matrix interface. The rank sum is an explicit numerical evaluation of that identity.

Uses

lemForward invocation adds; three-stage swap with signlemEdge residuals and rank budget

Used by

claimCircuit on role streams realizes shear

Sources

PaperOpen
Section
§3.4 The rational matrix interface
Page
—
Label
prop:bit-motif-interface
Line
sections/03-motifs.tex:492
Leannot aligned

Phase 2 aligns this node to a Lean declaration.