claimroutineinferred_dep

Kernel factorization extends to k columns

Kernel factorization holds on

k

columns with the same

s_{\rm c}

factors

extends the factorization to any column count

Claim·§3.5 The binary phase interface·inside propComplex network edges factor into translation kernels

Statement (paper)

For each edge

e

with residual basis

\mathcal B_e

and translation kernels

K_{e,v}

(forward or inverse) for

v\in\mathcal B_e

, on

k

columns one has

\bigl(\mathcal C_V\mathcal C_U^{-1}\bigr)^{\otimes k}=\prod_{v\in\mathcal B_e}K_{e,v}^{\otimes k}

. Thus each residual basis vector contributes one factor acting on all

k

columns, and there are

s_{\rm c}

such factors over the network.

In plain English

k

columns, the phase-frame difference

(\mathcal C_V\mathcal C_U^{-1})^{\otimes k}

of each edge equals the product over the residual basis

\mathcal B_e

of the tensor powers

K_{e,v}^{\otimes k}

of the translation kernels (forward or inverse). Each basis vector thus gives one factor acting on all

k

columns, and there are

s_{\rm c}

such factors over the network.

Why it's here

This follows from the single-column factorization because tensor powers respect products,

(AB)^{\otimes k}=A^{\otimes k}B^{\otimes k}

, so the factor count stays

s_{\rm c}

regardless of

k

. It lets the later telescoping argument, which yields

C^{\otimes m}

on the roles, be carried out on any positive number of columns.

Classified routine:

Direct consequence of the single-column factorization (claim-prop-complex-motif-interface-1) via the multiplicativity of tensor powers,

(AB)^{\otimes k}=A^{\otimes k}B^{\otimes k}

Uses

claimPhase-frame difference factors into translation kernels

Used by

claimRoute operators telescope to C^{⊗m}

Sources

PaperOpen

Section: §3.5 The binary phase interface
Page: —
Label: —
Line: sections/03-motifs.tex:616

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Kernel factorization extends to k columns" rests on claim-prop-complex-motif-interface-1