claimroutineinferred_dep

Escape indicator bounded by witness discrepancy

Escape indicator is bounded by powers of witness discrepancy at offending ports
turns the escape event into child discrepancies
Claim·§9.3 Witness envelopes and escaped paths·inside lemEscape contribution charged to child discrepancies

Statement (paper)

The indicator of the event Fx\mathcal F_x that an actual endpoint lies outside the envelope is at most a sum, over candidate paths, of nonnegative ss-th powers of the root discrepancy between the actual witness and the clean witness at an offending port, where the actual witness equals one and the clean witness equals zero; this holds also for exposed zero-weight ports, with no lower bound on the candidate's increment assumed.

In plain English

The indicator of the escape event Fx\mathcal F_x (an actual endpoint lying outside the envelope) is at most a sum over candidate paths of nonnegative ss-th powers of the root discrepancy between the actual and clean witnesses at an offending port, where the actual witness is 11 and the clean witness is 00. This also covers exposed zero-weight ports, and no lower bound on the candidate's increment is needed.

Why it's here

This converts the combinatorial escape event into a quantity controlled by the metric bounds on actual–clean child discrepancies, so later claims can charge each offending port to the corresponding child's witness discrepancy. It relies on the atom-port property that smooth witnesses equal one on every exposed entry, including weight-zero ones, so the actual witness is 11 at an offending port while the clean witness is 00, and no increment lower bound is needed.
Classified routine:
A direct bookkeeping step: since the actual witness equals 1 and the clean witness equals 0 at an offending port (by the atom-port property lem-atom-ports), the indicator is bounded by |1-0|^s, and a union over candidate paths gives the sum.

Uses

lemAtom ports: bounded rows with smooth witnesses

Used by

claimOutput error dominated by row-failure indicatorclaimRight-factor charge via actual incoming capclaimDirect and left offending ports charged

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Escape indicator bounded by witness discrepancy" rests on lem:atom-ports