Upper-shadow and Macaulay layer

This file connects Kruskal-Katona upper-shadow estimates to the Macaulay exchange inequalities used in Harper's theorem.

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

Upper-shadow / excess function. For a count binomPrefix N r + t (a full Hamming ball of radius r-1 plus t vertices of layer r), this is the number of vertices the closed neighbourhood adds beyond the full ball of radius r, i.e. the size of the upper shadow of the first t vertices of layer r.

Equations

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

theorem BooleanIsoperimetry.H_shadow_closed_form (N r t : ℕ) (hr : 1 ≤ r) : H N (binomPrefix N r + t) = binomPrefix N (r + 1) + upperShadow N r t

Macaulay closed form for H on a partial layer. For 1 ≤ r, the boundary of a full ball of radius r-1 plus the first t vertices of layer r equals the next full ball binomPrefix N (r+1) plus the upper shadow upperShadow N r t. This is sorry-free: it is just the definition of upperShadow together with the monotonicity bound binomPrefix N (r+1) = H N (binomPrefix N r) ≤ H N (binomPrefix N r + t).

theorem BooleanIsoperimetry.upperShadow_zero (N r : ℕ) (hr : 1 ≤ r) : upperShadow N r 0 = 0

The upper shadow of an empty partial layer is empty.

theorem BooleanIsoperimetry.upperShadow_mono (N r : ℕ) {t t' : ℕ} (h : t ≤ t') : upperShadow N r t ≤ upperShadow N r t'

The upper shadow is monotone in the partial-layer parameter t.

theorem BooleanIsoperimetry.upperShadow_full (N r : ℕ) (hr : 1 ≤ r) : upperShadow N r (N.choose r) = N.choose (r + 1)

A complete layer has upper shadow equal to the full next layer Nat.choose N (r+1): the upper shadow of all of layer r is all of layer r+1.

theorem BooleanIsoperimetry.upperShadow_le_choose (N r t : ℕ) (hr : 1 ≤ r) (ht : t ≤ N.choose r) : upperShadow N r t ≤ N.choose (r + 1)

Kruskal–Katona/Macaulay upper bound: the upper shadow of a partial layer never exceeds the full next layer. Sorry-free monotone consequence of upperShadow_full.

The Macaulay exchange leaf and its two shadow-sum corollaries

The genuine numerical heart of the positive-cascade Harper step is the regime-free max-form exchange theorem below. It says that for p + q = a + b with (p, q) the canonical cascade split of the common total, the canonical cross-boundary cost is no larger than the cost of the arbitrary split (a, b).

The two public H_shadow_* statements are max-free regime corollaries of this single exchange theorem: the positive canonical split collapses the left maxs to H N p + H N q, and the LE/GT hypotheses collapse the right maxs to the advertised sums. Via H_shadow_closed_form (see H_shadow_LE_sum_as_upperShadow) these corollaries are still the upper-shadow sum comparisons used by the Frankl–Füredi/Kruskal–Katona calculation.

theorem BooleanIsoperimetry.H_exchange_max_form_pos {N p q a b : ℕ} (hpq : CascadeSplit N (a + b) p q) (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) (_hq_pos : 1 ≤ q) : max (H N p) q + max (H N q) p ≤ max (H N a) b + max (H N b) a

Positive Frankl–Füredi / Macaulay exchange step. For a positive canonical cascade split (p, q) of a + b at level N, the canonical cross-boundary cost is at most the cross-boundary cost of the arbitrary split (a, b).

This is the remaining PDF-layer theorem: the paired Up/Down compression plus the Macaulay/Kruskal–Katona shadow comparison in the nondegenerate branch. The q = 0 branch is proved separately below by direct cascade arithmetic, and the full exchange theorem is assembled from the two branches.

theorem BooleanIsoperimetry.last_not_mem_image_castSucc {n : ℕ} (x : Cube n) : Fin.last n ∉ Finset.image Fin.castSucc x

The top coordinate Fin.last n never lies in the image of Fin.castSucc, since Fin.castSucc i < Fin.last n always.

theorem BooleanIsoperimetry.embed0_injective {n : ℕ} : Function.Injective embed0

embed0 is injective: it is Finset.image along the injective Fin.castSucc.

theorem BooleanIsoperimetry.embed1_injective {n : ℕ} : Function.Injective embed1

embed1 is injective: it inserts the top coordinate into the image of the injective Fin.castSucc, and that top coordinate is never already present.

theorem BooleanIsoperimetry.slice0_union_embed {N a b : ℕ} : slice0 (Finset.image embed0 (simplicialInitSeg N a) ∪ Finset.image embed1 (simplicialInitSeg N b)) = simplicialInitSeg N a

theorem BooleanIsoperimetry.slice1_union_embed {N a b : ℕ} : slice1 (Finset.image embed0 (simplicialInitSeg N a) ∪ Finset.image embed1 (simplicialInitSeg N b)) = simplicialInitSeg N b

theorem BooleanIsoperimetry.disjoint_embed {N a b : ℕ} : Disjoint (Finset.image embed0 (simplicialInitSeg N a)) (Finset.image embed1 (simplicialInitSeg N b))

theorem BooleanIsoperimetry.card_embed0 {N a : ℕ} (ha : a ≤ 2 ^ N) : (Finset.image embed0 (simplicialInitSeg N a)).card = a

theorem BooleanIsoperimetry.card_embed1 {N b : ℕ} (hb : b ≤ 2 ^ N) : (Finset.image embed1 (simplicialInitSeg N b)).card = b

