claimroutine

Minimal loci are symmetric, not a common unit circle

Claim·§8.2 A complete grid with generic positions·inside propNo algebraic configuration with large heights

Statement (paper)

Among pairs of locus sequences retaining a full number of graph edges, choose one of minimal total dimension, with limiting loci V1,V2⊂U2V_1,V_2\subset\mathcal U^2 of dimensions d1,d2d_1,d_2. Then each limiting curve equation is irreducible over U\mathcal U and has positive degree in both variables, and each limiting curve is invariant under (z,w)↦(w‾,z‾)(z,w)\mapsto(\overline w,\overline z). The loci V1,V2V_1,V_2 are not both the same unit circle (z−u)(w−v)=1(z-u)(w-v)=1 (with v=u‾v=\overline u), and after restricting the graph to these loci and pruning, the remaining graph still has a full count of edges, both vertex sets have size tn1+o(1)t_n^{1+o(1)}, and the minimum degree is tn1−o(1)t_n^{1-o(1)} on both sides.

In plain English

Choose a pair of locus sequences that keeps a full number of graph edges and has minimal total dimension d1+d2d_1+d_2, with limiting loci V1,V2⊂U2V_1,V_2\subset\mathcal U^2. Then each limiting curve has an irreducible equation of positive degree in both variables and is invariant under (z,w)↦(w‾,z‾)(z,w)\mapsto(\overline w,\overline z), V1,V2V_1,V_2 are not both the same unit circle (z−u)(w−v)=1(z-u)(w-v)=1, and the graph restricted to them and pruned still has a full edge count, vertex sets of size tn1+o(1)t_n^{1+o(1)} and minimum degree tn1−o(1)t_n^{1-o(1)} on both sides.

Why it's here

Minimality of the total dimension is used to normalise the loci: any degenerate or non-symmetric curve would give a smaller pair that still keeps enough edges. The hypothesis excluding edges inside a heavy unit circle rules out the common unit-circle case. Pruning then yields a balanced, high-minimum-degree graph on which the later steps (same-curve analysis, generic-point embeddings) can operate.
Classified routine:
A minimality/normalisation step inside the algebraic obstruction proof. It combines a standard descent on total dimension (replacing degenerate or non-symmetric curves by smaller loci), the paper's hypothesis excluding heavy unit circles, and standard graph pruning to reach high minimum degree.

Uses

Nothing else in the paper

Used by

claimSame curve, linear or hyperbola formclaimGeneric points embed function fields

Sources

PaperOpen
Section
§8.2 A complete grid with generic positions
Page
—
Label
—
Line
sections/07-algebra.tex:145
Leannot aligned

Phase 2 aligns this node to a Lean declaration.