Scalar Macaulay minimization

This file packages the set-family compression and shadow estimates into scalar Macaulay minimization lemmas consumed by the final Harper theorem.

theorem BooleanIsoperimetry.macaulay_extremal_pos_step_LE (n : ℕ) : (∀ m < n, ∀ (x y : ℕ), x ≤ 2 ^ m → y ≤ 2 ^ m → H (m + 1) (x + y) ≤ max (H m x) y + max (H m y) x) → ∀ {a b p q : ℕ} (ha : a ≤ 2 ^ n) (hb : b ≤ 2 ^ n), p ≤ 2 ^ n → q ≤ 2 ^ n → p + q = a + b → ∀ (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

Positive-cascade Case-I (LE) Macaulay shadow-sum leaf. Now a proved corollary of the set-family shadow leaf H_shadow_LE_sum (which collapses the Frankl–Füredi paired-compression cost via H_exchange_max_form_pos). The hypotheses ih, hp, hq, hpq are retained to keep the call site signature stable; the content is entirely the shadow-sum comparison.

theorem BooleanIsoperimetry.macaulay_extremal_pos_step_GT (n : ℕ) : (∀ m < n, ∀ (x y : ℕ), x ≤ 2 ^ m → y ≤ 2 ^ m → H (m + 1) (x + y) ≤ max (H m x) y + max (H m y) x) → ∀ {a b p q : ℕ} (ha : a ≤ 2 ^ n) (hb : b ≤ 2 ^ n), p ≤ 2 ^ n → q ≤ 2 ^ n → p + q = a + b → ∀ (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

Positive-cascade Case-II (GT) Macaulay shadow-sum leaf. Now a proved corollary of the set-family GT shadow-deficit leaf H_shadow_GT_sum.

theorem BooleanIsoperimetry.macaulay_extremal_pos_step (n : ℕ) (ih : ∀ m < n, ∀ (x y : ℕ), x ≤ 2 ^ m → y ≤ 2 ^ m → H (m + 1) (x + y) ≤ max (H m x) y + max (H m y) x) {a b p q : ℕ} (ha : a ≤ 2 ^ n) (hb : b ≤ 2 ^ n) (hp : p ≤ 2 ^ n) (hq : q ≤ 2 ^ n) (hpq : p + q = a + b) (hcasc : CascadeSplit n (a + b) p q) (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-cascade max-form wrapper. Sorry-free modulo the two oriented Macaulay shadow-sum leaves macaulay_extremal_pos_step_LE and macaulay_extremal_pos_step_GT.

theorem BooleanIsoperimetry.macaulay_bc_min (n : ℕ) (ih : ∀ m < n, ∀ (x y : ℕ), x ≤ 2 ^ m → y ≤ 2 ^ m → H (m + 1) (x + y) ≤ max (H m x) y + max (H m y) x) {a b p q : ℕ} (ha : a ≤ 2 ^ n) (hb : b ≤ 2 ^ n) (hp : p ≤ 2 ^ n) (hq : q ≤ 2 ^ n) (hpq : p + q = a + b) (hcasc : CascadeSplit n (a + b) p q) : max (H n p) q + max (H n q) p ≤ max (H n a) b + max (H n b) a

Scalar boundary-cost minimization at a fixed cascade split. Given the canonical cascade split (p, q) of a + b at level n, the canonical split minimizes the symmetric max-form boundary cost. The q = 0 branch is discharged sorry-free by Macaulay.harper_bc_min_q_zero_core, and the q ≥ 1 branch by macaulay_extremal_pos_step.

theorem BooleanIsoperimetry.harper_macaulay_min {N a b : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : H (N + 1) (a + b) ≤ max (H N a) b + max (H N b) a

Scalar Macaulay minimization — the arithmetic core of Harper. For any slice sizes a, b ≤ 2 ^ N, the boundary cost H (N+1) (a+b) of the canonical cascade split of the total mass a + b is minimal among all ways of distributing that mass into two N-dimensional slices of sizes a and b.

Proved by strong induction on the dimension N (the Frankl–Füredi recursion): H_succ_cascade reduces the LHS to max (H N p) q + max (H N q) p, and macaulay_bc_min closes it using the lower-dimensional induction hypothesis.

theorem BooleanIsoperimetry.initialSlicePair_harper_bound {N a b : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : (neighborhood 1 (simplicialInitSeg (N + 1) (a + b))).card ≤ (neighborhood 1 (initialSlicePair N a b)).card

Embedded-pair Harper/Macaulay shadow comparison. Among families in Q_{N+1} with a+b vertices, the simplicial initial segment has closed neighborhood no larger than the particular two-slice family consisting of canonical initial segments of sizes a and b. Sorry-free corollary of harper_macaulay_min via the cardinality bridge neighborhood_initialSlicePair_card.

theorem BooleanIsoperimetry.harper_compression_descent {N : ℕ} (A : Finset (Cube N)) : (neighborhood 1 (simplicialInitSeg N A.card)).card ≤ (neighborhood 1 A).card

Harper's vertex-isoperimetric theorem (family level, slice-induction form). The simplicial initial segment of a given size has the smallest closed unit neighborhood among all families of that size: |N(initSeg N |A|)| ≤ |N(A)|.

The proof is the PDF Frankl–Füredi dimension recursion: split a family B ⊆ Cube (M+1) into its two M-dimensional slices, use neighborhood_succ, lower-bound each cross term by a maximum via the dimension-M induction hypothesis, and invoke the scalar Macaulay minimization harper_macaulay_min.