Research proof index

Version of boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch with a shared sampled prefix before the real/random branch is chosen.

Four-way disagreement+bad additive bind bound. A merge of probEvent_bind_le_add_of_disagree with the three-world probEvent_bind_le_add_bad_of_disagree: the disagreement set D (a table-level exceptional set, not a bad event) is charged its full mass ε₁; everywhere off D the my-world is bounded by the oc-world plus the per-shared-sample...

Three-way disagreement-aware additive bind bound (hop A). A coupled three-world variant of probEvent_bind_le_add_of_disagree: the three worlds share the sampling computation mx, and at each shared sample x, off the disagreement set D the my-world is bounded by the oc-world plus the per-step slack ε, while on D the ob-world (the bad w...

Prefix-event split for a bind. Prefix points satisfying p are charged in full; off-prefix continuations are charged by the uniform tail bound ε.

Convex prefix-event split for a bind. The off-prefix tail bound ε is charged only on the mass outside p, giving Pr[p] + (1 - Pr[p]) * ε.

First-moment / Markov bound (support-restricted cost). Variant of probEvent_le_tsum_probOutput_mul_cost whose c ≥ 1 hypothesis need only hold on the support of mx.