theorem BooleanIsoperimetry.H_shadow_LE_sum {N a b p q : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) (hcasc : CascadeSplit N (a + b) p q) (hq_pos : 1 ≤ q) (hba : b ≤ a) (hcase : a ≤ H N b) : H N p + H N q ≤ H N a + H N b

Macaulay shadow-sum leaf, LE regime. For the canonical cascade split (p, q) of a + b with b ≤ a and a ≤ H N b (the LE regime in which the outer boundary maxs collapse to H N a + H N b), the canonical boundary sum is minimal. Via H_shadow_closed_form this is the upper-shadow comparison upperShadow N rp tp + upperShadow N rq tq ≤ upperShadow N ra ta + upperShadow N rb tb modulo whole layers (see H_shadow_LE_sum_as_upperShadow). This is the genuine Kruskal–Katona/Macaulay leaf; it is true (verified against the exact cascade model of H, all split dimensions N ≤ 4) but its proof is the Frankl–Füredi shadow calculation, which is now fully formalized and sorry-free.

theorem BooleanIsoperimetry.H_shadow_GT_sum {N a b p q : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) (hcasc : CascadeSplit N (a + b) p q) (hq_pos : 1 ≤ q) (hba : b ≤ a) (hcase : H N b < a) : H N p + H N q ≤ H N a + a

Macaulay shadow-sum leaf, GT regime. For the canonical cascade split (p, q) of a + b with b ≤ a and H N b < a (the GT/slack regime in which the outer boundary max (H N b) a collapses to a), the canonical boundary sum is bounded by H N a + a. As with the LE leaf, via H_shadow_closed_form this is a sum comparison of upperShadow quantities with the GT slack a. This is the genuine GT shadow-deficit leaf of Frankl–Füredi; true (cascade-model verified) but now fully formalized and sorry-free.

theorem BooleanIsoperimetry.H_exchange_max_form_q_zero {N a b p : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) (hp : p ≤ 2 ^ N) (hb_le_a : b ≤ a) (hpq : p = a + b) (hcasc : CascadeSplit N (a + b) p 0) : H N p + p ≤ max (H N a) b + max (H N b) a

theorem BooleanIsoperimetry.H_exchange_max_form {N s p q a b : ℕ} (hpq : CascadeSplit N s p q) (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) (hab : a + b = s) : max (H N p) q + max (H N q) p ≤ max (H N a) b + max (H N b) a

Regime-free max-form exchange theorem, assembled from the proved degenerate q = 0 branch and the positive Frankl–Füredi/Macaulay leaf.

theorem BooleanIsoperimetry.harper_split_min {n x y : ℕ} (hx : x ≤ 2 ^ n) (hy : y ≤ 2 ^ n) : H (n + 1) (x + y) ≤ max (H n x) y + max (H n y) x

Scalar Frankl–Füredi / Macaulay crux (★). The single inductive step of Harper's vertex-isoperimetric theorem: for capacity-bounded slice masses x, y ≤ 2^n, the boundary of the canonical split of x + y at level n+1 is at most the cross-slice boundary functional max (H n x) y + max (H n y) x.

This is the genuine remaining obstruction — the Frankl–Füredi paired-compression / Kruskal–Katona–Macaulay shadow comparison — now stated as a pure scalar inequality in three naturals. It is strictly narrower than the family-level harper_vertex_iso below (which is proved from it via the slice induction), and is equivalent (through H_succ_cascade) to the finite-checked max-form exchange step.

theorem BooleanIsoperimetry.harper_vertex_iso (N : ℕ) (A : Finset (Cube N)) : H N A.card ≤ (neighborhood 1 A).card

Harper's vertex-isoperimetric theorem (master form). For every finite family A of vertices of the N-cube, the simplicial initial segment of the same size has a closed 1-neighbourhood no larger than A's; equivalently the boundary function H N A.card lower-bounds (neighborhood 1 A).card.

This is the Frankl–Füredi/PDF master statement, generalising the initial-segment identity H to arbitrary families. It is proved here by the standard slice induction on N: neighborhood_succ decomposes the boundary across the two coordinate slices, the induction hypothesis bounds each slice, and the single cross-slice crux is harper_split_min.

theorem BooleanIsoperimetry.H_shadow_LE_sum_as_upperShadow {N a b p q ra rb rp rq ta tb tp tq : ℕ} (hra : 1 ≤ ra) (hrb : 1 ≤ rb) (hrp : 1 ≤ rp) (hrq : 1 ≤ rq) (hae : a = binomPrefix N ra + ta) (hbe : b = binomPrefix N rb + tb) (hpe : p = binomPrefix N rp + tp) (hqe : q = binomPrefix N rq + tq) : H N p + H N q ≤ H N a + H N b ↔ binomPrefix N (rp + 1) + upperShadow N rp tp + (binomPrefix N (rq + 1) + upperShadow N rq tq) ≤ binomPrefix N (ra + 1) + upperShadow N ra ta + (binomPrefix N (rb + 1) + upperShadow N rb tb)

Layer-sum bridge (sorry-free). Given the Macaulay layer decompositions of a, b, p, q (each a full ball of radius rx - 1 plus tx vertices of layer rx, with 1 ≤ rx), the LE/GT boundary sums are exactly the corresponding sums of binomPrefix whole-layer terms plus upperShadow partial-layer terms. This makes precise that H_shadow_LE_sum / H_shadow_GT_sum are pure upper-shadow (Kruskal–Katona/Macaulay) inequalities, and lets the leaves be checked empirically by tabulating upperShadow. It is a direct consequence of H_shadow_closed_form, hence sorry-free.