lemmaroutineinferred_dep

Matching labels are nearly constant

Lemma·inc:matching·§2.4 Matching labels and uniformly rare sets

Statement (paper)

For the sequence of edge laws in , there are absolute constants s0>0,C<∞s_0>0,C<\infty and an index after which the following holds uniformly for every pair of label maps ℓP:P→A\ell_P:P\to\mathcal A, ℓQ:Q→A\ell_Q:Q\to\mathcal A into a finite set. If s=PE(ℓP(p)≠ℓQ(q))≤s0, s=\Prob_E\bigl(\ell_P(p)\ne\ell_Q(q)\bigr)\le s_0, some label a0∈Aa_0\in\mathcal A satisfies μ{ℓP≠a0}+κ{ℓQ≠a0}≤Cs. \mu\{\ell_P\ne a_0\}+\kappa\{\ell_Q\ne a_0\}\le Cs. Moreover, for independent p,p′∼μp,p'\sim\mu, at every value of ss, P(ℓP(p)≠ℓP(p′))≤Cs. \Prob\bigl(\ell_P(p)\ne\ell_P(p')\bigr)\le Cs. The analogous statement holds for independent centers of law κ\kappa.

In plain English

For the incidence pieces, if two label maps ℓP,ℓQ\ell_P,\ell_Q on points and centers disagree along a random edge with probability s≤s0s\le s_0, then one label a0a_0 accounts for all but a CsCs mass: μ{ℓP≠a0}+κ{ℓQ≠a0}≤Cs\mu\{\ell_P\ne a_0\}+\kappa\{\ell_Q\ne a_0\}\le Cs. Also, for independent p,p′∼μp,p'\sim\mu, P(ℓP(p)≠ℓP(p′))≤Cs\Prob(\ell_P(p)\ne\ell_P(p'))\le Cs for every ss, and likewise for independent centers of law κ\kappa.

Why it's here

This turns edge-wise label agreement into global near-constancy, using the two-sided expansion and uniform degrees from the incidence piece: a label that is nearly preserved along edges cannot split a large set of points from its neighbors. Later rare-event and height arguments use it to replace labels that rarely mismatch along edges by a single common label, up to a mass of order ss.
Classified routine:
Standard consequence of edge expansion (Cheeger-type argument) in a bipartite graph with controlled degrees: a labeling that is nearly preserved along edges is nearly constant. Here it is a direct bookkeeping consequence of the two-sided expansion and degree control established in the incidence-piece proposition.

Sources

PaperOpen
Section
§2.4 Matching labels and uniformly rare sets
Page
—
Label
inc:matching
Line
sections/01-incidence.tex:356
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: Lemma inc:matching is "For the sequence of edge laws in " (01-incidence.tex:357) and its proof sums and uses .