claimroutine

Normalized coordinates with bounded mean heights

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

Statement (paper)

Suppose S≤S0S\le S_0 on a subsequence. Then there are an edge value d0d_0 and a point p0∈Pp_0\in P such that the normalized coordinates Zx=(zx−zp0)/d0Z_x=(z_x-z_{p_0})/d_0 and Wx=d0(wx−wp0)W_x=d_0(w_x-w_{p_0}) satisfy, for a constant Ch<∞C_h<\infty depending only on S0S_0, Eμ(h(Zp)+h(Wp))+Eκ(h(Zq)+h(Wq))+EE(h(De)+h(De−1))≤Ch\E_\mu(h(Z_p)+h(W_p))+\E_\kappa(h(Z_q)+h(W_q))+\E_E(h(D_e)+h(D_e^{-1}))\le C_h, where De=de/d0D_e=d_e/d_0, and the edge identity (Zp−Zq)(Wp−Wq)=1(Z_p-Z_q)(W_p-W_q)=1 still holds.

In plain English

If the total variation SS stays bounded by S0S_0 along a subsequence, one can choose an edge value d0d_0 and a base point p0p_0 so that the normalized coordinates Zx=(zx−zp0)/d0Z_x=(z_x-z_{p_0})/d_0 and Wx=d0(wx−wp0)W_x=d_0(w_x-w_{p_0}) have mean heights of ZZ, WW and of De±1D_e^{\pm1} (with De=de/d0D_e=d_e/d_0) bounded by a constant ChC_h depending only on S0S_0, while (Zp−Zq)(Wp−Wq)=1(Z_p-Z_q)(W_p-W_q)=1 on every edge.

Why it's here

This step converts the bounded-SS assumption into a concrete normalization where all heights are uniformly bounded, which the unit-distance edge relation survives. The matching lemma supplies a single common label, the transfer lemma passes from edge heights to heights between independent points, and the height properties handle translation, rescaling and sums. The next claim uses these bounds to get tail bounds on the coordinates under a random embedding.
Classified routine:
A normalization step inside the proof of ht-bounded that combines the paper's earlier matching lemma, height-transfer lemma and the standard Weil height properties (translation, inversion, sums) by bookkeeping. No new idea beyond those earlier nodes is needed.

Uses

lemMatching labels are nearly constantlemEdge height cost controls point-pair height costlemBasic properties of the height

Used by

claimCoupling tail bounds uniform in history

Sources

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

Phase 2 aligns this node to a Lean declaration.