claimroutineinferred_dep

Direct and left offending ports charged

Charges direct and left offending ports to child witness discrepancies
handles the direct and left-port cases of escape charging
Claim·§9.3 Witness envelopes and escaped paths·inside lemEscape contribution charged to child discrepancies

Statement (paper)

For a direct or left offending port, the contribution is bounded by summing the child's witness discrepancy over its own row and endpoint domain, with only a fixed factor for the bounded number of possible right ports. Projected paths are partitioned by the fixed copy symbols with constant multiplicity, and normalization and preparation dependencies make the same direct witness comparison. In this row-event estimate the validity mask of a candidate from a narrower terminal slice may be dropped, so no factor πa/πt\pi_a/\pi_t is incurred, while the transformed source hit is retained as in Equation .

In plain English

For a direct or left offending port, the escape contribution is bounded by the child's witness discrepancy summed over its own row and endpoint domain, times a fixed factor for the bounded number of right ports. The projected-path, normalization and preparation cases reduce to the same direct witness comparison, with no πa/πt\pi_a/\pi_t factor incurred.

Why it's here

Using the previous claim, which bounds the escape indicator by witness discrepancies at offending ports, this step charges each direct or left offending port to the corresponding child's discrepancy, which has the prescribed bound 2−pmλm2^{-p_m}\lambda_m. Dropping the validity mask of a candidate from a narrower terminal slice avoids a πa/πt\pi_a/\pi_t loss, while the transformed source hit is kept. This leaves only constant multiplicities and the later scale and reset accounting.
Classified routine:
Bookkeeping step inside the proof of the escape lemma: it applies the earlier claim bounding the escape indicator by witness discrepancies and sums those discrepancies over each child's row and endpoint domain, picking up only constant factors for the bounded number of ports and copy symbols.

Uses

claimEscape 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:419
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Direct and left offending ports charged" rests on claim-lem-fp-escape-1