claimroutineinferred_dep

Precision gain absorbs scale and reset costs

Scale, variant and reset costs are

2^{O(d)}

and absorbed by precision gain

closes the escape bound with final bookkeeping

Claim·§9.3 Witness envelopes and escaped paths·inside lemEscape contribution charged to child discrepancies

Statement (paper)

At slack

d

, the scale ratios, variants, and immediate path counts cost at most

2^{O(d)}

, and the possible reset factor in Equation is absorbed by the precision gain. Indeed, for admissible row tasks with

u\le f

, Equation gives

p_m\ge p-O(d)+\tfrac12\log_2(f/u)

, and hence

(f/u)^{1/s}2^{-p_m}\le 2^{-p+O(d)}(f/u)^{1/8-1/2}\le 2^{-p+O(d)}

In plain English

At slack

d

, scale ratios, variants and immediate path counts cost at most

2^{O(d)}

, and any reset factor

(f/u)^{1/s}

is absorbed by the precision gain, so each charged child term is at most

2^{-p+O(d)}\lambda_m

Why it's here

This is the final bookkeeping step of the escape lemma: after the previous claims charge each offending port to a child discrepancy

2^{-p_m}\lambda_m

, it shows the leftover factors only cost

2^{O(d)}

. For admissible row tasks with

u\le f

the child precision satisfies

p_m\ge p-O(d)+\tfrac12\log_2(f/u)

, so the reset factor

(f/u)^{1/s}

is beaten by

(f/u)^{-1/2}

, and the bound takes the form

2^{-p}2^{Cd}\lambda_m

in the lemma's sum.

Classified routine:

Bookkeeping inside the escape lemma. It combines the child-precision bound from eq:est-child-precision (p_m >= p - O(d) + (1/2)log(f/u)) with the earlier charging claims, using the elementary inequality (f/u)^{1/8-1/2} <= 1 when u <= f.

Uses

lemRaw difference bounds at slack-d groupsclaimRight-factor charge via actual incoming capclaimDirect and left offending ports charged

Used by

Nothing in the paper

Sources

PaperOpen

Section: §9.3 Witness envelopes and escaped paths
Page: —
Label: —
Line: sections/fingerprints.tex:430

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Precision gain absorbs scale and reset costs" rests on claim-lem-fp-escape-3
info
inferred_dep
outline: "Precision gain absorbs scale and reset costs" rests on claim-lem-fp-escape-4