How 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.
A finite family of subsets of and its incidence matrix over
Definition
Fix a field and a natural number .
A set family on is a finite list
of pairwise distinct subsets of . Its incidence matrix over is the matrix
whose row indexed by is the incidence vector of .
If , define its Gram matrix to be the matrix whose entry is
so the Gram matrix records all pairings of the incidence vectors at once.
Remarks
- Distinctness of the sets is part of the definition because all the bounds on this page count sets, not repeated rows of a matrix.
Depends on
- The incidence vector $v_A\in F^{n}$ of a subset $A\subseteq[n]$ over a stated field
- The standard bilinear form $\langle x,y\rangle=\sum_{i<n}x_iy_i$ on $F^{n}$
- The vector space $M_{m \times n}(F) := F^{\,m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
- The cardinality $\lvert A\rvert$ of a finite set
Used by
- A k-uniform family on [n] with all pairwise intersections of size t<k has at most n members Corollary
- The n singletons form an Oddtown family, so the bound m≤ n is attained for every n Corollary
- A set family whose incidence vectors are dependent over F₂ and independent over ℝ Counterexample
- L-intersecting families Definition
- The inclusion matrix W_t,k(n) of t-sets against k-sets Definition
- An Oddtown family of four clubs on four citizens, and why a fifth cannot be added Example
- The pairing construction gives an Eventown family of size 2^⌊ n/2⌋ Example
- The seven lines of the Fano plane meet pairwise in one point, and Fisher's bound is tight Example
- If the incidence vectors of A₁,…,Aₘ⊆[n] are linearly independent over F then m≤ n Lemma
- Eventown: distinct A₁,…,Aₘ⊆[n] with every | Aᵢ| and every | Aᵢ∩ Aⱼ| even satisfy m≤ 2^⌊ n/2⌋ Theorem
- Fisher's inequality, nonuniform form: distinct nonempty A₁,…,Aₘ⊆[n] with | Aᵢ∩ Aⱼ|=t for all i≠ j satisfy m≤ n Theorem
- Oddtown: distinct A₁,…,Aₘ⊆[n] with every | Aᵢ| odd and every | Aᵢ∩ Aⱼ| (i≠ j) even satisfy m≤ n Theorem
Dependency tree · two levels
19 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
- J. Matousek, Thirty-three Miniatures, Miniature 3 (standard reference, not scraped)
- L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §2.4 (standard reference, not scraped)