propositionroutineinferred_dep

Organized pair graph with height-controlled ratios

Proposition·ext:pairs·§7.3 Removing common unit circles and choosing witnesses

Statement (paper)

For the incidence graphs and levels constructed above, there are J→∞J\to\infty, a sequence ωt→0\omega_t\to0, and a simple bipartite graph E\mathcal E between two copies of PP, each of size at most t1+o(1)t^{1+o(1)}, with at least t2−o(1)t^{2-o(1)} edges, having the following properties. Each edge (p,r)(p,r) has distinct endpoints and an assigned center q=q(p,r)∈Qq=q(p,r)\in Q with pq,rq∈Epq,rq\in E. Set λpr=zp−zq(p,r)zr−zq(p,r). \lambda_{pr}=\frac{z_p-z_{q(p,r)}}{z_r-z_{q(p,r)}}. No edge has both endpoints on any real unit circle containing at least t9/10t^{9/10} points of PP. Uniformly over the edges and complete rectangles of E\mathcal E, (zp−zr)(wp−wr)=2−λpr−λpr−1,h(λpr)≥J/3,h ⁣(λprλp′r′λpr′λp′r)≤ωtJ.\begin{aligned} (z_p-z_r)(w_p-w_r)&=2-\lambda_{pr}-\lambda_{pr}^{-1}, \\ h(\lambda_{pr})&\ge J/3, \\ h\!\left(\frac{\lambda_{pr}\lambda_{p'r'}} {\lambda_{pr'}\lambda_{p'r}}\right) &\le\omega_tJ. \end{aligned} In the last line all four indicated edges are required to be present; their assigned centers need not agree. The edge ratios λpr\lambda_{pr} are unrelated to the fixed score constant λ\lambda.

In plain English

Along a sequence t→∞t\to\infty there is a simple bipartite graph E\mathcal E between two copies of PP, each side of size at most t1+o(1)t^{1+o(1)}, with at least t2−o(1)t^{2-o(1)} edges. Each edge (p,r)(p,r) has distinct endpoints, a center q(p,r)∈Qq(p,r)\in Q adjacent to both, and no edge lies on a real unit circle with at least t9/10t^{9/10} points of PP. With λpr=(zp−zq)/(zr−zq)\lambda_{pr}=(z_p-z_q)/(z_r-z_q), the edges satisfy (zp−zr)(wp−wr)=2−λpr−λpr−1(z_p-z_r)(w_p-w_r)=2-\lambda_{pr}-\lambda_{pr}^{-1} and h(λpr)≥J/3h(\lambda_{pr})\ge J/3, while every rectangle with all four edges present has h(λprλp′r′/(λpr′λp′r))≤ωtJh(\lambda_{pr}\lambda_{p'r'}/(\lambda_{pr'}\lambda_{p'r}))\le\omega_tJ for some ωt→0\omega_t\to0.

Why it's here

This packages the wedges from the common height band, after deleting those on popular unit circles, into a dense bipartite graph. Every edge has a large ratio height, while every rectangle has a ratio of ratios of small height. Later steps can use this combination of large edge height and small rectangle height to obtain the main power-saving bound. The identity comes from the unit-distance relations at the shared center. The height bounds come from the accurate point profiles in the band, and the circle condition comes from removing wedges on popular circles.
Classified routine:
A packaging step that combines the common height band (ext-band), removal of wedges on popular circles (ext-circles) and the profile approximations (ext-profiles) into a dense bipartite graph. The identity is a direct algebraic consequence of the unit-distance relations at the shared center, and the height bounds follow by the triangle inequality for Weil heights.

Uses

lemCommon height band of accurate wedgeslemPopular unit circles carry few wedgeslemPoint profiles approximate wedge differences

Used by

thmPower-saving bound for planar unit distances

Sources

PaperOpen
Section
§7.3 Removing common unit circles and choosing witnesses
Page
—
Label
ext:pairs
Line
sections/06-extraction.tex:379
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: 06-extraction.tex:443 "By and " uses the profile approximation of Lemma ext:profiles to bound b_{pr}.