Binomial cascade arithmetic

This file develops binomial-prefix and Macaulay-cascade infrastructure for simplicial initial segments in the Boolean cube, including the slice recurrence for the Harper boundary function H.

def BooleanIsoperimetry.IsBinomialCascade (n k r t : ℕ) : Prop

IsBinomialCascade n k r t is the canonical layer decomposition of k in the n-cube: all layers of sizes < r are full, and t points are taken from layer r.

The final disjunct makes the decomposition canonical at layer boundaries: when a layer is completely full, we move to the next layer with residual 0.

Equations

• BooleanIsoperimetry.IsBinomialCascade n k r t = (r ≤ n + 1 ∧ t ≤ n.choose r ∧ k = BooleanIsoperimetry.binomPrefix n r + t ∧ (t < n.choose r ∨ r = n + 1))

def BooleanIsoperimetry.cascadeSlice0Value (n r t : ℕ) : ℕ

The lower-slice size determined by cascade parameters n, r, and t.

Equations

• BooleanIsoperimetry.cascadeSlice0Value n r t = BooleanIsoperimetry.binomPrefix n r + (t - BooleanIsoperimetry.choosePred n r)

def BooleanIsoperimetry.cascadeSlice1Value (n r t : ℕ) : ℕ

The upper-slice size determined by cascade parameters n, r, and t.

Equations

• BooleanIsoperimetry.cascadeSlice1Value n r t = BooleanIsoperimetry.binomPrefix n (r - 1) + min t (BooleanIsoperimetry.choosePred n r)

def BooleanIsoperimetry.CascadeSplit (n k p q : ℕ) : Prop

The algebraic lower/upper split for the canonical cascade of k in dimension n + 1. It is independent of slice0, slice1, rank, and neighborhoods.

Equations

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

theorem BooleanIsoperimetry.int_sum_mul_le_of_prefix_le_of_antitone_weight (M : ℕ) (u v w : ℕ → ℤ) (hpref : ∀ r ≤ M, ∑ i ∈ Finset.range r, v i ≤ ∑ i ∈ Finset.range r, u i) (htot : ∑ i ∈ Finset.range M, u i = ∑ i ∈ Finset.range M, v i) : (∀ i < M, 0 ≤ w i) → ∀ (hwanti : ∀ (i : ℕ), i + 1 < M → w (i + 1) ≤ w i), ∑ i ∈ Finset.range M, w i * v i ≤ ∑ i ∈ Finset.range M, w i * u i

Abel summation majorization over ℤ: if v is majorized by u in prefix sums, and w is antitone, then the w-weighted sum of v is ≤ that of u.

theorem BooleanIsoperimetry.binomPrefix_zero (n : ℕ) : binomPrefix n 0 = 0

theorem BooleanIsoperimetry.binomPrefix_succ (n r : ℕ) : binomPrefix n (r + 1) = binomPrefix n r + n.choose r

theorem BooleanIsoperimetry.binomPrefix_mono (n : ℕ) {r s : ℕ} (h : r ≤ s) : binomPrefix n r ≤ binomPrefix n s

theorem BooleanIsoperimetry.binomPrefix_full (n : ℕ) : binomPrefix n (n + 1) = 2 ^ n

theorem BooleanIsoperimetry.choose_eq_zero_of_gt {n r : ℕ} (h : n < r) : n.choose r = 0

theorem BooleanIsoperimetry.binomPrefix_le_two_pow (n r : ℕ) : binomPrefix n r ≤ 2 ^ n

theorem BooleanIsoperimetry.binomPrefix_eq_two_pow_of_ge (n r : ℕ) (h : n + 1 ≤ r) : binomPrefix n r = 2 ^ n

theorem BooleanIsoperimetry.binomPrefix_pascal (n r : ℕ) : binomPrefix (n + 1) r = binomPrefix n r + binomPrefix n (r - 1)

theorem BooleanIsoperimetry.choose_succ_dim (n r : ℕ) : (n + 1).choose r = n.choose r + choosePred n r

Nat.choose (n+1) r splits as Nat.choose n r + choosePred n r.

theorem BooleanIsoperimetry.binomPrefix_pred_add_choosePred (n r : ℕ) : binomPrefix n (r - 1) + choosePred n r = binomPrefix n r

binomPrefix n (r-1) + choosePred n r = binomPrefix n r.

theorem BooleanIsoperimetry.exists_isBinomialCascade (n k : ℕ) (hk : k ≤ 2 ^ (n + 1)) : ∃ (r : ℕ) (t : ℕ), IsBinomialCascade (n + 1) k r t

