claimroutineinferred_dep

Recurrence total cost and conversion to H

Claim·§5.4 An explicit guard-width bound·inside propSimultaneous Hadamard layer in near-linear time

Statement (paper)

The row construction and the recurrence analysis give total time

O(Vd^{\lambda'})

on fixed tapes, including all padded and auxiliary streams, and Equation converts the resulting exact

C

-layer to

\mathcal H

In plain English

The row construction together with the recurrence analysis gives total running time

O(Vd^{\lambda'})

on a fixed number of tapes, counting all padded and auxiliary streams. The identity in Equation (phase-butterfly-layer) then converts the resulting exact

C

-layer into the layer

\mathcal H

Why it's here

This step closes the time bound of the proposition by summing the packed basis-change costs, which the uniform near-linear bound makes available with one common constant. It then uses the telescoping of complex-network edge frames to

C^{\otimes m}

to turn the computed

C

-layer into

\mathcal H

, so the next claim can analyze exact guarded evaluation of

\mathcal H z

Classified routine:

Bookkeeping step: sums the uniformly near-linear packed basis-change costs from the preceding claim over the recurrence, then applies the paper's phase-butterfly identity (telescoping edge frames via prop-complex-motif-interface) to convert the C-layer to H.

Uses

claimPacked basis changes cost uniformly near-linearpropComplex network edges factor into translation kernels

Used by

claimGuarded evaluation with single final truncation

Sources

PaperOpen

Section: §5.4 An explicit guard-width bound
Page: —
Label: —
Line: sections/05-layers.tex:974

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Recurrence gives O(Vd^λ') and converts C layer to H_0" rests on claim-prop-simultaneous-layer-2
info
inferred_dep
outline: "Recurrence gives O(Vd^λ') and converts C layer to H_0" rests on prop:complex-motif-interface