Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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.

Sauer–Shelah: a family on [n] of VC dimension at most d has at most i=0d(ni) members

Statement

Let FP([n]) have VC dimension at most d. Then

Fi=0d(ni).

Facts & Assumptions

Given: a family FP([n]) with VC(F)d.

[L3]

Down-shifting creates no new shattered set (Every set shattered by Sj(F) is shattered by F).

[L4]

A downward-closed family shatters each of its members (If F is closed under taking subsets then F shatters every FF).

Proof

technique · direct
1.1

Apply [L1] to obtain a downward-closed family G by iterated shifting from F.

L1
2.1

By [L2], the shift process preserves the number of sets, so G=F; and by [L3], the VC dimension does not increase, so VC(G)d.

L2L3step 1.1
3.1

Because G is downward closed, [L4] says that every member of G is shattered. Since VC(G)d, every member of G therefore has size at most d.

L4step 2.1
4.1

So G is a subset of the union of the layers [[n]]0,,[[n]]d, whose total size is i=0d(ni) by [F1]. Using step 2.1, the same bound holds for F.

F1step 2.1step 3.1

Remarks

  • The argument is purely combinatorial. The page later gives a second proof through multilinear polynomials, but this theorem itself uses only shifting.

Depends on

Used by

Dependency tree · two levels

29 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