claimroutine
Many complete grids by Jensen
Claim·§8.2 A complete grid with generic positions·inside lemGeneric complete grid with independent coordinates
Statement (paper)
Let the two pruned set sizes be and their edge density be . Then the number of ordered complete -by- grids, allowing repetitions, is at least .
In plain English
If the two pruned vertex sets have sizes and with edge density , then the number of ordered complete -by- grids (repetitions allowed) is at least , which equals .
Why it's here
This is a counting lower bound showing complete grids are plentiful in the pruned graphs, via Jensen's inequality applied to the edge density (the claim's working name). The abundance lets the later diagonal choice pick grids index by index that avoid every countable family of polynomial tests, which gives the algebraic independence in the parent lemma.
Classified routine:
This is the standard Jensen/convexity lower bound on homomorphism counts of complete bipartite graphs K_{N,j} in a bipartite graph of given edge density (the Sidorenko/Kővári–Sós–Turán-type counting argument), applied to the pruned sets.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §8.2 A complete grid with generic positions
- Page
- —
- Label
—- Line
sections/07-algebra.tex:232
Leannot aligned
Phase 2 aligns this node to a Lean declaration.