Simplicial coordinate compression

This file defines coordinate up/down compression operations on Boolean-cube families and proves basic neighborhood monotonicity and slice-pair facts.

def BooleanIsoperimetry.IsCoordinateUp {N : ℕ} (i : Fin N) (A A' : Finset (Cube N)) : Prop

A faithful relation for the Up compression of a family along a coordinate i. It pushes elements missing i to have i, provided the target is not already present.

Equations

• BooleanIsoperimetry.IsCoordinateUp i A A' = (A'.card = A.card ∧ ∀ (x : BooleanIsoperimetry.Cube N), x ∈ A' ↔ x ∈ A ∧ (i ∈ x ∨ insert i x ∈ A) ∨ i ∈ x ∧ x ∉ A ∧ Finset.erase x i ∈ A)

def BooleanIsoperimetry.IsCoordinateDown {N : ℕ} (i : Fin N) (B B' : Finset (Cube N)) : Prop

A faithful relation for the Down compression of a family along a coordinate i. It pushes elements containing i to miss i, provided the target is not already present.

Equations

• BooleanIsoperimetry.IsCoordinateDown i B B' = (B'.card = B.card ∧ ∀ (x : BooleanIsoperimetry.Cube N), x ∈ B' ↔ x ∈ B ∧ (i ∉ x ∨ Finset.erase x i ∈ B) ∨ i ∉ x ∧ x ∉ B ∧ insert i x ∈ B)

noncomputable def BooleanIsoperimetry.coordinateUp {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : Finset (Cube N)

Coordinate-up compression along i.

Equations

• BooleanIsoperimetry.coordinateUp i A = {x ∈ A | i ∈ x ∨ insert i x ∈ A} ∪ Finset.image (fun (x : BooleanIsoperimetry.Cube N) => insert i x) ({x ∈ A | i ∉ x ∧ insert i x ∉ A})

noncomputable def BooleanIsoperimetry.coordinateDown {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : Finset (Cube N)

Coordinate-down compression along i.

Equations

• BooleanIsoperimetry.coordinateDown i A = {x ∈ A | i ∉ x ∨ x.erase i ∈ A} ∪ Finset.image (fun (x : Finset (Fin N)) => x.erase i) ({x ∈ A | i ∈ x ∧ x.erase i ∉ A})

theorem BooleanIsoperimetry.coordinateUp_spec {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : IsCoordinateUp i A (coordinateUp i A)

theorem BooleanIsoperimetry.coordinateDown_spec {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : IsCoordinateDown i A (coordinateDown i A)

theorem BooleanIsoperimetry.IsCoordinateUp_unique {N : ℕ} {i : Fin N} {A A' A'' : Finset (Cube N)} (h1 : IsCoordinateUp i A A') (h2 : IsCoordinateUp i A A'') : A' = A''

theorem BooleanIsoperimetry.coordinateUp_eq {N : ℕ} {i : Fin N} {A A' : Finset (Cube N)} (hA : IsCoordinateUp i A A') : A' = coordinateUp i A

theorem BooleanIsoperimetry.IsCoordinateDown_unique {N : ℕ} {i : Fin N} {A A' A'' : Finset (Cube N)} (h1 : IsCoordinateDown i A A') (h2 : IsCoordinateDown i A A'') : A' = A''

theorem BooleanIsoperimetry.coordinateDown_eq {N : ℕ} {i : Fin N} {A A' : Finset (Cube N)} (hA : IsCoordinateDown i A A') : A' = coordinateDown i A

theorem BooleanIsoperimetry.mem_coordinateUp_iff {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) : x ∈ coordinateUp i A ↔ x ∈ A ∧ (i ∈ x ∨ insert i x ∈ A) ∨ i ∈ x ∧ x ∉ A ∧ Finset.erase x i ∈ A

Membership characterization of the explicit Up compression, read off directly from coordinateUp_spec.

theorem BooleanIsoperimetry.coordinateUp_mem_of_not_mem {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) (hix : i ∉ x) : x ∈ coordinateUp i A ↔ x ∈ A ∧ insert i x ∈ A

theorem BooleanIsoperimetry.coordinateUp_mem_of_mem {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) (hix : i ∈ x) : x ∈ coordinateUp i A ↔ x ∈ A ∨ Finset.erase x i ∈ A

theorem BooleanIsoperimetry.mem_coordinateDown_iff {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) : x ∈ coordinateDown i A ↔ x ∈ A ∧ (i ∉ x ∨ Finset.erase x i ∈ A) ∨ i ∉ x ∧ x ∉ A ∧ insert i x ∈ A

Membership characterization of the explicit Down compression, read off directly from coordinateDown_spec.

theorem BooleanIsoperimetry.coordinateDown_mem_of_mem {N : ℕ} (i : Fin N) (B : Finset (Cube N)) (x : Cube N) (hix : i ∈ x) : x ∈ coordinateDown i B ↔ x ∈ B ∧ Finset.erase x i ∈ B

theorem BooleanIsoperimetry.coordinateDown_mem_of_not_mem {N : ℕ} (i : Fin N) (B : Finset (Cube N)) (x : Cube N) (hix : i ∉ x) : x ∈ coordinateDown i B ↔ x ∈ B ∨ insert i x ∈ B

Hamming-distance helpers for the coordinate shadow inclusions

theorem BooleanIsoperimetry.hDist_comm {N : ℕ} (x y : Cube N) : hDist x y = hDist y x

theorem BooleanIsoperimetry.hDist_self_le_one {N : ℕ} (x : Cube N) : hDist x x ≤ 1

theorem BooleanIsoperimetry.hDist_erase_le_hDist {N : ℕ} (i : Fin N) (x y : Cube N) (h : hDist x y ≤ 1) : hDist (Finset.erase x i) (Finset.erase y i) ≤ 1

theorem BooleanIsoperimetry.hDist_insert_le_hDist {N : ℕ} (i : Fin N) (x y : Cube N) (h : hDist x y ≤ 1) : hDist (insert i x) (insert i y) ≤ 1

theorem BooleanIsoperimetry.hDist_insert_self_le_one {N : ℕ} (i : Fin N) (x : Cube N) : hDist (insert i x) x ≤ 1

theorem BooleanIsoperimetry.hDist_self_insert_le_one {N : ℕ} (i : Fin N) (x : Cube N) : hDist x (insert i x) ≤ 1

theorem BooleanIsoperimetry.hDist_erase_self_le_one {N : ℕ} (i : Fin N) (x : Cube N) : hDist (Finset.erase x i) x ≤ 1

theorem BooleanIsoperimetry.hDist_self_erase_le_one {N : ℕ} (i : Fin N) (x : Cube N) : hDist x (Finset.erase x i) ≤ 1

theorem BooleanIsoperimetry.eq_insert_of_hDist_le_one_of_not_mem_of_mem {N : ℕ} {x y : Cube N} {i : Fin N} (h : hDist x y ≤ 1) (hix : i ∉ x) (hiy : i ∈ y) : y = insert i x

theorem BooleanIsoperimetry.eq_erase_of_hDist_le_one_of_mem_of_not_mem {N : ℕ} {x y : Cube N} {i : Fin N} (h : hDist x y ≤ 1) (hix : i ∈ x) (hiy : i ∉ y) : y = Finset.erase x i

theorem BooleanIsoperimetry.neighborhood_coordinateUp_subset {N : ℕ} {i : Fin N} {A : Finset (Cube N)} : neighborhood 1 (coordinateUp i A) ⊆ coordinateUp i (neighborhood 1 A)

Coordinate Up shadow inclusion (PDF Frankl-Füredi). The closed unit neighborhood of an Up-compressed family is contained in the Up-compression of the neighborhood. This is the classical "compression does not expand the shadow" fact.

theorem BooleanIsoperimetry.neighborhood_coordinateDown_subset {N : ℕ} {i : Fin N} {A : Finset (Cube N)} : neighborhood 1 (coordinateDown i A) ⊆ coordinateDown i (neighborhood 1 A)

Coordinate Down shadow inclusion (PDF Frankl-Füredi). The mirror of neighborhood_coordinateUp_subset for Down compression.

noncomputable def BooleanIsoperimetry.compressionPotential {N : ℕ} (A : Finset (Cube N)) : ℕ

The Frankl-Füredi compression potential used for well-founded descent: the sum of simplicial ranks of all vertices in the family. Coordinate and within-layer shifts are expected to strictly reduce this potential unless they are already fixed points.

Equations

• BooleanIsoperimetry.compressionPotential A = ∑ x ∈ A, BooleanIsoperimetry.rank x

noncomputable def BooleanIsoperimetry.pairCompressionPotential {N : ℕ} (A B : Finset (Cube N)) : ℕ

The paired version of compressionPotential, matching the two-slice Frankl-Füredi compression process.

Equations

• BooleanIsoperimetry.pairCompressionPotential A B = BooleanIsoperimetry.compressionPotential A + BooleanIsoperimetry.compressionPotential B

def BooleanIsoperimetry.IsCoordinateUpFixed {N : ℕ} (A : Finset (Cube N)) : Prop

A family is fixed by all currently formalized Up-compressions. This is only the coordinate part of the PDF terminal condition; the within-layer/colex shifts still have to be added before fixed points can be identified with simplicial initial segments.

Equations

• BooleanIsoperimetry.IsCoordinateUpFixed A = ∀ (i : Fin N), BooleanIsoperimetry.IsCoordinateUp i A A

def BooleanIsoperimetry.IsCoordinateDownFixed {N : ℕ} (A : Finset (Cube N)) : Prop

A family is fixed by all currently formalized Down-compressions.

Equations

• BooleanIsoperimetry.IsCoordinateDownFixed A = ∀ (i : Fin N), BooleanIsoperimetry.IsCoordinateDown i A A

theorem BooleanIsoperimetry.coordinateUp_card_eq {N : ℕ} {i : Fin N} {A A' : Finset (Cube N)} (hA : IsCoordinateUp i A A') : A'.card = A.card

theorem BooleanIsoperimetry.coordinateDown_card_eq {N : ℕ} {i : Fin N} {B B' : Finset (Cube N)} (hB : IsCoordinateDown i B B') : B'.card = B.card

theorem BooleanIsoperimetry.coordinateUp_neighborhood_card_le {N : ℕ} {i : Fin N} {A A' : Finset (Cube N)} (hA : IsCoordinateUp i A A') : (neighborhood 1 A').card ≤ (neighborhood 1 A).card

PDF compression lemma (Up move). An Up-compression along coordinate i does not increase the closed unit neighborhood (vertex boundary) of a family. This is the classical Frankl–Füredi / Harper statement "the i-compression does not increase the shadow", here in the closed-neighborhood form |N(C_i^↑ A)| ≤ |N(A)|. It is a genuine combinatorial obligation about the concrete IsCoordinateUp relation, not a missing definition: every object in the statement is already formalized. It is proved in the PDF by the inclusion N(C_i^↑ A) ⊆ C_i^↑(N A) together with cardinality-preservation of C_i^↑.

theorem BooleanIsoperimetry.coordinateDown_neighborhood_card_le {N : ℕ} {i : Fin N} {B B' : Finset (Cube N)} (hB : IsCoordinateDown i B B') : (neighborhood 1 B').card ≤ (neighborhood 1 B).card

PDF compression lemma (Down move). The mirror of coordinateUp_neighborhood_card_le: a Down-compression along coordinate i does not increase the closed unit neighborhood, |N(C_i^↓ B)| ≤ |N(B)|. Symmetric to the Up case under the coordinate-i flip isometry of the cube.

noncomputable def BooleanIsoperimetry.downMap {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) : Cube N

The explicit single-vertex Down map underlying coordinateDown: a vertex containing i whose i-erasure is not already present is pushed down to that erasure; every other vertex is fixed.

Equations

• BooleanIsoperimetry.downMap i A x = if i ∈ x ∧ Finset.erase x i ∉ A then Finset.erase x i else x

theorem BooleanIsoperimetry.simplicialLt_erase_self {N : ℕ} {i : Fin N} {x : Cube N} (hi : i ∈ x) : simplicialLt (Finset.erase x i) x

Erasing a present coordinate is a strictly earlier simplicial vertex.

theorem BooleanIsoperimetry.downMap_rank_le {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (x : Cube N) : rank (downMap i A x) ≤ rank x

The Down map never increases simplicial rank.

theorem BooleanIsoperimetry.downMap_injOn {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : Set.InjOn (downMap i A) ↑A

The Down map is injective on its family.

theorem BooleanIsoperimetry.coordinateDown_eq_image {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : coordinateDown i A = Finset.image (downMap i A) A

coordinateDown is the image of the family under downMap.

theorem BooleanIsoperimetry.coordinateDown_potential_le {N : ℕ} (i : Fin N) (A : Finset (Cube N)) : compressionPotential (coordinateDown i A) ≤ compressionPotential A

coordinateDown never increases the rank potential.

theorem BooleanIsoperimetry.exists_downMap_ne_of_ne {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (hne : coordinateDown i A ≠ A) : ∃ x ∈ A, downMap i A x ≠ x

If a coordinate Down-compression actually changes the family, it strictly moves at least one vertex down.

theorem BooleanIsoperimetry.coordinateDown_potential_lt_of_ne {N : ℕ} (i : Fin N) (A : Finset (Cube N)) (hne : coordinateDown i A ≠ A) : compressionPotential (coordinateDown i A) < compressionPotential A

Coordinate Down-compression strictly decreases the rank potential when it moves something. Combined with the proven size- and boundary-control (coordinateDown_card_eq, coordinateDown_neighborhood_card_le) this gives any non-Down-fixed family an explicit Frankl–Füredi compression descent witness.

def BooleanIsoperimetry.IsColexShift {N : ℕ} (A A' : Finset (Cube N)) : Prop

Within-layer colexicographic shift. It moves an element to a strictly earlier element in the same layer (same cardinality), provided the target is not already in the family.

Equations

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

def BooleanIsoperimetry.IsColexShiftFixed {N : ℕ} (A : Finset (Cube N)) : Prop

A family is stable under all within-layer colex shifts.

Equations

• BooleanIsoperimetry.IsColexShiftFixed A = ∀ (A' : Finset (BooleanIsoperimetry.Cube N)), ¬BooleanIsoperimetry.IsColexShift A A'

def BooleanIsoperimetry.IsLowerLevelSaturated {N : ℕ} (A : Finset (Cube N)) : Prop

The missing level-saturation condition in the PDF compression route: once the compression process keeps a vertex of a given Hamming level, every lower Hamming level is already completely filled. Coordinate Down-compressions alone only fill coordinate subfaces of a present vertex; they do not imply this global saturation across a whole level.

Equations

• BooleanIsoperimetry.IsLowerLevelSaturated A = ∀ ⦃x y : BooleanIsoperimetry.Cube N⦄, Finset.card x < Finset.card y → y ∈ A → x ∈ A

theorem BooleanIsoperimetry.lowerLevelSaturated_colexFixed_is_downClosed {N : ℕ} (A : Finset (Cube N)) (hLower : IsLowerLevelSaturated A) (hColex : IsColexShiftFixed A) (x y : Cube N) : simplicialLe x y → y ∈ A → x ∈ A

theorem BooleanIsoperimetry.coordinate_compressed_is_downClosed {N : ℕ} (A : Finset (Cube N)) (_hDown : IsCoordinateDownFixed A) (hLower : IsLowerLevelSaturated A) (hColex : IsColexShiftFixed A) (x y : Cube N) : simplicialLe x y → y ∈ A → x ∈ A

noncomputable def BooleanIsoperimetry.initialSlicePair (N a b : ℕ) : Finset (Cube (N + 1))

The embedded two-slice family whose lower slice is the initial segment of size a and whose upper slice is the initial segment of size b. This is the PDF-language object behind the scalar Macaulay split step.

Equations

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

theorem BooleanIsoperimetry.initialSlicePair_embed0_injective {N : ℕ} : Function.Injective embed0

theorem BooleanIsoperimetry.initialSlicePair_last_not_mem_embed0 {N : ℕ} (x : Cube N) : Fin.last N ∉ embed0 x

theorem BooleanIsoperimetry.initialSlicePair_embed1_injective {N : ℕ} : Function.Injective embed1

theorem BooleanIsoperimetry.slice0_initialSlicePair {N a b : ℕ} : slice0 (initialSlicePair N a b) = simplicialInitSeg N a

theorem BooleanIsoperimetry.slice1_initialSlicePair {N a b : ℕ} : slice1 (initialSlicePair N a b) = simplicialInitSeg N b

theorem BooleanIsoperimetry.neighborhood_initialSlicePair_card {N a b : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : (neighborhood 1 (initialSlicePair N a b)).card = max (H N a) b + max (H N b) a

theorem BooleanIsoperimetry.card_le_two_pow {N : ℕ} (S : Finset (Cube N)) : S.card ≤ 2 ^ N

Every family on the N-cube has cardinality at most 2 ^ N.