theorem BooleanIsoperimetry.cascade_slice_add {n k r t : ℕ} (h : IsBinomialCascade (n + 1) k r t) : cascadeSlice0Value n r t + cascadeSlice1Value n r t = k

The two cascade slice values sum to k.

theorem BooleanIsoperimetry.cascadeSlice0Value_le {n k r t : ℕ} (h : IsBinomialCascade (n + 1) k r t) : cascadeSlice0Value n r t ≤ 2 ^ n

The lower cascade slice value is at most 2^n.

theorem BooleanIsoperimetry.cascadeSlice1Value_le {n k r t : ℕ} : IsBinomialCascade (n + 1) k r t → cascadeSlice1Value n r t ≤ 2 ^ n

The upper cascade slice value is at most 2^n.

theorem BooleanIsoperimetry.exists_cascade_split (n k : ℕ) (hk : k ≤ 2 ^ (n + 1)) : ∃ (p : ℕ) (q : ℕ), p ≤ 2 ^ n ∧ q ≤ 2 ^ n ∧ p + q = k ∧ CascadeSplit n k p q

Every integer k ≤ 2^(n+1) admits a valid cascade split (p, q) bounded by 2^n.

theorem BooleanIsoperimetry.isBinomialCascade_unique {m k r t r' t' : ℕ} (h : IsBinomialCascade m k r t) (h' : IsBinomialCascade m k r' t') : r = r' ∧ t = t'

Uniqueness of the canonical binomial cascade decomposition. For a fixed total k and dimension m, the canonical cascade (r, t) with all layers below r full and t points of layer r is unique. Standard fact: if r < r' then the full prefix binomPrefix m (r+1) already exceeds the partial sum, forcing t = Nat.choose m r and (via the canonical boundary disjunct) r = m, which is incompatible with r < r' ≤ m.

theorem BooleanIsoperimetry.cascadeSplit_unique {n k p q p' q' : ℕ} (h : CascadeSplit n k p q) (h' : CascadeSplit n k p' q') : p = p' ∧ q = q'

Uniqueness of the canonical cascade split. Because the underlying binomial cascade (r, t) is unique, the canonical split (p, q) of a fixed total k in dimension n + 1 is uniquely determined. This is what lets the Frankl–Füredi terminal family be identified with the canonical cascade pair.

theorem BooleanIsoperimetry.card_filter_card_eq (n c : ℕ) : {w : Cube n | Finset.card w = c}.card = n.choose c

The number of vertices of the n-cube with cardinality exactly c is C(n,c).

theorem BooleanIsoperimetry.card_filter_card_lt (n c : ℕ) : {w : Cube n | Finset.card w < c}.card = binomPrefix n c

The number of vertices of the n-cube with cardinality < c is binomPrefix n c.

theorem BooleanIsoperimetry.lowCard_eq_initSeg (n c : ℕ) : {w : Cube n | Finset.card w < c} = simplicialInitSeg n (binomPrefix n c)

The set of low-cardinality vertices is exactly an initial segment.

theorem BooleanIsoperimetry.rank_lt_binomPrefix_iff {n c : ℕ} (w : Cube n) : rank w < binomPrefix n c ↔ Finset.card w < c

rank versus cardinality: rank w < binomPrefix n c ↔ w.card < c.

theorem BooleanIsoperimetry.binomPrefix_card_le_rank {n : ℕ} (w : Cube n) : binomPrefix n (Finset.card w) ≤ rank w

Layer lower bound on rank.

theorem BooleanIsoperimetry.rank_lt_binomPrefix_card_succ {n : ℕ} (w : Cube n) : rank w < binomPrefix n (Finset.card w + 1)

Layer upper bound on rank.

theorem BooleanIsoperimetry.cubeToNat_lt {n : ℕ} (u : Cube n) : cubeToNat u < 2 ^ n

cubeToNat of any vertex of the n-cube is < 2^n.

theorem BooleanIsoperimetry.simplicialLt_embed1_embed1 {n : ℕ} (u w : Cube n) : simplicialLt (embed1 u) (embed1 w) ↔ simplicialLt u w

embed1 reflects (and preserves) the strict simplicial order.

theorem BooleanIsoperimetry.simplicialLt_embed0_embed1 {n : ℕ} (u w : Cube n) : simplicialLt (embed0 u) (embed1 w) ↔ Finset.card u < Finset.card w + 1

Comparing an embed0 vertex with an embed1 vertex reduces to cardinalities.

theorem BooleanIsoperimetry.rank_embed1 {n : ℕ} (w : Cube n) : rank (embed1 w) = rank w + binomPrefix n (Finset.card w + 1)

theorem BooleanIsoperimetry.slice1_eq_filter {n k : ℕ} : slice1 (simplicialInitSeg (n + 1) k) = {w : Cube n | rank w + binomPrefix n (Finset.card w + 1) < k}

The upper slice of an initial segment as an explicit filter.

theorem BooleanIsoperimetry.cascade_pred_iff {n r t c rho : ℕ} (ht : t ≤ (n + 1).choose r) (hlo : binomPrefix n c ≤ rho) (hhi : rho < binomPrefix n (c + 1)) : rho + binomPrefix n (c + 1) < binomPrefix (n + 1) r + t ↔ rho < binomPrefix n (r - 1) + min t (choosePred n r)

theorem BooleanIsoperimetry.slice1_card_eq_cascade {n k r t : ℕ} (h : IsBinomialCascade (n + 1) k r t) : (slice1 (simplicialInitSeg (n + 1) k)).card = cascadeSlice1Value n r t

The upper slice cardinality matches the cascade value.

theorem BooleanIsoperimetry.slice_card_eq_cascade {n k p q : ℕ} (h : CascadeSplit n k p q) : (slice0 (simplicialInitSeg (n + 1) k)).card = p ∧ (slice1 (simplicialInitSeg (n + 1) k)).card = q

The actual Lean slice sizes of the simplicial initial segment match the components of the cascade split.

theorem BooleanIsoperimetry.cascade_split_add {n k p q : ℕ} (h : CascadeSplit n k p q) : p + q = k

The two components of a cascade split add back to the split mass.

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

In a cascade split the lower slice is at least as large as the upper slice.

theorem BooleanIsoperimetry.H_add_self_mono {n x y : ℕ} (h : x ≤ y) : H n x + x ≤ H n y + y

The strictly-increasing "mass" function H n x + x is monotone.

theorem BooleanIsoperimetry.simplicialLt_embed1_embed0 {n : ℕ} (u w : Cube n) : simplicialLt (embed1 u) (embed0 w) ↔ Finset.card u + 1 ≤ Finset.card w

Comparing an embed1 vertex with an embed0 vertex reduces to cardinalities.

theorem BooleanIsoperimetry.empty_mem_initSeg {n k : ℕ} (hk : 1 ≤ k) : ∅ ∈ simplicialInitSeg n k

The empty vertex lies in every nonempty initial segment.

theorem BooleanIsoperimetry.cascade_p_le_H_q {n k p q : ℕ} (h : CascadeSplit n k p q) (hq : 1 ≤ q) : p ≤ H n q

theorem BooleanIsoperimetry.gShift_embed0 {n : ℕ} (v : Cube n) : gShift (embed0 v) = embed0 (gShift v)

gShift on the 0-slice commutes with the embedding.

theorem BooleanIsoperimetry.gShift_embed1 {n : ℕ} (v : Cube n) : gShift (embed1 v) = if Finset.Nonempty v then embed1 (gShift v) else embed0 ∅

gShift on the 1-slice stays in the 1-slice, except for {n} which maps to ∅ in the 0-slice.

theorem BooleanIsoperimetry.H_eq_gShift_count (n k : ℕ) : H n k = {v : Cube n | rank (gShift v) < k}.card

Explicit boundary count: H n k counts vertices whose gShift lands in the segment.

theorem BooleanIsoperimetry.H_succ_cascade {n k p q : ℕ} (h : CascadeSplit n k p q) : H (n + 1) k = max (H n p) q + max (H n q) p

Recursion for H in terms of the canonical cascade split.

theorem BooleanIsoperimetry.cascadeSplit_one (n : ℕ) : CascadeSplit n 1 1 0

The canonical cascade split of the singleton initial segment is (1, 0).

theorem BooleanIsoperimetry.H_one (n : ℕ) : H n 1 = n + 1

The boundary of the singleton initial segment: H n 1 = n + 1.

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

theorem BooleanIsoperimetry.H_increment_eq_gShift_inv (n p : ℕ) (w : Cube n) (hw : rank w = p) : H n (p + 1) = H n p + {v : Cube n | gShift v = w}.card

The exact increment of H: passing from an initial segment of size p to p + 1 enlarges the closed neighbourhood by exactly the number of vertices whose gShift is the unique rank-p vertex w.

This provides the exact layer-profile increment structure for H, upgrading the lower bound in H_increment_lower to a full structural equality.

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