claimroutineinferred_dep

Output error dominated by row-failure indicator

Output error on the escape event is at most a constant times its indicator
reduces output error to the escape indicator
Claim·§9.3 Witness envelopes and escaped paths·inside lemEscape contribution charged to child discrepancies

Statement (paper)

Each output under consideration is bounded and has bounded row support, and the union of the two output supports is bounded by Equation . Hence its entire row error power on Fx\mathcal F_x is at most a fixed multiple of 1Fx\mathbf1_{\mathcal F_x}, so the output error is dominated by the row-failure indicator, with no endpoint sum left on the output side.

In plain English

Each output considered is bounded with bounded row support, and the union of the two output supports is bounded by the buffer row-support estimate. So its full row error power on Fx\mathcal F_x is at most a fixed constant times 1Fx\mathbf1_{\mathcal F_x}, and no endpoint sum remains on the output side.

Why it's here

This lets the output-side error be replaced by the escape indicator Fx\mathcal F_x alone. That indicator is already bounded by witness discrepancies in the previous claim, so the contribution of Fx\mathcal F_x can be charged to child discrepancies to give the bound in the lemma.
Classified routine:
Direct bookkeeping consequence of boundedness of outputs and the buffer row-support bound (eq. buf-row-support): bounded functions with bounded support have error power at most a constant times the failure indicator, which then feeds into the previous claim's escape bound.

Uses

claimEscape indicator bounded by witness discrepancy

Used by

Nothing in the paper

Sources

PaperOpen
Section
§9.3 Witness envelopes and escaped paths
Page
—
Label
—
Line
sections/fingerprints.tex:380
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Output error dominated by row-failure indicator" rests on claim-lem-fp-escape-1