lemmaroutine

Edge height cost controls point-pair height cost

Lemma·ht:transfer·§4.3 Excluding bounded total variation

Statement (paper)

Suppose a probability law

\omega

on two finite vertex sets

P\times Q

, with point marginal

\mu

, has the following property: for all assignments of finite labels to its vertices, two independent

\mu

-points disagree with probability at most

C_0

times the edge disagreement probability. For any coordinate

U:P\cup Q\to\mathcal N

\E_{p,p'\sim\mu}h(U_p-U_{p'}) \le C_1\bigl(\E_{(p,q)\sim\omega}h(U_p-U_q)+1\bigr),

where

C_1

depends only on

C_0

In plain English

If a probability law

\omega

P\times Q

with point marginal

\mu

is such that, for every finite labelling of vertices, two independent

\mu

-points disagree with probability at most

C_0

times the edge disagreement probability, then for any coordinate

U:P\cup Q\to\mathcal N

the average of

h(U_p-U_{p'})

over independent

p,p'\sim\mu

is at most

C_1

times (the average of

h(U_p-U_q)

over edges

(p,q)\sim\omega

, plus 1), with

C_1

depending only on

C_0

Why it's here

This lemma transfers the label-disagreement hypothesis into a bound on the height function

h

, so that the height of differences between arbitrary pairs of points is controlled by the height along edges. This lets later arguments (such as ruling out bounded

S

) pass from small edge heights to small heights between independent points.

Classified routine:

Follows from the label-disagreement (expansion/Cheeger-type) hypothesis by a standard layer-cake argument: apply the hypothesis to dyadic level-set labellings of the height function

h

and sum over scales.

Uses

Nothing else in the paper

Used by

propTotal variation S cannot stay boundedclaimNormalized coordinates with bounded mean heights

Sources

PaperOpen

Section: §4.3 Excluding bounded total variation
Page: —
Label: ht:transfer
Line: sections/03-heights.tex:174

Leannot aligned

Phase 2 aligns this node to a Lean declaration.