Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31
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.

Local LYM inequality comparing a uniform family with its upper shadow

Statement

Let AA be an nn-element set, let 0≤k<n0\le k<n, and let F⊆[A]k\mathcal F\subseteq[A]^k. Then

∣F∣(nk)≤∣∇F∣(nk+1).\frac{|\mathcal F|}{\binom nk}\le\frac{|\nabla\mathcal F|}{\binom n{k+1}}.

Equality holds exactly when every T∈∇FT\in\nabla\mathcal F contains all of its kk-element subsets in F\mathcal F.

Facts & Assumptions

Given: An nn-element set AA, a natural k<nk<n, a family F⊆[A]k\mathcal F\subseteq[A]^k, and its upper shadow ∇F\nabla\mathcal F.

[F1]

The upper shadow consists of the (k+1)(k+1)-sets containing at least one member of F\mathcal F (The lower and upper shadows of a uniform set family).

[L1]

A disjoint union of finite sets has cardinality the sum of the cardinalities; cardinality is transported by a bijection; and if k+t=nk+t=n then t=n−kt=n-k (The sum rule: a finite disjoint union is finite with ∣A∪B∣=∣A∣+∣B∣\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and ∣⋃i∈IAi∣=∑i∈I∣Ai∣\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert, and a sum over a finite index set splits along a partition, The cardinality ∣A∣\lvert A\rvert of a finite set, Injection, surjection, bijection, Order on the natural numbers, Addition is cancellative).

[L2]

The binomial closed formula implies (nk)(n−k)=(nk+1)(k+1)\binom nk(n-k)=\binom n{k+1}(k+1) for k<nk<n ((nk) k! (n−k)!=n!\binom{n}{k}\,k!\,(n-k)! = n! for k≤nk \le n; hence (nk) k!=nk‾\binom{n}{k}\,k! = n^{\underline{k}}, the quotient n!/(k!(n−k)!)n!/(k!(n-k)!) is a natural number, and (nk)=(nn−k)\binom{n}{k} = \binom{n}{n-k}, The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=∣[n]k∣\binom{n}{k} := \lvert [n]^{k}\rvert).

Proof

technique · direct
1.1

Fix S∈[A]kS\in[A]^k. Since AA is the disjoint union of SS and A∖SA\setminus S, [L1] gives ∣A∖S∣=n−k|A\setminus S|=n-k. The map x↦S∪{x}x\mapsto S\cup\{x\} is a bijection from A∖SA\setminus S to the (k+1)(k+1)-subsets of AA properly containing SS: its inverse sends such a set to its unique element outside SS. Thus every S∈[A]kS\in[A]^k has exactly n−kn-k one-element extensions.

givenL1construct
1.2

Fix T∈[A]k+1T\in[A]^{k+1}. The map y↦T∖{y}y\mapsto T\setminus\{y\} is a bijection from TT to its kk-element subsets, with inverse sending a kk-subset to its unique omitted element. Hence TT has exactly k+1k+1 such subsets.

givenL1construct
2.1

Count pairs (S,T)(S,T) with S∈FS\in\mathcal F, T∈[A]k+1T\in[A]^{k+1}, and S⊂TS\subset T. By step 1.1, there are ∣F∣(n−k)|\mathcal F|(n-k) pairs.

step 1.1
2.2

Every second coordinate lies in ∇F\nabla\mathcal F, and step 1.2 shows that a fixed T∈∇FT\in\nabla\mathcal F contains at most k+1k+1 members of F\mathcal F. Thus the same number of pairs is at most ∣∇F∣(k+1)|\nabla\mathcal F|(k+1).

step 1.2F1
3.1

Steps 2.1 and 2.2 give ∣F∣(n−k)≤∣∇F∣(k+1)|\mathcal F|(n-k)\le|\nabla\mathcal F|(k+1). Using [L2] and dividing by the positive binomial coefficients gives the stated normalized inequality.

step 2.1step 2.2L2algebra
3.2

Equality in step 2.2 holds precisely when every T∈∇FT\in\nabla\mathcal F contributes all of its k+1k+1 possible kk-subsets, which is precisely the equality condition in the Statement.

step 2.2F1
4.1

Therefore the normalized local LYM inequality holds, with the asserted equality characterization.

step 3.1step 3.2∎

Remarks

Applying the same result to complements gives the equivalent lower-shadow form

∣∂F∣(nk−1)≥∣F∣(nk)\frac{|\partial\mathcal F|}{\binom n{k-1}} \ge \frac{|\mathcal F|}{\binom nk}

for 1≤k≤n1\le k\le n.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 77 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources