claimroutineinferred_dep

Z corrections repair the X_a to Y_a route

Z

corrections turn the

X_a\to Y_a

route into

C^{\otimes mk}

repairs the exceptional route so all roles carry

C

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

Statement (paper)

For the pair

X_a\to Y_a

, the route operator is the tensor of

C^{-1}

on the

27

coordinates of

\operatorname{supp}(u_a)

and

C

elsewhere. Conjugating by

Z=\operatorname{diag}(1,-1)

using

C=iZC^{-1}Z

, namely applying

Z_{a,k}

before the network at

X_a

and

i^{27k}Z_{a,k}

after the network at

Y_a

, turns this operator into

C^{\otimes mk}

k

columns. Hence, up to the scalar sign

-1

of the scalar exchange on the physical

X

outputs, which is removed by negating those outputs and sending output role

\rho(w)

back to role

w

, every role, including every scratch role, carries the required forward tensor product

C^{\otimes mk}

In plain English

On the

X_a\to Y_a

route the operator is

C^{-1}

on the 27 coordinates of

\operatorname{supp}(u_a)

and

C

elsewhere. Applying

Z_{a,k}

before the network at

X_a

and

i^{27k}Z_{a,k}

after it at

Y_a

turns this into

C^{\otimes mk}

k

columns. After negating the physical

X

outputs and relabeling output role

\rho(w)

w

, every role, scratch roles included, carries

C^{\otimes mk}

Why it's here

The previous claim left

X_a\to Y_a

as the only route not equal to

C^{\otimes m}

. Since

C=iZC^{-1}Z

, conjugating by

Z

on each of the 27 flipped coordinates turns

C^{-1}

into

C

at the cost of a factor

i

per coordinate, and the

i^{27k}

cancels these factors. The remaining scalar sign

-1

from the signed exchange is absorbed by negating the outputs, which completes the proof of the proposition's telescoping assertion on every role.

Classified routine:

A direct computation: conjugating C^{-1} by Z gives C up to a factor i per coordinate, and these factors are cancelled by i^{27k}, completing the bookkeeping begun in the preceding telescoping claim (claim-prop-complex-motif-interface-3).

Uses

claimRoute operators telescope to C^{⊗m}

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Z sign corrections fix the X_a→Y_a route" rests on claim-prop-complex-motif-interface-3