claimroutineinferred_dep

Full procedures include layout conjugation

Conjugating by LL gives LBFt−LBF^-_t and Ft+B−1L−1F^+_tB^{-1}L^{-1} procedures
identifies the full operators and storage positions
Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

Writing D−=BFt−\mathcal D_-=BF_{\boldsymbol t}^- and D+=Ft+B−1\mathcal D_+=F_{\boldsymbol t}^+B^{-1} for the exact logical forward and opposite procedures, executing each operation on named slots after LL conjugates it by LL. Hence the full exact operator of the forward procedure is (LD−L−1)L=LBFt−(L\mathcal D_-L^{-1})L=LBF_{\boldsymbol t}^-, and that of the opposite procedure is L−1(LD+L−1)=Ft+B−1L−1L^{-1}(L\mathcal D_+L^{-1})=F_{\boldsymbol t}^+B^{-1}L^{-1}. In particular, the forward entry with frequency address jj is stored at L(Bj)L(Bj).

In plain English

Conjugating each logical operation by the layout permutation LL makes the forward procedure realize LBFt−LBF_{\boldsymbol t}^- and the opposite procedure realize Ft+B−1L−1F_{\boldsymbol t}^+B^{-1}L^{-1}. In particular, the forward entry with frequency address jj ends up stored at position L(Bj)L(Bj).

Why it's here

The parallel layers act on named slots of the layout produced by LL, so each logical step D±\mathcal D_\pm is run as LD±L−1L\mathcal D_\pm L^{-1}. Composing this with the single application of LL (or L−1L^{-1}) from the layout-permutation claim makes the conjugating L−1LL^{-1}L factors cancel, which gives the full operators and the storage location of each output entry that the cost lemma's later steps need.
Classified routine:
Direct bookkeeping: conjugating each logical step by the layout permutation L and composing with the single application of L from the earlier layout-permutation claim, so the intermediate L^{-1}L factors cancel.

Uses

claimLayout permutation by moves and chunk exchangeslemRoots of unity orthogonality and inverse transforms

Used by

Nothing in the paper

Sources

PaperOpen
Section
§6.2 A layout on which the parallel layers apply
Page
—
Label
—
Line
sections/06-transforms.tex:422
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Full procedures implement LBF^- and F^+B^{-1}L^{-1}" rests on claim-lem-synthetic-transform-cost-1
  • info
    inferred_dep
    outline: "Full procedures implement LBF^- and F^+B^{-1}L^{-1}" rests on lem:synthetic-characters