claimroutine

Phase-frame difference factors into translation kernels

Phase-frame difference is a product of scs_{\rm c} translation kernels
single-column core of the kernel factorization
Claim·§3.5 The binary phase interface·inside propComplex network edges factor into translation kernels

Statement (paper)

For each edge of the complex network with tail and head labels U,VU,V, the phase-frame difference CVCU−1\mathcal C_V\mathcal C_U^{-1} is a product, over the vectors vv of an orthonormal basis of the edge residual, of translation kernels aI+bXvaI+bX_v or their inverses, where (Xvf)(x)=f(x+v)(X_vf)(x)=f(x+v). The sum of the basis lengths over the network is sc=Wcm−2N+2Lcs_{\rm c}=W_{\rm c}m-2N+2L_{\rm c}, and the deficit 2N−2Lc2N-2L_{\rm c} is positive.

In plain English

For each edge with tail and head labels U,VU,V, the phase-frame difference CVCU−1\mathcal C_V\mathcal C_U^{-1} is a product of translation kernels aI+bXvaI+bX_v (or their inverses), one for each vector vv in an orthonormal basis of the edge residual. The basis lengths sum over the network to sc=Wcm−2N+2Lcs_{\rm c}=W_{\rm c}m-2N+2L_{\rm c}, and the deficit 2N−2Lc2N-2L_{\rm c} is positive.

Why it's here

This is the single-column core of the complex motif interface. It rests on the residual lemma, which supplies orthonormal bases of the binary residuals and the total length count Wm−2N+2LWm-2N+2L, so each edge's phase change splits into elementary translation kernels. The positive deficit gives the bound sc<Wcms_{\rm c}<W_{\rm c}m that the parent proposition needs, and the multi-column version extends this by tensoring.
Classified routine:
This step follows directly from the residual lemma (lem-motif-residuals), which supplies the orthonormal residual bases and the length count Wm−2N+2LWm-2N+2L. Factoring the phase-frame change into translation kernels along each basis vector is standard bookkeeping applied to that lemma.

Uses

lemEdge residuals and rank budget

Used by

claimKernel factorization extends to k columns

Sources

PaperOpen
Section
§3.5 The binary phase interface
Page
—
Label
—
Line
sections/03-motifs.tex:586
Leannot aligned

Phase 2 aligns this node to a Lean declaration.