claimroutineinferred_dep

Coupling tail bounds uniform in history

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

Statement (paper)

There exist fixed constants B≥2B\ge2 and 0<r<10<r<1 such that, for every finite history map HH on PP, under the joint law with an independent uniformly random embedding σ\sigma, the probability that any of Zp,Wp,Zp^,Wp^,(Zqj,Wqj,Dj,Dj−1)j=13Z_p,W_p,Z_{\widehat p},W_{\widehat p},(Z_{q_j},W_{q_j},D_j,D_j^{-1})_{j=1}^3 has embedded absolute value greater than BB is less than 1/1001/100, and the probability that any of the events p≠p^, ∣σ(Zp^−Zp)∣<rp\ne\widehat p,\ |\sigma(Z_{\widehat p}-Z_p)|<r or Dj≠Dl, ∣σ(Dj−Dl)∣<rD_j\ne D_l,\ |\sigma(D_j-D_l)|<r (1≤j<l≤3)(1\le j<l\le3) occurs is less than 1/1001/100 in total.

In plain English

There are fixed constants B≥2B\ge2 and 0<r<10<r<1 such that, for every finite history map HH on PP, under the coupled law with an independent uniform random embedding σ\sigma, all the listed normalized coordinates and edge ratios have embedded absolute value at most BB except with probability under 1/1001/100. Likewise, the events that distinct values among Zp,Zp^Z_p,Z_{\widehat p} or among D1,D2,D3D_1,D_2,D_3 have embedded difference smaller than rr have total probability under 1/1001/100.

Why it's here

The bounded mean heights from the previous claim do not depend on the history. Combining them with the Markov-type tail bounds of the height lemma, a union bound over the finitely many listed quantities gives large-value and near-coincidence bounds that are uniform in HH. This gives the next claim a good set of outcomes where the tests pass and the values stay separated.
Classified routine:
Follows from the history-independent bounded mean heights of the previous claim combined with the Markov-type tail bounds from the height lemma, via a union bound over finitely many quantities.

Uses

claimNormalized coordinates with bounded mean heightslemBasic properties of the height

Used by

claimPositive-probability good outcome exists

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Coupling tail bounds uniform in history" rests on claim-ht-bounded-1
  • info
    inferred_dep
    outline: "Coupling tail bounds uniform in history" rests on ht:height