Kruskal-Katona upper-shadow core

This file proves the set-family upper-shadow minimization theorem used by the Boolean-isoperimetry argument.

def BooleanIsoperimetry.layer (N r : ℕ) : Finset (Cube N)

The family of all r-element vertices in the N-cube.

Equations

• BooleanIsoperimetry.layer N r = {x : BooleanIsoperimetry.Cube N | Finset.card x = r}

noncomputable def BooleanIsoperimetry.upperShadowVal (N r t : ℕ) : ℕ

Local numeric upper-shadow value (identical to Shadow.upperShadow but defined here so the Kruskal–Katona core is strictly upstream of Shadow.lean): upperShadowVal N r t = H N (binomPrefix N r + t) - binomPrefix N (r+1).

Equations

• BooleanIsoperimetry.upperShadowVal N r t = BooleanIsoperimetry.H N (BooleanIsoperimetry.binomPrefix N r + t) - BooleanIsoperimetry.binomPrefix N (r + 1)

noncomputable def BooleanIsoperimetry.layerInitSeg (N r t : ℕ) : Finset (Cube N)

The layer-r part of the simplicial initial segment with local size t.

Equations

• BooleanIsoperimetry.layerInitSeg N r t = {x ∈ BooleanIsoperimetry.simplicialInitSeg N (BooleanIsoperimetry.binomPrefix N r + t) | Finset.card x = r}

noncomputable def BooleanIsoperimetry.upperLayerShadow (N r : ℕ) (A : Finset (Cube N)) : Finset (Cube N)

The layer-r + 1 upper shadow of a uniform family in layer r.

Equations

• BooleanIsoperimetry.upperLayerShadow N r A = {x ∈ A.upShadow | Finset.card x = r + 1}

theorem BooleanIsoperimetry.binomPrefix_eq_card_lt (N r : ℕ) : binomPrefix N r = {x : Cube N | Finset.card x < r}.card

theorem BooleanIsoperimetry.mem_layerInitSeg_iff {N r t : ℕ} {x : Cube N} : x ∈ layerInitSeg N r t ↔ Finset.card x = r ∧ rank x < binomPrefix N r + t

theorem BooleanIsoperimetry.layerInitSeg_card {N r t : ℕ} (ht : t ≤ N.choose r) : (layerInitSeg N r t).card = t

theorem BooleanIsoperimetry.upperLayerShadow_sized {N r : ℕ} {A : Finset (Cube N)} {y : Cube N} (hy : y ∈ upperLayerShadow N r A) : Finset.card y = r + 1

theorem BooleanIsoperimetry.neighborhood_binomPrefix {N r : ℕ} (hr : 1 ≤ r) : neighborhood 1 (simplicialInitSeg N (binomPrefix N r)) = simplicialInitSeg N (binomPrefix N (r + 1))

theorem BooleanIsoperimetry.mem_layerInitSeg_iff_rank {N r t : ℕ} {x : Cube N} : x ∈ layerInitSeg N r t ↔ Finset.card x = r ∧ binomPrefix N r ≤ rank x ∧ rank x < binomPrefix N r + t

theorem BooleanIsoperimetry.simplicialInitSeg_decomp {N r t : ℕ} (ht : t ≤ N.choose r) : simplicialInitSeg N (binomPrefix N r + t) = simplicialInitSeg N (binomPrefix N r) ∪ layerInitSeg N r t

theorem BooleanIsoperimetry.upShadow_subset_neighborhood {N r : ℕ} (A : Finset (Cube N)) : (∀ x ∈ A, Finset.card x = r) → A.upShadow ⊆ neighborhood 1 A

theorem BooleanIsoperimetry.hDist_eq_one_of_card_diff {N r : ℕ} {u x : Cube N} (hu : Finset.card u = r) (hx : Finset.card x = r + 1) (hd : hDist u x ≤ 1) : u ⊆ x ∧ Finset.card (x \ u) = 1

theorem BooleanIsoperimetry.card_le_of_hDist_le_one {N r : ℕ} {u x : Cube N} (hu : Finset.card u = r) (hd : hDist u x ≤ 1) : Finset.card x ≤ r + 1

