Macaulay increment arithmetic

This file develops the increment profile of the Harper boundary function and the nested-cascade inequalities used by the final minimization argument.

noncomputable def BooleanIsoperimetry.HIncrement (n p : ℕ) : ℕ

The first forward difference of the closed-neighborhood profile of the simplicial initial segments. It is stated with truncated subtraction because H is monotone but the project mostly uses additive inequalities over ℕ.

Equations

• BooleanIsoperimetry.HIncrement n p = BooleanIsoperimetry.H n (p + 1) - BooleanIsoperimetry.H n p

theorem BooleanIsoperimetry.H_eq_sum_HIncrement (n k : ℕ) : H n k = ∑ p ∈ Finset.range k, HIncrement n p

theorem BooleanIsoperimetry.H_increment_lower_dim_sub (n p : ℕ) (hp : p + 1 ≤ 2 ^ n) : H n p + (n - p) ≤ H n (p + 1)

Additive form of the one-step lower bound: the new point contributes at least n - p new neighborhood vertices. This is a direct corollary of H_increment_lower, but the shape is easier to reuse in cascade-layer arguments.

theorem BooleanIsoperimetry.HIncrement_lower (n p : ℕ) (hp : p + 1 ≤ 2 ^ n) : n - p ≤ HIncrement n p

First-difference form of H_increment_lower: as long as p + 1 is inside the n-cube, the p-th increment of H n is at least n - p.

theorem BooleanIsoperimetry.HIncrement_eq_gShift_inv (n p : ℕ) (w : Cube n) (hw : rank w = p) : HIncrement n p = {v : Cube n | gShift v = w}.card

The exact first difference of H is the number of preimages of the rank-p vertex under gShift. This exactly captures the Kruskal-Katona binomial layer profile.

theorem BooleanIsoperimetry.gShift_preimage_eq_insert_below_min {n : ℕ} (w : Cube n) (h : Finset.Nonempty w) : {v : Cube n | gShift v = w} = Finset.image (fun (j : Fin n) => insert j w) {j : Fin n | ↑j < ↑(Finset.min' w h)}

Exact gShift-preimage structure of a nonempty vertex. For a nonempty vertex w, the vertices v with gShift v = w are exactly the vertices insert j w obtained by adding a new minimum coordinate j strictly below w.min'. (Adding such a j makes it the new minimum, and gShift removes it again.) This is the set-level Kruskal–Katona/Macaulay layer structure: the gShift-fibre of w is an interval of "lower extensions".

This refines H_increment_lower (which only established the ⊇ inclusion and a cardinality lower bound) to a full equality of fibres, and is the reusable input for the exact increment-profile value HIncrement_eq_min'.

theorem BooleanIsoperimetry.HIncrement_eq_min' {n : ℕ} (p : ℕ) (w : Cube n) (hw : rank w = p) (hne : Finset.Nonempty w) : HIncrement n p = ↑(Finset.min' w hne)

Exact Macaulay increment profile (minimum-coordinate form). The p-th first difference of the closed-neighbourhood profile H equals the smallest active coordinate of the (unique) rank-p vertex w. Equivalently, the number of gShift-preimages of w is w.min'.

This is the exact Kruskal–Katona/Macaulay layer-increment value, upgrading the lower bound HIncrement_lower (n - p ≤ HIncrement n p, via rank_add_min_ge) to a closed form. It is reusable, non-circular H-increment theory: it mentions only H, rank, gShift, and Finset.min', and sits well below the cascade/Macaulay-window leaves in the dependency order.

theorem BooleanIsoperimetry.HIncrement_zero (n : ℕ) : HIncrement n 0 = n + 1

The empty-rank first difference: adding the empty vertex exposes the whole closed unit ball around it.

noncomputable def BooleanIsoperimetry.macaulayShadowWeight {n : ℕ} (w : Cube n) : ℕ

The exact Macaulay shadow weight of a rank vertex. Nonempty vertices contribute their smallest active coordinate; the empty vertex contributes the n + 1 vertices in its closed unit ball.

Equations

• BooleanIsoperimetry.macaulayShadowWeight w = if h : Finset.Nonempty w then ↑(Finset.min' w h) else n + 1

theorem BooleanIsoperimetry.rank_eq_zero_of_not_nonempty {n p : ℕ} (w : Cube n) (hw : rank w = p) (hempty : ¬Finset.Nonempty w) : p = 0

theorem BooleanIsoperimetry.HIncrement_eq_macaulayShadowWeight {n : ℕ} (p : ℕ) (w : Cube n) (hw : rank w = p) : HIncrement n p = macaulayShadowWeight w

Uniform exact first-difference formula, including the empty vertex. This is the rank-indexed layer profile used to turn a Macaulay shadow window into an ordinary sum over vertices in the corresponding rank interval.

Macaulay layer increment-profile bounds

Reusable upper bounds for the HIncrement/min-coordinate layer profile. The existing HIncrement_lower (n - p ≤ HIncrement n p) gives a global lower bound; the lemmas below give the per-layer upper bound HIncrement n j ≤ n - r for every rank j in Macaulay layer r (the cardinality-r band [binomPrefix n r, binomPrefix n (r+1))). This is the increment-profile theory flagged by the Aristotle obstruction: it pins the increment of a layer-r vertex between n - (binomPrefix n (r+1) - 1) and n - r, and is exactly the upper-shadow-window bound used by the Frankl–Füredi/Macaulay window comparisons.

The combinatorial core is the elementary cube_min'_add_card_le: a card-r subset of Fin n has its smallest coordinate plus its cardinality bounded by n (its r coordinates all lie in [min', n), an interval of size n - min').

theorem BooleanIsoperimetry.cube_min'_add_card_le {n : ℕ} (w : Cube n) (h : Finset.Nonempty w) : ↑(Finset.min' w h) + Finset.card w ≤ n

