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.
, and with equality only when
Statement
Let and let . Then
- the map is injective on , and therefore ;
- ;
- equality holds in part 2 exactly when .
Facts & Assumptions
Given: a family and an index .
By definition, only when and ; otherwise (The down-shift of a set family at a point ).
Proof
Suppose with . Then at least one of or is shifted. If both were shifted, then and adding back gives , impossible. So exactly one is shifted, say , and then because is not shifted. But [F1] says precisely that when is shifted, a contradiction. Therefore is injective.
Since the map is injective, it is a bijection from the finite set onto its image , so .
Every shifted set loses the element and every unshifted set keeps its size, so . Equality holds exactly when no set is shifted, and that is exactly the condition .
Remarks
- The proof uses only the two clauses of the definition. Nothing about shattering enters yet.
Depends on
Used by
- All subsets of [4] of size at most 2: VC dimension 2 and exactly ∑_i≤2C(4, i)=11 members Example
- Applying down-shifts until none changes the family terminates, and the result is closed under taking subsets Lemma
- Every set shattered by Sⱼ(F) is shattered by F Lemma
- Sauer–Shelah: a family on [n] of VC dimension at most d has at most ∑ᵢ₌₀ᵈC(n, i) members 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
- L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §7.5 (standard reference, not scraped)