claimroutineinferred_dep

Route operators telescope to C^{⊗m}

Route operators telescope to C⊗mC^{\otimes m} except on Xa→YaX_a\to Y_a
identifies phase frames along each signed route
Claim·§3.5 The binary phase interface·inside propComplex network edges factor into translation kernels

Statement (paper)

Let ρ\rho be the underlying permutation of the complex roles, exchanging Xa,YaX_a,Y_a and fixing each scratch role. Then in the complex network an input role ww reaches the output role ρ(w)\rho(w) with the sign +1+1 for Xa→YaX_a\to Y_a, −1-1 for Ya→XaY_a\to X_a and +1+1 for each scratch role, and with operator CUsink(ρ(w))CUsource(w)−1\mathcal C_{U_{\mathrm{sink}(\rho(w))}}\mathcal C_{U_{\mathrm{source}(w)}}^{-1}; on kk columns this operator is replaced by its kkth tensor power, with the scalar route sign applied once. Every such route other than Xa→YaX_a\to Y_a joins a zero label (frame II) and a full label (frame C⊗mC^{\otimes m}, since qF(x)=wt⁡(x)q_{\mathcal F}(x)=\operatorname{wt}(x)), so its operator is C⊗mC^{\otimes m}.

In plain English

In the complex network, each input role ww is routed to the output role ρ(w)\rho(w) (swapping XaX_a and YaY_a, fixing scratch roles) with sign +1+1 for Xa→YaX_a\to Y_a and scratch roles and −1-1 for Ya→XaY_a\to X_a. The route operator is CUsink(ρ(w))CUsource(w)−1\mathcal C_{U_{\mathrm{sink}(\rho(w))}}\mathcal C_{U_{\mathrm{source}(w)}}^{-1}, its kkth tensor power on kk columns, and it equals C⊗mC^{\otimes m} for every route except Xa→YaX_a\to Y_a.

Why it's here

The signed-swap lemma fixes which roles are connected and with what sign, and the edge-by-edge kernel factorization on kk columns lets the phase-frame differences telescope along each route to a source-to-sink frame ratio. Every route other than Xa→YaX_a\to Y_a joins a zero label (frame II) to a full label (frame C⊗mC^{\otimes m}), so the ratio is C⊗mC^{\otimes m}; the exceptional Xa→YaX_a\to Y_a route is then repaired by the next claim's diagonal sign corrections.
Classified routine:
A direct bookkeeping consequence of the signed-swap lemma (lem-scalar-motifs) and the preceding k-column kernel factorization claim. The phase-frame differences telescope along each route to a source-to-sink ratio, which equals C^{⊗m} because q_F(x)=wt(x).

Uses

lemForward invocation adds; three-stage swap with signclaimKernel factorization extends to k columns

Used by

claimZ corrections repair the X_a to Y_a route

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Route operators from common-frame identity; C^{⊗m} on most roles" rests on claim-prop-complex-motif-interface-2