A nonempty vertex of the n-cube satisfies min' + card ≤ n: its card active coordinates all lie in [min', n), an interval of size n - min'. A pure Finset.min' bound, used for the per-layer increment upper bound.

theorem BooleanIsoperimetry.exists_rank_eq {n j : ℕ} (hj : j < 2 ^ n) : ∃ (w : Cube n), rank w = j

Every rank below 2 ^ n is realised by some vertex of the n-cube (rank is a bijection onto range (2 ^ n)).

theorem BooleanIsoperimetry.HIncrement_le_of_mem_layer {n r j : ℕ} (hr : 1 ≤ r) (hlo : binomPrefix n r ≤ j) (hhi : j < binomPrefix n (r + 1)) : HIncrement n j ≤ n - r

Per-layer increment upper bound. For a rank j in Macaulay layer r (i.e. binomPrefix n r ≤ j < binomPrefix n (r+1), the cardinality-r band), the increment HIncrement n j (the min coordinate of the rank-j vertex) is at most n - r. This is the upper companion of HIncrement_lower.

theorem BooleanIsoperimetry.HIncrement_window_le_of_layer {n r a L : ℕ} (hr : 1 ≤ r) (hlo : binomPrefix n r ≤ a) (hhi : a + L ≤ binomPrefix n (r + 1)) : ∑ i ∈ Finset.Ico a (a + L), HIncrement n i ≤ L * (n - r)

Per-layer increment window bound. A length-L rank window contained in a single Macaulay layer r has total HIncrement mass at most L * (n - r). This is the reusable upper-shadow-window bound for a window confined to one layer; it follows by summing HIncrement_le_of_mem_layer over the window.

theorem BooleanIsoperimetry.HIncrement_window_eq_macaulayShadowWeight_sum (n lo hi : ℕ) (hhi : hi ≤ 2 ^ n) : ∑ i ∈ Finset.Ico lo hi, HIncrement n i = ∑ w : Cube n with lo ≤ rank w ∧ rank w < hi, macaulayShadowWeight w

