claimroutineinferred_dep

Each layout round meets layer hypotheses

Each round meets the layer hypotheses, costing O(Tpℓdλ′)O(Tp\ell d^{\lambda'}) in total
main cost term of the transform
Claim·§6.2 A layout on which the parallel layers apply·inside lemCost and accuracy of synthetic transform

Statement (paper)

For every round on a group of DD consecutive chunks with the same chunk index in the remaining chunks, the layer sees the complete address set [P]×[2K]D×[S][P]\times[2^K]^D\times[S] with PS2DK=MPS2^{DK}=M and log⁡2(2M)≤CMp\log_2(2M)\leq C_Mp, and its header E\mathcal E, built from p,d,r,K,wp,d,r,K,w and the round data D,P,S,ρD,P,S,\rho, satisfies ∣E∣≤Cdescp|\mathcal E|\leq C_{\rm desc}p. Hence Proposition  applies to each round, at cost O(Tpdλ′)O(Tpd^{\lambda'}) per round and O(Tpℓdλ′)O(Tp\ell d^{\lambda'}) in total.

In plain English

For every round acting on a group of DD consecutive same-index chunks, the layer sees the full address set [P]×[2K]D×[S][P]\times[2^K]^D\times[S] with PS2DK=MPS2^{DK}=M, log⁡2(2M)≤CMp\log_2(2M)\leq C_Mp, and a header E\mathcal E with ∣E∣≤Cdescp|\mathcal E|\leq C_{\rm desc}p. So the simultaneous-layer proposition applies to each round, at cost O(Tpdλ′)O(Tpd^{\lambda'}) per round and O(Tpℓdλ′)O(Tp\ell d^{\lambda'}) in total.

Why it's here

This checks the hypotheses of the simultaneous-layer proposition for every round on the chunk-grouped layout from the layout-permutation claim, using the constants CMC_M and CdescC_{\rm desc} fixed in the lemma. Its cost bound, multiplied over the rounds, gives the main Tpℓdλ′Tp\ell d^{\lambda'} term in the transform cost and supplies the per-round bound used by the later error-accounting claim.
Classified routine:
A hypothesis-checking step: it verifies that each round on the chunk-grouped layout (from the layout-permutation claim) meets the size and header bounds of the paper's simultaneous-layer proposition, then sums the per-round cost over the rounds. This is bookkeeping on earlier results.

Uses

propSimultaneous Hadamard layer in near-linear timeclaimLayout permutation by moves and chunk exchanges

Used by

claimOne truncation per round bounds error

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Rounds on chunk groups meet simultaneous-layer hypotheses" rests on claim-lem-synthetic-transform-cost-1