Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

A second proof of Sauer–Shelah, from the multilinear polynomial space

Statement

If F⊆P([n]) has VC dimension at most d, then

∣F∣≤∑i=0d(ni).

Facts & Assumptions

Given: a family F⊆P([n]) with VC⁡(F)≤d.

[L1]

Over R, if T is not shattered, then on the incidence vectors of F the monomial xT is a linear combination of the monomials xS for S⊊T (If F does not shatter T then xT agrees on {vF:F∈F} with a combination of the xS for S⊊T).

[L2]

For 0≤s≤n, the multilinear monomials of degree at most s span a space of dimension ∑i=0s(ni) on the cube (The functions {0,1}n→F obtained from xT with ∣T∣≤s are linearly independent, so they span a space of dimension ∑i=0s(ni)).

Proof

technique · direct
1.1constructalgebra

Let V be the vector space of all functions F→R. For A⊆[n], put qA(x):=∏i∈Axi∏i∉A(1−xi). At an incidence vector vB, this polynomial is 1 when B=A and 0 otherwise. Therefore every g∈V is represented on the incidence vectors of F by the multilinear polynomial ∑A∈Fg(A)qA, so the restrictions of all squarefree monomials xT span V.

2.1L1step 1.1

If ∣T∣>d, then T is not shattered. Hence [L1] expresses the restriction of xT on F as a combination of the restrictions of the monomials xS with S⊊T. Inducting on ∣T∣ shows that every monomial restriction is in the span of those with degree at most d.

3.1L2step 2.1∎

Therefore the restrictions of the monomials xT with ∣T∣≤d already span V. Put s:=min⁡{d,n}; no subset of [n] has size above n, so this is the same spanning family as the one with ∣T∣≤s. By [L2], there are at most ∑i=0s(ni) of them. If d≤n this is already ∑i=0d(ni); if d>n, then (ni)=0 for i>n, so the same sum is also ∑i=0d(ni). Hence dim⁡V=∣F∣ is at most ∑i=0d(ni). This is the same numerical bound as Sauer–Shelah: a family on [n] of VC dimension at most d has at most ∑i=0d(ni) members, proved by a genuinely different route.

Remarks

  • The shifting proof works with families of sets; this proof works with a span of monomial functions. The shared bound is the conclusion, not the method.

Depends on

Used by

Dependency tree · two levels

50 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