Exact interval form of the Macaulay layer profile: a rank window of HIncrement is the sum of the explicit shadow weights of the vertices whose ranks lie in the same interval. The endpoint bound hi ≤ 2^n is the natural cube-capacity condition used by all Harper windows.

theorem BooleanIsoperimetry.H_strictMono_on_initial_layer {n p : ℕ} (hp : p + 1 ≤ 2 ^ n) (hpn : p < n) : H n p < H n (p + 1)

Strictness consequence of the increment lower bound: before rank n, extending the initial segment by one strictly enlarges its closed neighborhood.

theorem BooleanIsoperimetry.canonical_boundaryCost_eq_H_add {n k p q : ℕ} (hp : p ≤ 2 ^ n) (_hq : q ≤ 2 ^ n) (hq_pos : 1 ≤ q) (h_casc : CascadeSplit n k p q) : max (H n p) q + max (H n q) p = H n p + H n q

The genuine inductive content of Harper's inequality, isolated as a single statement with the induction hypothesis ih supplied explicitly. This is the sole remaining open step: it is exactly the inductive step of Harper's vertex-isoperimetric theorem ("the canonical cascade split minimises the cross boundary expression"), which is not currently in Mathlib.

Given the canonical cascade split (p, q) of a + b (so H (n+1) (a+b) = max (H n p) q + max (H n q) p by H_succ_cascade), and given Harper's inequality at all strictly smaller dimensions (ih), the canonical split has boundary value no larger than the value of any other split (a, b).

It is stated non-circularly: it refers only to H, CascadeSplit, and the induction hypothesis ih, never to boundaryCost, CascadeInterleaves, H_inequality_core, or any later result that ultimately depends on it.

WHAT IS KNOWN (verified by computation for n ≤ 4): after reducing the left side to H n p + H n q (using q ≤ p ≤ H n q from the cascade), and taking a ≥ b by symmetry, the goal splits into

• Case I (a ≤ H n b): H n p + H n q ≤ H n a + H n b;
• Case II (a > H n b): H n p + H n q ≤ H n a + a. Both are true; closing them is the missing combinatorial heart (a compression / nested-cascade interleaving argument using ih).

theorem BooleanIsoperimetry.boundaryCost_comm (n a b : ℕ) : max (H n a) b + max (H n b) a = max (H n b) a + max (H n a) b

theorem BooleanIsoperimetry.boundaryCost_eq_case_le {n a b : ℕ} (ha : a ≤ 2 ^ n) (hb_le_a : b ≤ a) (hcase : a ≤ H n b) : max (H n a) b + max (H n b) a = H n a + H n b

theorem BooleanIsoperimetry.boundaryCost_eq_case_gt {n a b : ℕ} (ha : a ≤ 2 ^ n) (hb_le_a : b ≤ a) (hcase : H n b < a) : max (H n a) b + max (H n b) a = H n a + a

