证明
Lemma 18 ([Path lists and their encounter bound]). For every original witness…Lemma 17 ([Stability under every cut replacement]). Fix feasible endpoint and…观点
The preceding inner-integral comparison proves the displayed bound on every feasible fiber. On an infeasible fiber the original contribution is zero. We explain the remaining bookkeeping to specify precisely how the full integral is recovered. Keep L,B_ l ,B_ j j_n fixed and integrate the extensions in j_n, d as in the displayed ledger. Whenever the original domain is nonempty, all the nearest-kernel factorizations apply. Restore the baseline kernels from , then integrate the fixed paths. Finally drop the remaining cut and nearest-lift restrictions from the baseline integral by positivity, obtaining. Its predicates are measurable functions of the baseline paths, specified by finite cell algorithms. This use of the conditional comparison is valid pointwise at the fixed data: a positive original inner integral has a witness, and otherwise the required upper bound is automatic.