theorem BooleanIsoperimetry.neighborhood_union {N r : ℕ} (A B : Finset (Cube N)) : neighborhood r (A ∪ B) = neighborhood r A ∪ neighborhood r B

theorem BooleanIsoperimetry.upperShadowVal_eq_card_upperLayerShadow {N r t : ℕ} (hr : 1 ≤ r) (ht : t ≤ N.choose r) : upperShadowVal N r t = (upperLayerShadow N r (layerInitSeg N r t)).card

Kruskal--Katona upper-shadow minimization in project language

The next theorem is the single-layer Macaulay/Kruskal--Katona input needed by the Frankl--Füredi paired-compression layer. It is deliberately stated with the real set-family upper shadow upperLayerShadow, not the numerical upperShadow wrapper.

theorem BooleanIsoperimetry.upShadow_eq_upperLayerShadow_of_uniform {N r : ℕ} {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) : A.upShadow = upperLayerShadow N r A

theorem BooleanIsoperimetry.upperLayerShadow_card_eq_shadow_compls {N r : ℕ} {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) : (upperLayerShadow N r A).card = A.compls.shadow.card

theorem BooleanIsoperimetry.layerInitSeg_uniform {N r t : ℕ} (x : Cube N) : x ∈ layerInitSeg N r t → Finset.card x = r

theorem BooleanIsoperimetry.card_le_choose_of_uniform {N r : ℕ} {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) : A.card ≤ N.choose r

theorem BooleanIsoperimetry.cubeToNat_add_compl {N : ℕ} (A : Finset (Fin N)) : cubeToNat A + cubeToNat Aᶜ = cubeToNat Finset.univ

theorem BooleanIsoperimetry.cubeToNat_compl_lt_cubeToNat_compl {N : ℕ} {A B : Finset (Fin N)} : cubeToNat Aᶜ < cubeToNat Bᶜ ↔ cubeToNat B < cubeToNat A

theorem BooleanIsoperimetry.toColex_lt_iff_cubeToNat_lt {N : ℕ} {A B : Finset (Fin N)} : toColex A < toColex B ↔ cubeToNat A < cubeToNat B

theorem BooleanIsoperimetry.toColex_compl_lt_toColex_compl {N : ℕ} {A B : Finset (Fin N)} : toColex Aᶜ < toColex Bᶜ ↔ toColex B < toColex A

theorem BooleanIsoperimetry.layerInitSeg_compls_isInitSeg {N r t : ℕ} : t ≤ N.choose r → Finset.Colex.IsInitSeg (layerInitSeg N r t).compls (N - r)

The complement of a simplicial layer initial segment is a colex initial segment. This is the remaining order-orientation bridge needed to feed the project's layer initial segments into mathlib's lower-shadow Kruskal--Katona theorem.

On a fixed Hamming layer, the project order takes larger binary/colex values first; complementation changes a larger r-set value into a smaller (N-r)-set value. Thus complements of project initial segments are ordinary colex initial segments.

theorem BooleanIsoperimetry.upperLayerShadow_min {N r : ℕ} {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) : (upperLayerShadow N r (layerInitSeg N r A.card)).card ≤ (upperLayerShadow N r A).card

Upper-shadow Kruskal--Katona target. Among all r-uniform families in the N-cube with the same cardinality, the simplicial layer initial segment has minimum upper shadow in layer r+1.

This is the project-language form of the mathlib KK theorem transported from lower shadows through complementation, with the fixed-card simplicial order identified with the corresponding colex/opposite-colex layer order.

theorem BooleanIsoperimetry.upperShadowVal_numeric_min {N r t : ℕ} (hr : 1 ≤ r) (ht : t ≤ N.choose r) {A : Finset (Cube N)} (hA : ∀ x ∈ A, Finset.card x = r) (hcard : A.card = t) : upperShadowVal N r t ≤ (upperLayerShadow N r A).card

Numeric corollary of upperLayerShadow_min: the numerical scaffold upperShadow is bounded by the actual upper shadow of every same-size r-uniform family.