theorem BooleanIsoperimetry.harper_bc_min_q_zero_core (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.harper_bc_min_q_zero (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 : ℕ} (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.cascade_max_eq_right {n x x0 x1 : ℕ} (hx : CascadeSplit n x x0 x1) : max (H n x1) x0 = if 1 ≤ x1 then H n x1 else x0

theorem BooleanIsoperimetry.H_succ_cascade_expand {n x x0 x1 : ℕ} (hx : CascadeSplit n x x0 x1) (hx0 : x0 ≤ 2 ^ n) : max (H n x0) x1 + max (H n x1) x0 = H n x0 + if 1 ≤ x1 then H n x1 else x0

theorem BooleanIsoperimetry.harper_extremal_n (n : ℕ) (ih : ∀ m < n + 1, ∀ (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) (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

The level-n Harper extremal inequality, extracted from the induction hypothesis ih (at m = n) and packaged for canonical cascade splits.

Given the canonical cascade split (p, q) of a + b at level n, its cross boundary cost is no larger than that of the arbitrary split (a, b). This is exactly ih n rewritten through H_succ_cascade; it is the one-dimension-lower Macaulay/Harper extremal statement, used as a tool for the genuine n → n+1 inductive step below.

theorem BooleanIsoperimetry.cascade_p_le {n k p q : ℕ} (h : CascadeSplit n k p q) : p ≤ 2 ^ n

theorem BooleanIsoperimetry.cascade_q_le {n k p q : ℕ} (h : CascadeSplit n k p q) : q ≤ 2 ^ n

theorem BooleanIsoperimetry.harper_extremal_step_nested_q_zero (n : ℕ) (_ih : ∀ m < n + 1, ∀ (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 p0 p1 q0 q1 a0 a1 b0 b1 : ℕ} (ha : a ≤ 2 ^ (n + 1)) (hb : b ≤ 2 ^ (n + 1)) (hcasc : CascadeSplit (n + 1) (a + b) p q) (hq_zero : q = 0) (_hp0 : p0 ≤ 2 ^ n) (_hp1 : p1 ≤ 2 ^ n) (_hq0 : q0 ≤ 2 ^ n) (_hq1 : q1 ≤ 2 ^ n) (_ha0 : a0 ≤ 2 ^ n) (_ha1 : a1 ≤ 2 ^ n) (_hb0 : b0 ≤ 2 ^ n) (_hb1 : b1 ≤ 2 ^ n) (hp_split : CascadeSplit n p p0 p1) (hq_split : CascadeSplit n q q0 q1) (ha_split : CascadeSplit n a a0 a1) (hb_split : CascadeSplit n b b0 b1) : max (max (H n p0) p1 + max (H n p1) p0) q + max (max (H n q0) q1 + max (H n q1) q0) p ≤ max (max (H n a0) a1 + max (H n a1) a0) b + max (max (H n b0) b1 + max (H n b1) b0) a

The degenerate top-level branch of the nested extremal step. When the canonical upper slice q is empty, the statement reduces to the already-proved harper_bc_min_q_zero in dimension n + 1 (with a symmetric a,b branch).

theorem BooleanIsoperimetry.cascade_slice_mono {n x x0 x1 y y0 y1 : ℕ} (hx : CascadeSplit n x x0 x1) (hy : CascadeSplit n y y0 y1) (hxy : x ≤ y) : x0 ≤ y0 ∧ x1 ≤ y1

Monotonicity of the canonical cascade slices. If x ≤ y then both canonical slice values of x are dominated by those of y. This is because the lower (resp. upper) slice of a simplicial initial segment is monotone in the segment size (initial segments are nested), and slice_card_eq_cascade identifies these slice cardinalities with the cascade split values.

theorem BooleanIsoperimetry.cascade_lower_le_of_neighbor_lt {n a b p q : ℕ} (hcasc : CascadeSplit (n + 1) (a + b) p q) (hq_pos : 1 ≤ q) (hcase : H (n + 1) b < a) : p ≤ a

In the GT regime of the inductive step (the larger part a exceeds the neighbourhood H (n+1) b of the smaller part b), the canonical lower slice p of a + b is at most a.

Proof: if a < p then, since p + q = a + b, the upper slice satisfies q < b; but the canonical compression gives p ≤ H (n+1) q ≤ H (n+1) b < a, contradicting a < p. This is a clean structural consequence of cascade_p_le_H_q, H_mono, and cascade_split_add; it is non-circular (it does not use any later Harper result).

theorem BooleanIsoperimetry.one_le_binomPrefix_succ (n r : ℕ) : 1 ≤ binomPrefix n (r + 1)

Every positive canonical split with empty upper subslice has mass exactly one.

theorem BooleanIsoperimetry.cascade_upper_zero_eq_one {n q q0 q1 : ℕ} (h : CascadeSplit n q q0 q1) (hq_pos : 1 ≤ q) (hq1_zero : q1 = 0) : q = 1

If the upper slice in a canonical split is zero but the split mass is positive, then the split mass is the singleton initial segment.

theorem BooleanIsoperimetry.cascade_upper_zero_eq_zero_or_one {n q q0 q1 : ℕ} (h : CascadeSplit n q q0 q1) (hq1_zero : q1 = 0) : q = 0 ∨ q = 1

If the upper slice in a canonical split is zero, then the split mass is in the bottom layer: it is either empty or the singleton initial segment.

theorem BooleanIsoperimetry.cascade_upper_zero_lower_eq {n q q0 q1 : ℕ} (h : CascadeSplit n q q0 q1) (hq1_zero : q1 = 0) : q0 = q

In the same situation, the lower slice is the whole split mass.

theorem BooleanIsoperimetry.cascade_split_binomPrefix (n r : ℕ) (hr : 1 ≤ r) (hrn : r ≤ n + 1) : CascadeSplit n (binomPrefix (n + 1) r) (binomPrefix n r) (binomPrefix n (r - 1))

A full binomial prefix binomPrefix (n+1) r splits canonically into the corresponding full layers binomPrefix n r and binomPrefix n (r-1) in the lower dimensions.

theorem BooleanIsoperimetry.H_binomPrefix (n r : ℕ) (hr : 1 ≤ r) : H n (binomPrefix n r) = binomPrefix n (r + 1)

The boundary of a full binomial prefix (a complete collection of layers) is exactly the next full binomial prefix, evaluated algebraically on H.

theorem BooleanIsoperimetry.H_binomPrefix_first_diff (n : ℕ) : H n (binomPrefix n 1) - H n (binomPrefix n 0) = n.choose 0 + n.choose 1

The first full binomial-prefix jump of H: the closed neighbourhood of the singleton initial segment contains both the empty layer and the first layer.

theorem BooleanIsoperimetry.H_binomPrefix_diff (n r : ℕ) (hr : 2 ≤ r) : H n (binomPrefix n r) - H n (binomPrefix n (r - 1)) = n.choose r

Layer-precise increment behavior away from the empty-prefix edge case: the total increment of H across the r-th positive binomial layer is exactly its size Nat.choose n r. This is required because H is not concave across layer boundaries.

theorem BooleanIsoperimetry.H_binomPrefix_succ_diff (n r : ℕ) (hr : 1 ≤ r) : H n (binomPrefix n (r + 1)) - H n (binomPrefix n r) = n.choose (r + 1)

Adjacent full-binomial-prefix form of the same layer calculation. This avoids subtraction from r - 1 and is often the cleaner statement for induction over cascade layers.

theorem BooleanIsoperimetry.H_binomPrefix_add_layer (n r : ℕ) (hr : 1 ≤ r) : H n (binomPrefix n r) + n.choose (r + 1) = H n (binomPrefix n (r + 1))

Additive full-layer form of H_binomPrefix_succ_diff. This avoids truncated subtraction and is the shape needed when comparing sums of whole Kruskal-Katona/Macaulay layers.

theorem BooleanIsoperimetry.H_binomPrefix_window (n r s : ℕ) (hr : 1 ≤ r) (hrs : r ≤ s) : H n (binomPrefix n r) + ∑ i ∈ Finset.Ico (r + 1) (s + 1), n.choose i = H n (binomPrefix n s)

Additive window form for complete binomial layers: moving H from the full prefix below layer r to the full prefix below layer s adds exactly the whole layers r+1, ..., s. This is a reusable whole-block version of the increment-window profile behind the positive-cascade obstruction.

theorem BooleanIsoperimetry.H_binomPrefix_partial_layer_le (n r t : ℕ) (hr : 1 ≤ r) (ht : t ≤ n.choose (r + 1)) : H n (binomPrefix n r) + t ≤ H n (binomPrefix n (r + 1))

Partial-layer upper bound for H on complete binomial prefixes. If only t points of the next Macaulay layer are available, with t no larger than the whole next layer, then adding t to the boundary of the lower full prefix stays below the boundary of the next full prefix.

This is the inequality form of H_binomPrefix_add_layer, useful when a cascade comparison cuts through a layer rather than moving by a whole binomial block.

theorem BooleanIsoperimetry.H_binomPrefix_partial_window_le (n r s t : ℕ) (hr : 1 ≤ r) (hrs : r ≤ s) (ht : t ≤ ∑ i ∈ Finset.Ico (r + 1) (s + 1), n.choose i) : H n (binomPrefix n r) + t ≤ H n (binomPrefix n s)

Partial-window upper bound for H on complete binomial prefixes. Any amount t bounded by the total size of the complete layers from r+1 through s can be added to H at the lower full prefix without exceeding H at the upper full prefix.

This packages the full-window equality in the one-sided form needed for partial-window majorization and nested-cascade interleaving arguments.

theorem BooleanIsoperimetry.H_add_le_H_add_of_le_telescope (n a b c d : ℕ) (hab : a + b = c + d) (hac : a ≤ c) (hinc : ∀ i < c - a, H (n + 1) (a + i + 1) + H (n + 1) (b - i - 1) ≤ H (n + 1) (a + i) + H (n + 1) (b - i)) : H (n + 1) c + H (n + 1) d ≤ H (n + 1) a + H (n + 1) b

theorem BooleanIsoperimetry.H_add_le_H_add_of_ge_telescope (n a b c d : ℕ) (hab : a + b = c + d) (hca : c ≤ a) (hinc : ∀ i < a - c, H (n + 1) (c + i) + H (n + 1) (d - i) ≤ H (n + 1) (c + i + 1) + H (n + 1) (d - i - 1)) : H (n + 1) c + H (n + 1) d ≤ H (n + 1) a + H (n + 1) b

theorem BooleanIsoperimetry.harper_case_gt_a_ge_p (n : ℕ) {a b p q : ℕ} (hq_pos : 1 ≤ q) (hcase : H (n + 1) b < a) (hcasc : CascadeSplit (n + 1) (a + b) p q) : p ≤ a

In Case GT, the canonical split p is at most as large as a. This is the structural half of the GT branch: if a is already larger than the neighbourhood of b, then the positive canonical split of a+b cannot put more than a vertices in its lower slice. The proof uses only the earlier canonical compression lemma cascade_p_le_H_q and monotonicity of H.

theorem BooleanIsoperimetry.harper_gt_split_between (n : ℕ) {a b p q : ℕ} (hq_pos : 1 ≤ q) (hcase : H (n + 1) b < a) (hcasc : CascadeSplit (n + 1) (a + b) p q) : b ≤ q ∧ q ≤ p ∧ p ≤ a

Structural "central compression" invariant of the GT regime of the positive Macaulay step. When the larger part a already dominates the neighbourhood of the smaller part (H (n+1) b < a), the canonical cascade split (p, q) of a + b is sandwiched between the two parts: b ≤ q ≤ p ≤ a.

This records that, in the slack regime, passing to the canonical split moves mass strictly inward (from the a-side toward the b-side) without crossing either endpoint. It depends only on the level-n+1 cascade structure (harper_case_gt_a_ge_p, cascade_q_le_p, cascade_split_add) and the case hypothesis, so it is non-circular and reusable in any GT-regime argument.

noncomputable def BooleanIsoperimetry.cascadeBoundary (n x0 x1 : ℕ) : ℕ

The two-slice boundary expression produced by the cascade recursion one dimension up. This is the local algebraic boundary cost of a nested split x = x0 + x1 before rewriting it back to H (n+1) x.

Equations

• BooleanIsoperimetry.cascadeBoundary n x0 x1 = max (BooleanIsoperimetry.H n x0) x1 + max (BooleanIsoperimetry.H n x1) x0

theorem BooleanIsoperimetry.cascadeBoundary_eq_H_succ {n x x0 x1 : ℕ} (hx : CascadeSplit n x x0 x1) : cascadeBoundary n x0 x1 = H (n + 1) x

A nested cascade boundary is exactly the corresponding H (n+1) value.

noncomputable def BooleanIsoperimetry.pairedCascadeBoundary (n x0 x1 y0 y1 : ℕ) : ℕ

The paired nested boundary expression for two level-n cascade splits. The remaining positive Macaulay step compares this profile for the canonical split (p,q) against the profile for an arbitrary split (a,b).

Equations

• BooleanIsoperimetry.pairedCascadeBoundary n x0 x1 y0 y1 = BooleanIsoperimetry.cascadeBoundary n x0 x1 + BooleanIsoperimetry.cascadeBoundary n y0 y1

theorem BooleanIsoperimetry.pairedCascadeBoundary_eq_H_add {n x y x0 x1 y0 y1 : ℕ} (hx : CascadeSplit n x x0 x1) (hy : CascadeSplit n y y0 y1) : pairedCascadeBoundary n x0 x1 y0 y1 = H (n + 1) x + H (n + 1) y

Paired nested boundaries rewrite to the sum of the two H (n+1) boundary values. This packages the four-block expression that occurs in the two open positive-cascade leaves.

theorem BooleanIsoperimetry.cascadeBoundary_mono {n x0 x1 y0 y1 : ℕ} (h0 : x0 ≤ y0) (h1 : x1 ≤ y1) : cascadeBoundary n x0 x1 ≤ cascadeBoundary n y0 y1

Componentwise monotonicity of the nested two-slice boundary profile. This is the local monotonicity tool available before the genuine Macaulay interleaving argument starts: if both exposed cascade slices grow, then the corresponding two-slice boundary cost grows.

theorem BooleanIsoperimetry.pairedCascadeBoundary_mono {n x0 x1 y0 y1 z0 z1 w0 w1 : ℕ} (hx0 : x0 ≤ z0) (hx1 : x1 ≤ z1) (hy0 : y0 ≤ w0) (hy1 : y1 ≤ w1) : pairedCascadeBoundary n x0 x1 y0 y1 ≤ pairedCascadeBoundary n z0 z1 w0 w1

Paired version of cascadeBoundary_mono, used when comparing the four exposed blocks in a nested cascade profile.

theorem BooleanIsoperimetry.cascadeBoundary_mono_of_cascade_le {n x x0 x1 y y0 y1 : ℕ} (hx : CascadeSplit n x x0 x1) (hy : CascadeSplit n y y0 y1) (hxy : x ≤ y) : cascadeBoundary n x0 x1 ≤ cascadeBoundary n y0 y1

Monotonicity of cascadeBoundary along canonical cascade splits. It packages cascade_slice_mono with the local boundary monotonicity above.

theorem BooleanIsoperimetry.nested_cascade_mass_conservation {n a b p q p0 p1 q0 q1 a0 a1 b0 b1 : ℕ} (hcasc : CascadeSplit (n + 1) (a + b) p q) (hp_split : CascadeSplit n p p0 p1) (hq_split : CascadeSplit n q q0 q1) (ha_split : CascadeSplit n a a0 a1) (hb_split : CascadeSplit n b b0 b1) : p0 + p1 + (q0 + q1) = a0 + a1 + (b0 + b1)

Mass conservation for the two nested cascade decompositions under a common top-level split. This is the algebraic form of the fact that the four exposed level-n pieces of (p,q) and (a,b) occupy the same total window.

theorem BooleanIsoperimetry.nested_cascade_flat_mass_conservation {n a b p q p0 p1 q0 q1 a0 a1 b0 b1 : ℕ} (hcasc : CascadeSplit (n + 1) (a + b) p q) (hp_split : CascadeSplit n p p0 p1) (hq_split : CascadeSplit n q q0 q1) (ha_split : CascadeSplit n a a0 a1) (hb_split : CascadeSplit n b b0 b1) : p0 + p1 + q0 + q1 = a0 + a1 + b0 + b1

The same conservation statement in flattened form, often more convenient for linear arithmetic over component-wise interleaving inequalities.

def BooleanIsoperimetry.cappedPrefixMass (n k l : ℕ) : ℕ

Capped prefix mass: the number of elements in the first k vertices of the n-cube that belong to layers < l.

Equations

• BooleanIsoperimetry.cappedPrefixMass n k l = min k (BooleanIsoperimetry.binomPrefix n l)

def BooleanIsoperimetry.splitPrefixMass (n a b l : ℕ) : ℕ

The combined prefix mass of a split (a, b) up to layer l. The 0-slice contributes layers < l + 1, while the 1-slice contributes layers < l after adding the last coordinate.

Equations

• BooleanIsoperimetry.splitPrefixMass n a b l = BooleanIsoperimetry.cappedPrefixMass n a (l + 1) + BooleanIsoperimetry.cappedPrefixMass n b l

def BooleanIsoperimetry.CascadeInterleaves (n p q a b : ℕ) : Prop

Structural majorization relation for splits. A split (p, q) interleaves (a, b) when (p, q) is the canonical cascade split of the common total a + b and, in addition, (p, q) is at least as bottom-heavy as (a, b) at every binomial prefix layer.

The relation is purely structural: the first conjunct records the cascade profile of (p, q) and the second is the prefix-mass (Macaulay) majorization. It mentions neither boundaryCost nor H_inequality_core.

The prefix-mass conjunct alone is not enough to force the boundary-cost inequality (two different splits can have identical prefix masses but distinct boundary costs), which is why the cascade profile of (p, q) is recorded as well.

Equations

• One or more equations did not get rendered due to their size.

theorem BooleanIsoperimetry.splitPrefixMass_le_min (n a b l : ℕ) : splitPrefixMass n a b l ≤ min (a + b) (binomPrefix n (l + 1) + binomPrefix n l)

A pointwise upper bound on the prefix mass of an arbitrary split.

theorem BooleanIsoperimetry.cascade_splitPrefixMass_eq {n k p q : ℕ} (h : CascadeSplit n k p q) (l : ℕ) : splitPrefixMass n p q l = min k (binomPrefix n (l + 1) + binomPrefix n l)

The canonical cascade split saturates the prefix-mass bound at every layer.

theorem BooleanIsoperimetry.canonicalSplit_interleaves {n a b p q : ℕ} (_ha : a ≤ 2 ^ n) (_hb : b ≤ 2 ^ n) (h_casc : CascadeSplit n (a + b) p q) : CascadeInterleaves n p q a b

The canonical cascade split of a + b maximizes prefix mass, hence interleaves any other split (a, b).

theorem BooleanIsoperimetry.cappedPrefixMass_succ_of_cascadeSplit {n k k0 k1 : ℕ} (hk : CascadeSplit n k k0 k1) (l : ℕ) : cappedPrefixMass (n + 1) k (l + 1) = cappedPrefixMass n k0 (l + 1) + cappedPrefixMass n k1 l

theorem BooleanIsoperimetry.splitPrefixMass_succ_of_cascadeSplits {n a a0 a1 b b0 b1 : ℕ} (ha : CascadeSplit n a a0 a1) (hb : CascadeSplit n b b0 b1) (l : ℕ) : splitPrefixMass (n + 1) a b (l + 1) = splitPrefixMass n a0 b0 (l + 1) + splitPrefixMass n a1 b1 l

theorem BooleanIsoperimetry.CascadeInterleaves.lower_succ {n a b p q p0 p1 q0 q1 a0 a1 b0 b1 : ℕ} (h_inter : CascadeInterleaves (n + 1) p q a b) (hp : CascadeSplit n p p0 p1) (hq : CascadeSplit n q q0 q1) (ha : CascadeSplit n a a0 a1) (hb : CascadeSplit n b b0 b1) (l : ℕ) : splitPrefixMass n a0 b0 (l + 1) + splitPrefixMass n a1 b1 l ≤ splitPrefixMass n p0 q0 (l + 1) + splitPrefixMass n p1 q1 l