Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Which field each bound is proved over, and what changes when it is replaced
Remarks
Oddtown and Eventown are proved over , and they use only the bilinear form and dimension facts available there. Fisher's inequality and Graham-Pollak are proved over , because each uses the fact that a sum of nonnegative squares vanishes only termwise.
The combinatorial Nullstellensatz is field-generic: the proof uses only the polynomial ring over a field and the strict degree bounds. Cauchy-Davenport is the specialised finite-field application where the field is , and primality is the step that makes that field available and keeps the decisive binomial coefficient nonzero.
The companion-page false statements test these hypotheses alongside sharpness and boundary claims: changing the field or losing positivity breaks some linear arguments, deleting the top coefficient breaks the Nullstellensatz, while the Oddtown and Sauer--Shelah examples test whether their numerical bounds can be strengthened.
Depends on
- Oddtown: distinct $A_1,\dots,A_m\subseteq[n]$ with every $\lvert A_i\rvert$ odd and every $\lvert A_i\cap A_j\rvert$ ($i\ne j$) even satisfy $m\le n$
- Eventown: distinct $A_1,\dots,A_m\subseteq[n]$ with every $\lvert A_i\rvert$ and every $\lvert A_i\cap A_j\rvert$ even satisfy $m\le 2^{\lfloor n/2\rfloor}$
- Fisher's inequality, nonuniform form: distinct nonempty $A_1,\dots,A_m\subseteq[n]$ with $\lvert A_i\cap A_j\rvert=t$ for all $i\ne j$ satisfy $m\le n$
- Graham–Pollak: a complete bipartite decomposition of $K_n$ has at least $n-1$ parts
- Alon's Combinatorial Nullstellensatz: if $\deg f=\sum_it_i$, the coefficient of $x_1^{t_1}\cdots x_n^{t_n}$ in $f$ is nonzero, and $\lvert S_i\rvert>t_i$, then $f(s_1,\dots,s_n)\ne0$ for some $s_i\in S_i$
- Cauchy–Davenport: for $p$ prime and nonempty $A,B\subseteq\mathbb{Z}/p$, $\lvert A+B\rvert\ge\min\{p,\lvert A\rvert+\lvert B\rvert-1\}$
- The standard bilinear form $\langle x,y\rangle=\sum_{i<n}x_iy_i$ on $F^{n}$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
43 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics (standard reference, not scraped)
- N. Alon, Combinatorial Nullstellensatz (standard reference, not scraped)