claimroutineinferred_dep

Positive-probability good outcome exists

Claim·§4.3 Excluding bounded total variation·inside propTotal variation S cannot stay bounded

Statement (paper)

With the selected history HH used in , with one common prediction p^\widehat p and three independently sampled neighbors q1,q2,q3q_1,q_2,q_3 of pp, there is positive probability that all three acceptance tests pass, all displayed quantities are bounded by BB, and ∣σ(Zp^−Zp)∣≥r|\sigma(Z_{\widehat p}-Z_p)|\ge r and ∣σ(Dj−Dl)∣≥r|\sigma(D_j-D_l)|\ge r for j<lj<l, that is, holds.

In plain English

With the selected history HH, a common prediction p^\widehat p and three independent neighbors q1,q2,q3q_1,q_2,q_3 of pp, there is positive probability that all three acceptance tests pass, every displayed quantity is bounded by BB, and the required separations ∣σ(Zp^−Zp)∣≥r|\sigma(Z_{\widehat p}-Z_p)|\ge r and ∣σ(Dj−Dl)∣≥r|\sigma(D_j-D_l)|\ge r for j<lj<l hold.

Why it's here

This is a union-bound step. The failure probabilities are each small: the tests fail o(1)o(1) of the time by the quantized-test claim with history, and the large-value and near-coincidence events have total probability under 1/1001/100 each by the uniform tail bounds. So the good event has positive probability, and it supplies the outcome that the next claim's determinant and Cramer's rule contradiction needs.
Classified routine:
A standard union bound combining the earlier claims: the quantized-test failure probability from claim-ht-bounded-3 is o(1), and the tail and near-coincidence events are each under 1/100 by the uniform bounds of claim-ht-bounded-2, so the good event has positive probability.

Uses

propIncidence piece with degree and expansion controlclaimCoupling tail bounds uniform in historyclaimQuantized acceptance tests with a history predictor

Used by

claimDeterminant and Cramer's rule contradiction

Sources

PaperOpen
Section
§4.3 Excluding bounded total variation
Page
—
Label
—
Line
sections/03-heights.tex:307
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Positive-probability outcome: tests pass, separated" rests on claim-ht-bounded-2
  • info
    inferred_dep
    outline: "Positive-probability outcome: tests pass, separated" rests on claim-ht-bounded-3