claimroutineinferred_dep

Right-factor charge via actual incoming cap

Right-port escape charge is ≤

C\frac fu

times right child's witness discrepancy

charges the right factor via the incoming cap

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

Statement (paper)

For a fixed guessed variant and a two-factor path

x\to z\to y

, after the measure-preserving change of variables, the right-port contribution is at most a constant times

\frac1N\mathbb E\sum_x\frac{X_u(x)}u\sum_{z:(x,z)\in\mathcal P^{\mathrm{ac}}_L}Z_f(z)\sum_{y:Y_{a'}(y)=1}|e_R(z,y)|^s \le\frac{K_c}{N u}\mathbb E\sum_z Z_f(z)\sum_{y:Y_{a'}(y)=1}|e_R(z,y)|^s =K_c\frac f u\,\mathfrak d_{f,a'}(W_R^{\mathrm{ac}},W_R^{\mathrm{cl}})^s,

where the middle inequality uses only the incoming cap of the actual left port relation

\mathcal P^{\mathrm{ac}}_L

, and the right task's tuple does not depend on the old source

x

In plain English

For a fixed guessed variant and a two-factor path

x\to z\to y

, after the measure-preserving change of variables, the right-port contribution to the escape charge is at most a constant times

\frac f u\,\mathfrak d_{f,a'}(W_R^{\mathrm{ac}},W_R^{\mathrm{cl}})^s

, the right child's witness discrepancy.

Why it's here

Following the previous claim, which bounds the escape indicator by powers of witness discrepancies, this step charges the right-port term to the right child's discrepancy. The sum over the old source

x

is removed by the incoming cap

K_c

of the actual left port relation, which is possible because the right task's tuple does not depend on

x

. The result is the factor

K_c f/u

times the metric discrepancy, which the later claims then convert into the

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

bounds.

Classified routine:

This is a direct bookkeeping step inside the escape lemma. It swaps the order of summation and uses the incoming cap

K_c

of the left port relation to drop the sum over

x

. That rewrites the term as the right child's witness discrepancy, using the measure-preserving variants from lem-env-variants and the bound from claim-lem-fp-escape-1.

Uses

lemWalk variants avoid storing endpointsclaimEscape indicator bounded by witness discrepancy

Used by

claimPrecision gain absorbs scale and reset costs

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Right-factor charge via actual incoming cap" rests on claim-lem-fp-escape-1