Frankl-Furedi compression layer

This file formalizes paired compression and terminalization infrastructure for families in the Boolean cube, connecting compressed families to canonical simplicial initial segments.

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

A family of vertices is a simplicial initial segment if it equals the canonical simplicial prefix of its cardinality.

Equations

• BooleanIsoperimetry.IsSimplicial A = (A = BooleanIsoperimetry.simplicialInitSeg N A.card)

noncomputable def BooleanIsoperimetry.embeddedPair (N : ℕ) (A B : Finset (Cube N)) : Finset (Cube (N + 1))

The embedded two-slice family in Q_{N+1} whose lower slice is A and upper slice is B.

Equations

• BooleanIsoperimetry.embeddedPair N A B = Finset.image BooleanIsoperimetry.embed0 A ∪ Finset.image BooleanIsoperimetry.embed1 B

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

embed0 is injective. Kept local to the paired-compression layer so the embedded-pair slice lemmas do not depend on the later scalar bridge file.

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

The top coordinate never lies in an embed0 image.

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

embed1 is injective.

theorem BooleanIsoperimetry.slice0_embeddedPair {N : ℕ} (A B : Finset (Cube N)) : slice0 (embeddedPair N A B) = A

The lower slice of an embedded pair is exactly its first component.

theorem BooleanIsoperimetry.slice1_embeddedPair {N : ℕ} (A B : Finset (Cube N)) : slice1 (embeddedPair N A B) = B

The upper slice of an embedded pair is exactly its second component.

theorem BooleanIsoperimetry.neighborhood_embeddedPair_card {N : ℕ} (A B : Finset (Cube N)) : (neighborhood 1 (embeddedPair N A B)).card = (neighborhood 1 A ∪ B).card + (neighborhood 1 B ∪ A).card

Exact neighborhood decomposition for an embedded two-slice family. This is the literal cardinality of the closed unit neighborhood in Q_{N+1}.

theorem BooleanIsoperimetry.disjoint_embeddedPair {N : ℕ} (A B : Finset (Cube N)) : Disjoint (Finset.image embed0 A) (Finset.image embed1 B)

theorem BooleanIsoperimetry.embeddedPair_card {N : ℕ} (A B : Finset (Cube N)) : (embeddedPair N A B).card = A.card + B.card

theorem BooleanIsoperimetry.embeddedPair_eq_of_slice_eq {N : ℕ} {A : Finset (Cube (N + 1))} {P Q : Finset (Cube N)} (h0 : slice0 A = P) (h1 : slice1 A = Q) : A = embeddedPair N P Q

noncomputable def BooleanIsoperimetry.PairShadowCost (N : ℕ) (A B : Finset (Cube N)) : ℕ

The Frankl-Füredi paired compression slice lower-bound functional for two slices A and B.

For arbitrary slices this is not the literal cardinality of the embedded family's neighborhood. The true cardinality has union terms |N(A) ∪ B| + |N(B) ∪ A|; this functional replaces each union by the cheaper lower bound max |N(A)| |B|. For nested/canonical terminal pairs the two coincide.

Equations

• BooleanIsoperimetry.PairShadowCost N A B = max (BooleanIsoperimetry.neighborhood 1 A).card B.card + max (BooleanIsoperimetry.neighborhood 1 B).card A.card

theorem BooleanIsoperimetry.PairShadowCost_le_neighborhood_embeddedPair_card {N : ℕ} (A B : Finset (Cube N)) : PairShadowCost N A B ≤ (neighborhood 1 (embeddedPair N A B)).card

The paired slice functional is a lower bound for the literal neighborhood size of the embedded family.

theorem BooleanIsoperimetry.PairShadowCost_initSeg_eq_max_H {N a b : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : PairShadowCost N (simplicialInitSeg N a) (simplicialInitSeg N b) = max (H N a) b + max (H N b) a

On canonical initial segments the paired slice functional is exactly the scalar max expression used in the cascade recurrence.

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

For canonical initial segments the literal embedded-neighborhood cardinality also evaluates to the scalar max expression, because all four slice families are nested initial segments.

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

The family-level nesting predicate used by the terminal Frankl-Füredi configuration: one slice is contained in the other. Kept as descriptive scaffolding for the geometric picture; it is intentionally not strong enough on its own to pin down the canonical cascade pair (see IsCanonicalCascadePair), so no theorem below claims a nested pair is automatically canonical.

Equations

• BooleanIsoperimetry.IsNestedPair A B = (A ⊆ B ∨ B ⊆ A)

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

A pair of families is weakly terminal for paired compression if they are both simplicial and nested. This is a necessary (not sufficient) feature of the genuine terminal configuration: it does not by itself force (A, B) to be the canonical cascade split of its total, because the individual volumes (A.card, B.card) need not coincide with the cascade split (p, q) of A.card + B.card. The earlier terminalPair_cost_eq_canonical / terminalPair_is_cascade_initial leaves stated equalities for every such pair and were therefore false; they have been removed in favour of the honest descent leaf pairedCompression_reaches_canonical below, which targets the strong IsCanonicalCascadePair predicate directly.

Equations

• BooleanIsoperimetry.IsWeaklyTerminalPair A B = (BooleanIsoperimetry.IsSimplicial A ∧ BooleanIsoperimetry.IsSimplicial B ∧ BooleanIsoperimetry.IsNestedPair A B)

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

The strong canonical / terminal predicate. A pair (A, B) is a canonical cascade pair when both slices are the simplicial initial segments named by the canonical cascade split (p, q) of their combined volume A.card + B.card. This is the genuine Frankl-Füredi terminal object: it fixes not only that the slices are simplicial and nested, but that the split of the total is the canonical cascade split. By cascadeSplit_unique the witnesses p, q are determined by the pair.

Equations

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

noncomputable def BooleanIsoperimetry.canonicalPairOfTotal (N total : ℕ) : Finset (Cube N) × Finset (Cube N)

Returns the canonical cascade pair for a given total volume.

Equations

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

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

The distance from a pair (A, B) to the canonical cascade pair of the same total volume, measured by symmetric difference size.

Equations

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

inductive BooleanIsoperimetry.IsPairedCompressionStep {N : ℕ} (A B : Finset (Cube N)) : Finset (Cube N) → Finset (Cube N) → Prop

A structurally meaningful paired step on two slice families.

It is either a coordinate-wise Up/Down compression (which preserves individual sizes), or the oriented weak-terminal cascade phase. The cascade constructor is intentionally not just "same total weak-terminal pair": weak terminality alone does not determine the Frankl-Füredi cascade split. In particular, at total 4 in dimension 2, the canonical split (3, 1) and the weakly terminal split (2, 2) have different costs, so an unoriented constructor would allow false cost-increasing moves out of the canonical pair.

The cascade phase therefore carries the real obligations that still have to be proved from the PDF/Macaulay argument: the target is the canonical cascade pair for the same total, the cost does not increase, and the distance potential strictly decreases. These fields are deliberately not inferred from weak terminality alone; they are supplied by the named cascade-exchange lemma below.

• coord {N : ℕ} {A B : Finset (Cube N)} (i : Fin N) (A' B' : Finset (Cube N)) (hA : IsCoordinateUp i A A') (hB : IsCoordinateDown i B B') : IsPairedCompressionStep A B A' B'
• cascade {N : ℕ} {A B : Finset (Cube N)} (A' B' : Finset (Cube N)) (hTerm : IsWeaklyTerminalPair A B) (hTarget : IsCanonicalCascadePair A' B') (hTotal : A'.card + B'.card = A.card + B.card) (hCost : PairShadowCost N A' B' ≤ PairShadowCost N A B) (hProgress : distanceToCanonical A' B' < distanceToCanonical A B) : IsPairedCompressionStep A B A' B'

theorem BooleanIsoperimetry.paired_step_total_mass {N : ℕ} {A B A' B' : Finset (Cube N)} (step : IsPairedCompressionStep A B A' B') : A'.card + B'.card = A.card + B.card

theorem BooleanIsoperimetry.paired_coordinate_step_cost_nonincrease {N : ℕ} {A B A' B' : Finset (Cube N)} {i : Fin N} (hA : IsCoordinateUp i A A') (hB : IsCoordinateDown i B B') : PairShadowCost N A' B' ≤ PairShadowCost N A B

One paired coordinate Up/Down compression does not increase the two-slice Frankl-Füredi cost.

This is now a sorry-free reduction to the two named PDF shadow-monotonicity lemmas above: the slice cardinalities are preserved by the compression (hA.1, hB.1), and max is monotone in its first argument, so the cost bound follows term-by-term from |N(A')| ≤ |N(A)| and |N(B')| ≤ |N(B)|. No scalar Harper minimization is used.

theorem BooleanIsoperimetry.paired_step_cost_nonincrease {N : ℕ} {A B A' B' : Finset (Cube N)} (step : IsPairedCompressionStep A B A' B') : PairShadowCost N A' B' ≤ PairShadowCost N A B

noncomputable def BooleanIsoperimetry.blockReplace {N : ℕ} (U V S : Cube N) : Cube N

PDF block replacement on a single vertex/set: S - U + V = (S \ U) ∪ V.

Equations

• BooleanIsoperimetry.blockReplace U V S = S \ U ∪ V

theorem BooleanIsoperimetry.blockReplace_recover {N : ℕ} {U V S : Cube N} (hUS : U ⊆ S) (hVS : Disjoint V S) : blockReplace U V S \ V ∪ U = S

Block recovery. When U ⊆ S and V is disjoint from S, the inverse move · - V + U undoes blockReplace U V. This is what makes the paper's 𝒰 one-to-one.

noncomputable def BooleanIsoperimetry.familyUpMap {N : ℕ} (U V : Cube N) (𝒜 : Finset (Cube N)) (S : Cube N) : Cube N

The paper's 𝒰 on a single set, relative to the family 𝒜.

Equations

• BooleanIsoperimetry.familyUpMap U V 𝒜 S = if U ⊆ S ∧ Disjoint V S ∧ BooleanIsoperimetry.blockReplace U V S ∉ 𝒜 then BooleanIsoperimetry.blockReplace U V S else S

noncomputable def BooleanIsoperimetry.familyDownMap {N : ℕ} (U V : Cube N) (ℬ : Finset (Cube N)) (S : Cube N) : Cube N

The paper's 𝒟 on a single set, relative to the family ℬ.

Equations

• BooleanIsoperimetry.familyDownMap U V ℬ S = if V ⊆ S ∧ Disjoint U S ∧ BooleanIsoperimetry.blockReplace V U S ∉ ℬ then BooleanIsoperimetry.blockReplace V U S else S

noncomputable def BooleanIsoperimetry.familyUp {N : ℕ} (U V : Cube N) (𝒜 : Finset (Cube N)) : Finset (Cube N)

The PDF Up operation on a whole family: 𝒰(𝒜) = { 𝒰(S) : S ∈ 𝒜 }.

Equations

• BooleanIsoperimetry.familyUp U V 𝒜 = Finset.image (BooleanIsoperimetry.familyUpMap U V 𝒜) 𝒜

noncomputable def BooleanIsoperimetry.familyDown {N : ℕ} (U V : Cube N) (ℬ : Finset (Cube N)) : Finset (Cube N)

The PDF Down operation on a whole family: 𝒟(ℬ) = { 𝒟(S) : S ∈ ℬ }.

Equations

• BooleanIsoperimetry.familyDown U V ℬ = Finset.image (BooleanIsoperimetry.familyDownMap U V ℬ) ℬ

theorem BooleanIsoperimetry.familyUpMap_injOn {N : ℕ} (U V : Cube N) (𝒜 : Finset (Cube N)) : Set.InjOn (familyUpMap U V 𝒜) ↑𝒜

The paper's 𝒰 is one-to-one on its family.

theorem BooleanIsoperimetry.familyDownMap_injOn {N : ℕ} (U V : Cube N) (ℬ : Finset (Cube N)) : Set.InjOn (familyDownMap U V ℬ) ↑ℬ

The paper's 𝒟 is one-to-one on its family.

theorem BooleanIsoperimetry.familyUp_card {N : ℕ} (U V : Cube N) (𝒜 : Finset (Cube N)) : (familyUp U V 𝒜).card = 𝒜.card

Cardinality preservation for 𝒰 (|𝒰(𝒜)| = |𝒜|).

theorem BooleanIsoperimetry.familyDown_card {N : ℕ} (U V : Cube N) (ℬ : Finset (Cube N)) : (familyDown U V ℬ).card = ℬ.card

Cardinality preservation for 𝒟 (|𝒟(ℬ)| = |ℬ|).

theorem BooleanIsoperimetry.familyUpDown_total {N : ℕ} (U V : Cube N) (𝒜 ℬ : Finset (Cube N)) : (familyUp U V 𝒜).card + (familyDown U V ℬ).card = 𝒜.card + ℬ.card

A single paired Up/Down move preserves the total volume |𝒜| + |ℬ|.

noncomputable def BooleanIsoperimetry.familyHammingDist {N : ℕ} (𝒜 ℬ : Finset (Cube N)) : ℕ

PDF family Hamming distance d(𝒜, ℬ) = min { |A △ B| : A ∈ 𝒜, B ∈ ℬ } (item 3 of the desired infrastructure: the separation functional the paper's paired move is required to preserve). Defined as 0 on an empty product, which never occurs for the nonempty families the paper compresses.

Equations

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

theorem BooleanIsoperimetry.distanceToCanonical_zero_canonical {N : ℕ} (A B : Finset (Cube N)) (h : distanceToCanonical A B = 0) : IsCanonicalCascadePair A B

Terminal characterization. A pair at distanceToCanonical = 0 is the canonical cascade pair of its total. This is the Lean form of the paper's terminal statement "no admissible move ⟹ opposite-centered Hamming spheres": the only fixed point of the descent is the canonical configuration.

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

A family is fully compressed for the Frankl–Füredi single-family compression process when it is lower-level saturated and fixed by every within-layer colex shift. These are exactly the two terminal conditions whose combination lowerLevelSaturated_colexFixed_is_downClosed shows forces simplicial down-closure (the coordinate-Down-fixedness used in coordinate_compressed_is_downClosed is not even needed — its argument there is discarded — so it is dropped here to keep the terminal set as large, and the descent leaf below as weak, as possible).

Equations

• BooleanIsoperimetry.IsFullyCompressed A = (BooleanIsoperimetry.IsLowerLevelSaturated A ∧ BooleanIsoperimetry.IsColexShiftFixed A)

theorem BooleanIsoperimetry.fullyCompressed_eq_initSeg {N : ℕ} (A : Finset (Cube N)) (h : IsFullyCompressed A) : A = simplicialInitSeg N A.card

Terminal ⟹ Hamming sphere. A fully compressed family is exactly the simplicial initial segment of its own size. This is the sorry-free Lean form of "no admissible compression move ⟹ opposite-centered Hamming sphere": combine the down-closure produced by the terminal conditions (lowerLevelSaturated_colexFixed_is_downClosed) with the structural fact that a down-closed family is an initial segment (downwardClosed_eq_initSeg).

theorem BooleanIsoperimetry.swap_potential_lt {N : ℕ} {A A' : Finset (Cube N)} {x y : Cube N} (hx : x ∈ A) (hy : y ∉ A) (hlt : simplicialLt y x) (heq : A' = insert y (A.erase x)) : compressionPotential A' < compressionPotential A

A rank-lowering single-set swap strictly decreases the rank potential compressionPotential = ∑ rank: replacing x by an earlier set y (simplicialLt y x, hence rank y < rank x) lowers the sum.

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

The precise residual Phase-1 descent target. IsDownFixedResidualShift A A' records that A' is a valid single Frankl–Füredi compression descent target for a coordinate-Down-fixed family: same size, no larger unit neighborhood, strictly smaller rank potential.

The intended witnesses are the paper colex/level shifts above, together with the separate boundary monotonicity theorems for those moves.

Equations

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

theorem BooleanIsoperimetry.residualShift_card {N : ℕ} {A A' : Finset (Cube N)} (h : IsDownFixedResidualShift A A') : A'.card = A.card

theorem BooleanIsoperimetry.residualShift_neighborhood_card_le {N : ℕ} {A A' : Finset (Cube N)} (h : IsDownFixedResidualShift A A') : (neighborhood 1 A').card ≤ (neighborhood 1 A).card

theorem BooleanIsoperimetry.residualShift_potential_lt {N : ℕ} {A A' : Finset (Cube N)} (h : IsDownFixedResidualShift A A') : compressionPotential A' < compressionPotential A

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

A singleton-coordinate block colex move. This is a useful special case of the paper's block operation, but it is not the full terminalization move for IsColexShiftFixed: a colex failure may replace an arbitrary same-layer vertex by an earlier one, not just one coordinate by another.

Equations

• BooleanIsoperimetry.IsPaperColexBlockMove A A' i j = (A' = BooleanIsoperimetry.familyUp {i} {j} A ∧ A' ≠ A ∧ i < j)

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

The pure within-layer Frankl–Füredi terminalization move: replace elements in the same Hamming layer using either a single-vertex colex shift or a single-coordinate colex block move.

This predicate describes only the move (rule 4): it carries no boundary certificate. Boundary monotonicity is genuinely a property of the selected move, not of every colex shift — the finite checker verify_colexShift_boundary_small.py exhibits an N = 4 down-fixed, lower-level-saturated family with a single-vertex colex shift that strictly increases the closed unit neighborhood. Hence the boundary bound must be proved for the specific KK-selected move at the existence site (not_colexShiftFixed_exists_paperColexShiftMove), never asserted for the whole predicate.

Equations

• BooleanIsoperimetry.IsPaperColexShiftMove A A' = (BooleanIsoperimetry.IsColexShift A A' ∨ ∃ (i : Fin N) (j : Fin N), BooleanIsoperimetry.IsPaperColexBlockMove A A' i j)

def BooleanIsoperimetry.IsPaperLevelBlockMove {N : ℕ} (A A' : Finset (Cube N)) (U V : Cube N) : Prop

A nontrivial level-changing block move satisfying the paper's residual conditions.

Equations

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

inductive BooleanIsoperimetry.IsPaperResidualStep {N : ℕ} (A : Finset (Cube N)) : Finset (Cube N) → Prop

One admissible residual compression step in the paper's reduction.

• colexShift {N : ℕ} {A A' : Finset (Cube N)} : IsPaperColexShiftMove A A' → (neighborhood 1 A').card ≤ (neighborhood 1 A).card → IsCoordinateDownFixed A → IsLowerLevelSaturated A → IsPaperResidualStep A A'
• levelBlock {N : ℕ} {A A' : Finset (Cube N)} {U V : Cube N} : IsPaperLevelBlockMove A A' U V → IsPaperResidualStep A A'

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

The transitive closure of admissible residual compression steps.

Equations

• BooleanIsoperimetry.IsPaperResidualSequence A A' = Relation.TransGen BooleanIsoperimetry.IsPaperResidualStep A A'

Block-move rank-descent infrastructure

The two *_potential_lt leaves are honest rank-descent facts, proved here with no Kruskal–Katona / Harper input. compressionPotential = ∑ rank, and familyUp U V acts on each set S by familyUpMap, which either leaves S fixed or replaces it with blockReplace U V S = (S \ U) ∪ V. We show every replaced set is simplicially smaller, so the rank sum strictly drops once at least one set actually moves (familyUp U V A ≠ A).

theorem BooleanIsoperimetry.cubeToNat_union_disjoint {N : ℕ} {s t : Cube N} (h : Disjoint s t) : cubeToNat (s ∪ t) = cubeToNat s + cubeToNat t

Binary value is additive over disjoint unions.

theorem BooleanIsoperimetry.cubeToNat_sdiff_add {N : ℕ} {U S : Cube N} (h : U ⊆ S) : cubeToNat (S \ U) + cubeToNat U = cubeToNat S

Binary value splits across a subset/complement.

theorem BooleanIsoperimetry.cubeToNat_le_of_subset {N : ℕ} {U S : Cube N} (h : U ⊆ S) : cubeToNat U ≤ cubeToNat S

theorem BooleanIsoperimetry.blockReplace_card {N : ℕ} {U V S : Cube N} (hUS : U ⊆ S) (hVS : Disjoint V S) : Finset.card (blockReplace U V S) = Finset.card S - Finset.card U + Finset.card V

Cardinality of a block replacement (S \ U) ∪ V when U ⊆ S and V is disjoint from S.

theorem BooleanIsoperimetry.cubeToNat_blockReplace {N : ℕ} {U V S : Cube N} (hUS : U ⊆ S) (hVS : Disjoint V S) : cubeToNat (blockReplace U V S) = cubeToNat S - cubeToNat U + cubeToNat V

Binary value of a block replacement.

theorem BooleanIsoperimetry.blockReplace_simplicialLt_level {N : ℕ} {U V S : Cube N} (hUS : U ⊆ S) (hVS : Disjoint V S) (hcard : Finset.card V < Finset.card U) : simplicialLt (blockReplace U V S) S

Level block move descent. Replacing block U ⊆ S by a strictly smaller block V (disjoint from S, V.card < U.card) yields a simplicially smaller set (lower Hamming weight comes first in the simplicial order).

theorem BooleanIsoperimetry.blockReplace_simplicialLt_colex {N : ℕ} {U V S : Cube N} (hUS : U ⊆ S) (hVS : Disjoint V S) (hcard : Finset.card U = Finset.card V) (hVU : simplicialLt V U) : simplicialLt (blockReplace U V S) S

Colex block move descent. Replacing block U ⊆ S by an equal-size block V (disjoint from S) that is simplicially below U yields a simplicially smaller set: equal weight, but a strictly larger binary value because cubeToNat U < cubeToNat V.

theorem BooleanIsoperimetry.familyUp_potential_lt_of_blockLt {N : ℕ} {U V : Cube N} {A : Finset (Cube N)} (hne : familyUp U V A ≠ A) (hlt : ∀ (S : Cube N), U ⊆ S → Disjoint V S → simplicialLt (blockReplace U V S) S) : compressionPotential (familyUp U V A) < compressionPotential A

Block-move potential descent (general). If every replaced set drops in the simplicial order, then a nontrivial familyUp U V move (familyUp U V A ≠ A) strictly decreases the rank potential compressionPotential = ∑ rank.

def BooleanIsoperimetry.IsUVAdmissibleForFamily {N : ℕ} (A : Finset (Cube N)) (U V : Cube N) : Prop

Admissibility for a paper block move, in the mathlib UV orientation. The paper's 𝒰-move (familyUp U V) is UV.compression V U (it removes the U block and inserts the disjoint V block). The Frankl–Füredi/Kruskal–Katona shadow-nonincrease hypothesis for UV.compression V U A (Finset.UV.card_shadow_compression_le V U) is ∀ x ∈ V, ∃ y ∈ U, IsCompressed (V.erase x) (U.erase y) A; phrased back through the block-move dictionary (familyUp_eq_UV_compression) this is exactly the predicate below. Note the quantifier orientation (x ∈ V, y ∈ U, erasing U at y and V at x) is the one that matches mathlib, not the transposed one.

Equations

• BooleanIsoperimetry.IsUVAdmissibleForFamily A U V = ∀ x ∈ V, ∃ y ∈ U, BooleanIsoperimetry.familyUp (Finset.erase U y) (Finset.erase V x) A = A

theorem BooleanIsoperimetry.compress_VU_eq_blockReplace {N : ℕ} {U V : Cube N} (hd : Disjoint U V) (S : Cube N) : UV.compress V U S = if U ⊆ S ∧ Disjoint V S then blockReplace U V S else S

Per-set block dictionary. For disjoint blocks U, V the mathlib single-element compression UV.compress V U agrees with the project's block replacement: it is blockReplace U V S = (S \ U) ∪ V exactly when U ⊆ S and V is disjoint from S, and the identity otherwise. (Disjointness of U, V is what makes (S ∪ V) \ U = (S \ U) ∪ V.)

theorem BooleanIsoperimetry.familyUp_eq_UV_compression {N : ℕ} (A : Finset (Cube N)) {U V : Cube N} (hd : Disjoint U V) : familyUp U V A = UV.compression V U A

Block-move ↔ mathlib UV-compression dictionary. For disjoint blocks the project's family 𝒰-move is literally mathlib's UV-compression with the slots swapped: familyUp U V A = UV.compression V U A. Proved set-theoretically from compress_VU_eq_blockReplace, identifying the image form (familyUpMap, which keeps a set fixed when its replacement already lies in A) with mathlib's "stay / move" split (UV.mem_compression).

theorem BooleanIsoperimetry.familyUp_shadow_card_le_of_admissible {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hUV : IsUVAdmissibleForFamily A U V) : (familyUp U V A).shadow.card ≤ A.shadow.card

Block move does not increase the shadow (Frankl–Füredi / Kruskal–Katona). For disjoint admissible blocks the 𝒰-move's shadow is no larger than the original's. This is the mathlib UV-compression shadow bound Finset.UV.card_shadow_compression_le transported across the block dictionary.

theorem BooleanIsoperimetry.blockReplace_compl {N : ℕ} {U V : Cube N} (hd : Disjoint U V) (S : Cube N) : (blockReplace U V S)ᶜ = blockReplace V U Sᶜ

Block replacement commutes with vertex complementation. For disjoint blocks, complementing the result of replacing U by V is the same as replacing V by U in the complemented set: (blockReplace U V S)ᶜ = blockReplace V U Sᶜ. This is the cube self-duality that turns the lower shadow into the upper shadow.

theorem BooleanIsoperimetry.familyUpMap_compl {N : ℕ} {U V : Cube N} (hd : Disjoint U V) (A : Finset (Cube N)) (S : Cube N) : (familyUpMap U V A S)ᶜ = familyUpMap V U A.compls Sᶜ

The per-set 𝒰-map intertwines with complementation: applying familyUpMap U V A then complementing equals complementing then applying the swapped map familyUpMap V U (Aᶜˢ). (The membership guard ∉ A becomes ∉ Aᶜˢ under the complement bijection.)

theorem BooleanIsoperimetry.familyUp_compls {N : ℕ} {U V : Cube N} (hd : Disjoint U V) (A : Finset (Cube N)) : (familyUp U V A).compls = familyUp V U A.compls

The 𝒰-move commutes with vertex complementation at family level. For disjoint blocks, (familyUp U V A)ᶜˢ = familyUp V U (Aᶜˢ). This is what reduces upper-shadow control of a block move to lower-shadow control of the dual block move on the complemented family.

theorem BooleanIsoperimetry.familyUp_upperShadow_card_le_of_admissible {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hUV' : IsUVAdmissibleForFamily A.compls V U) : (familyUp U V A).compls.shadow.card ≤ A.compls.shadow.card

Block move does not increase the upper shadow (the dual of familyUp_shadow_card_le_of_admissible). Phrased via the complement bijection (#(∂⁺ F) = #(∂ Fᶜˢ), mathlib Finset.shadow_compls): the lower shadow of the complemented image is bounded by that of Aᶜˢ. Needs the dual admissibility IsUVAdmissibleForFamily (Aᶜˢ) V U of the complemented family for the swapped blocks — admissibility of the lower-shadow move alone does not control the upper shadow (a finite counterexample exists already at N = 3).

theorem BooleanIsoperimetry.neighborhood_one_eq_self_union_shadow_upShadow {N : ℕ} (A : Finset (Cube N)) : neighborhood 1 A = A ∪ A.shadow ∪ A.upShadow

Closed unit neighborhood as the union of the family, its lower shadow, and its upper shadow. In the Boolean cube the closed Hamming ball of radius 1 of a family A is exactly A ∪ ∂A ∪ ∂⁺A: a vertex at Hamming distance ≤ 1 of some u ∈ A is either u itself, a one-element subset (lower shadow ∂A), or a one-element superset (upper shadow ∂⁺A). This is the structural dictionary bridging the project's metric neighborhood 1 to mathlib's Finset.shadow / Finset.upShadow, so the closed-neighborhood leaf below can be analysed with the standard set-family shadow operators (and the already-proved UV shadow bounds). Sorry-free.

theorem BooleanIsoperimetry.card_eq_sum_card_filter_layer {N : ℕ} (A : Finset (Cube N)) : A.card = ∑ k ∈ Finset.range (N + 1), {x ∈ A | Finset.card x = k}.card

theorem BooleanIsoperimetry.shadow_filter_layer_eq {N : ℕ} (A : Finset (Cube N)) (k : ℕ) : {x ∈ A.shadow | x.card = k} = {x ∈ {x ∈ A | x.card = k + 1}.shadow | x.card = k}

Lower-shadow membership in a fixed output layer only depends on the next input layer. This is the local Hamming-window dictionary used by the layer-by-layer closed-neighborhood argument.

theorem BooleanIsoperimetry.upShadow_filter_layer_eq {N : ℕ} (A : Finset (Cube N)) (k : ℕ) : {x ∈ A.upShadow | x.card = k} = {x ∈ {x ∈ A | x.card = k - 1}.upShadow | x.card = k}

Upper-shadow membership in a fixed output layer only depends on the previous input layer. The k = 0 case is empty on the upper-shadow side, and the Nat.pred formulation keeps the window statement total.

theorem BooleanIsoperimetry.neighborhood_one_filter_layer_eq_self_shadow_upShadow {N : ℕ} (A : Finset (Cube N)) (k : ℕ) : {x ∈ neighborhood 1 A | Finset.card x = k} = {x ∈ A | Finset.card x = k} ∪ {x ∈ {x ∈ A | x.card = k + 1}.shadow | Finset.card x = k} ∪ {x ∈ {x ∈ A | x.card = k - 1}.upShadow | Finset.card x = k}

theorem BooleanIsoperimetry.familyUp_subset_familyUp {N : ℕ} {U V : Cube N} (hd : Disjoint U V) {A B : Finset (Cube N)} (hsub : A ⊆ B) : familyUp U V A ⊆ familyUp U V B

theorem BooleanIsoperimetry.familyUp_shadow_subset {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hUV : IsUVAdmissibleForFamily A U V) : (familyUp U V A).shadow ⊆ familyUp U V A.shadow

theorem BooleanIsoperimetry.familyUp_upShadow_subset {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hUV' : IsUVAdmissibleForFamily A.compls V U) : (familyUp U V A).upShadow ⊆ familyUp U V A.upShadow

theorem BooleanIsoperimetry.neighborhood_one_subset_familyUp_neighborhood_of_admissible {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hadm : IsUVAdmissibleForFamily A U V) (hadm' : IsUVAdmissibleForFamily A.compls V U) : neighborhood 1 (familyUp U V A) ⊆ familyUp U V (neighborhood 1 A)

Closed unit-neighborhood compression inclusion. If a block move is doubly admissible for A, the neighborhood of the compressed family is a subset of the compression of the neighborhood. This avoids layer-by-layer bounds which are false when |V| < |U|, instead providing a global inclusion that preserves cardinality.

theorem BooleanIsoperimetry.neighborhood_one_card_le_for_admissible_block {N : ℕ} {A : Finset (Cube N)} {U V : Cube N} (hd : Disjoint U V) (hadm : IsUVAdmissibleForFamily A U V) (hadm' : IsUVAdmissibleForFamily A.compls V U) : (neighborhood 1 (familyUp U V A)).card ≤ (neighborhood 1 A).card

Closed unit-neighborhood nonincrease for a doubly-admissible block move. This is the genuine Frankl–Füredi boundary-monotonicity leaf: an admissible disjoint block 𝒰-move that is admissible in both directions (primal IsUVAdmissibleForFamily A U V, controlling the lower shadow, and dual IsUVAdmissibleForFamily (Aᶜˢ) V U, controlling the upper shadow) does not increase the closed unit neighborhood neighborhood 1 A.

It is proved via the global inclusion neighborhood_one_subset_familyUp_neighborhood_of_admissible, avoiding false layer-by-layer bounds for moves where |V| < |U|.

theorem BooleanIsoperimetry.paperColexBlockMove_card {N : ℕ} {A A' : Finset (Cube N)} {i j : Fin N} (h : IsPaperColexBlockMove A A' i j) : A'.card = A.card

theorem BooleanIsoperimetry.paperColexBlockMove_neighborhood_card_le {N : ℕ} {A A' : Finset (Cube N)} {i j : Fin N} (h : IsPaperColexBlockMove A A' i j) : (neighborhood 1 A').card ≤ (neighborhood 1 A).card

theorem BooleanIsoperimetry.paperColexBlockMove_potential_lt {N : ℕ} {A A' : Finset (Cube N)} {i j : Fin N} (h : IsPaperColexBlockMove A A' i j) : compressionPotential A' < compressionPotential A

theorem BooleanIsoperimetry.paperColexBlockMove_isResidualShift {N : ℕ} {A A' : Finset (Cube N)} {i j : Fin N} (h : IsPaperColexBlockMove A A' i j) (_hdown : IsCoordinateDownFixed A) (_hlower : IsLowerLevelSaturated A) : IsDownFixedResidualShift A A'

theorem BooleanIsoperimetry.paperColexShiftMove_card {N : ℕ} {A A' : Finset (Cube N)} (h : IsPaperColexShiftMove A A') : A'.card = A.card

theorem BooleanIsoperimetry.paperColexShiftMove_potential_lt {N : ℕ} {A A' : Finset (Cube N)} (h : IsPaperColexShiftMove A A') : compressionPotential A' < compressionPotential A

Rank-potential strict descent for a pure within-layer colex move. This is a genuine dictionary consequence of the move (swap_potential_lt for a single colex swap, paperColexBlockMove_potential_lt for a block move) — no boundary or KK input.

theorem BooleanIsoperimetry.paperColexShiftMove_isResidualShift {N : ℕ} {A A' : Finset (Cube N)} (h : IsPaperColexShiftMove A A') (hnbhd : (neighborhood 1 A').card ≤ (neighborhood 1 A).card) : IsDownFixedResidualShift A A'

Assemble the descent target from a pure within-layer colex move and the separately supplied boundary non-increase hnbhd. The boundary bound is genuine selection data (from the KK existence leaf), not a projection off the move predicate: paperColexShiftMove_neighborhood_card_le no longer exists because it is false for arbitrary colex shifts (see the IsPaperColexShiftMove docstring).

theorem BooleanIsoperimetry.paperLevelBlockMove_card {N : ℕ} {A A' : Finset (Cube N)} {U V : Cube N} (h : IsPaperLevelBlockMove A A' U V) : A'.card = A.card

theorem BooleanIsoperimetry.paperLevelBlockMove_neighborhood_card_le {N : ℕ} {A A' : Finset (Cube N)} {U V : Cube N} (h : IsPaperLevelBlockMove A A' U V) : (neighborhood 1 A').card ≤ (neighborhood 1 A).card

theorem BooleanIsoperimetry.paperLevelBlockMove_potential_lt {N : ℕ} {A A' : Finset (Cube N)} {U V : Cube N} (h : IsPaperLevelBlockMove A A' U V) : compressionPotential A' < compressionPotential A

theorem BooleanIsoperimetry.paperResidualStep_isResidualShift {N : ℕ} {A A' : Finset (Cube N)} (h : IsPaperResidualStep A A') : IsDownFixedResidualShift A A'

theorem BooleanIsoperimetry.paperResidualSequence_isResidualShift {N : ℕ} {A A' : Finset (Cube N)} (h : IsPaperResidualSequence A A') : IsDownFixedResidualShift A A'

theorem BooleanIsoperimetry.downFixed_erase_mem {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) {x : Cube N} (hx : x ∈ A) {i : Fin N} (hi : i ∈ x) : Finset.erase x i ∈ A

A coordinate-Down-fixed family is closed under deleting any present coordinate: if x ∈ A and i ∈ x then x.erase i ∈ A. This is the forward direction of the IsCoordinateDown i A A fixed-point characterization.

theorem BooleanIsoperimetry.downFixed_sdiff_mem {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) {S W : Cube N} (hS : S ∈ A) (hWS : W ⊆ S) : S \ W ∈ A

Iterating downFixed_erase_mem: a coordinate-Down-fixed family is closed under removing any sub-block W ⊆ S.

theorem BooleanIsoperimetry.downFixed_familyUp_erase_eq {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) (W : Cube N) : familyUp W ∅ A = A

The familyUp W ∅ move is trivial on a coordinate-Down-fixed family: removing a block from any of its sets stays inside the (down-closed) family, so no set is actually moved. This is one of the two admissibility ingredients of a paper level block move whose V is a single coordinate.

theorem BooleanIsoperimetry.downFixed_familyUp_add_compls_eq {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) (W : Cube N) : familyUp ∅ W A.compls = A.compls

Dual admissibility ingredient: familyUp ∅ W is trivial on the complemented family Aᶜˢ of a coordinate-Down-fixed A. Follows from downFixed_familyUp_erase_eq through the complement dictionary familyUp_compls.

theorem BooleanIsoperimetry.downFixed_downClosed {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) {R S : Cube N} (hS : S ∈ A) (hRS : R ⊆ S) : R ∈ A

Existence of a paper level block from lower-level-saturation failure.

For a coordinate-Down-fixed family A that is not lower-level-saturated, there is a present block U ∈ A with 2 ≤ U.card and a coordinate j ∉ U such that the single-coordinate level move familyUp U {j} A is nontrivial: some S ∈ A containing U and avoiding j has its block replacement (S \ U) ∪ {j} outside A.

This is the genuine combinatorial core (a strictly smaller terminalization lemma): the admissibility of the resulting move is automatic from down-fixedness (downFixed_familyUp_erase_eq, downFixed_familyUp_add_compls_eq), so only this pure existence statement remains. It is finite-checked NO_COUNTEREXAMPLE for N ≤ 4 by verify_paperBlock_existence_small.py (clean-form column).

theorem BooleanIsoperimetry.not_lowerLevelSaturated_exists_witness {N : ℕ} {A : Finset (Cube N)} (h : ¬IsLowerLevelSaturated A) : ∃ (T : Cube N) (S : Cube N), T ∉ A ∧ S ∈ A ∧ Finset.card T < Finset.card S

Direct witness form of lower-level-saturation failure.

theorem BooleanIsoperimetry.blockReplace_sdiff_sdiff_eq_right {N : ℕ} (S T : Cube N) : blockReplace (S \ T) (T \ S) S = T

The block replacement associated to an absent lower vertex T and a present larger vertex S: remove S \ T and insert T \ S.

theorem BooleanIsoperimetry.sdiff_card_lt_sdiff_card_of_card_lt {N : ℕ} {S T : Cube N} (hcard : Finset.card T < Finset.card S) : Finset.card (T \ S) < Finset.card (S \ T)

Cardinality comparison for the block replacement associated to T.card < S.card: the inserted block T \ S is strictly smaller than the removed block S \ T.

theorem BooleanIsoperimetry.not_lowerSat_exists_minimalAbsent_maxPresent {N : ℕ} {A : Finset (Cube N)} (h : ¬IsLowerLevelSaturated A) : ∃ (T : Cube N) (S : Cube N), T ∉ A ∧ (∀ R ⊂ T, R ∈ A) ∧ S ∈ A ∧ (∀ R ∈ A, Finset.card R ≤ Finset.card S) ∧ Finset.card T < Finset.card S

Extremal witness selection for lower-saturation failure (proved).

If A is not lower-level-saturated, there is a ⊆-minimal absent block T (every proper subset of T lies in A) together with a maximum-cardinality present block S, and T.card < S.card. This is the honest, dimension-free selection half of the Frankl–Füredi level-terminalization step; it needs only failure of saturation, not down-fixedness.

It does not by itself give an admissible block: the finite checker verify_nearMiss_false_small.py shows (claim UA, N = 5) that not every such extremal pair is jointly admissible, so the eventual proof of downFixed_not_lowerSat_exists_admissibleBlock must still select which extremal pair works. But every candidate produced here is a genuine minimal-absent / max-present witness, exactly the objects the paper move ranges over.

theorem BooleanIsoperimetry.not_lowerSat_exists_minDelta_pair {N : ℕ} {A : Finset (Cube N)} (h : ¬IsLowerLevelSaturated A) : ∃ (T : Cube N) (S : Cube N), T ∉ A ∧ S ∈ A ∧ Finset.card T < Finset.card S ∧ ∀ (T' S' : Cube N), T' ∉ A → S' ∈ A → Finset.card T' < Finset.card S' → Finset.card (S \ T) + Finset.card (T \ S) ≤ Finset.card (S' \ T') + Finset.card (T' \ S')

Minimal-symmetric-difference extremal witness selection (proved).

Refines not_lowerSat_exists_minimalAbsent_maxPresent by additionally selecting, among all minimal-absent / maximum-present witness pairs (T, S) with T.card < S.card, one that minimizes the Hamming symmetric difference |S \ T| + |T \ S| = |S △ T|. This is the exact selection criterion that the finite checker test_min_delta_extremal.py confirms (exhaustive N = 4) yields a jointly admissible Frankl–Füredi level block move U = S \ T, V = T \ S: among the extremal frontier the pair whose blocks are as small as possible is the one whose primal/dual erase-admissibility clauses hold.

Only the selection is proved here (sorry-free, pure finite minimization over the nonempty frontier of extremal pairs); the admissibility consequence for the selected pair is the remaining research content of downFixed_not_lowerSat_exists_admissibleBlock. This upgrades the previously external min-|S △ T| finite evidence to an in-Lean theorem, giving the exact selected objects the paper move ranges over.

theorem BooleanIsoperimetry.familyUp_eq_self_iff {N : ℕ} (W₁ W₂ : Cube N) (A : Finset (Cube N)) : familyUp W₁ W₂ A = A ↔ ∀ R ∈ A, W₁ ⊆ R → Disjoint W₂ R → blockReplace W₁ W₂ R ∈ A

Characterization of a trivial 𝒰-move (Mathlib dictionary lemma).

The family 𝒰-move familyUp W₁ W₂ A fixes A setwise exactly when no set of A is actually moved: for every R ∈ A with W₁ ⊆ R and W₂ disjoint from R, the block replacement blockReplace W₁ W₂ R = (R \ W₁) ∪ W₂ already lies in A. This is a pure image/injectivity dictionary fact about familyUp = A.image (familyUpMap …) and the definitional guard of familyUpMap; it carries no combinatorial content and is reused by both directional admissibility leaves.

theorem BooleanIsoperimetry.minDelta_pair_admissible_primal {N : ℕ} {A : Finset (Cube N)} {T S : Cube N} : IsCoordinateDownFixed A → T ∉ A → S ∈ A → ∀ (hcard : Finset.card T < Finset.card S) (hmin : ∀ (T' S' : Cube N), T' ∉ A → S' ∈ A → Finset.card T' < Finset.card S' → Finset.card (S \ T) + Finset.card (T \ S) ≤ Finset.card (S' \ T') + Finset.card (T' \ S')), ∀ x ∈ T \ S, ∃ y ∈ S \ T, familyUp (Finset.erase (S \ T) y) (Finset.erase (T \ S) x) A = A

Primal directional leaf. The lower-shadow (primal) erase-admissibility clause for the minimal-symmetric-difference extremal pair. For each x in the inserted block T \ S some coordinate y of the removed block S \ T can be spared so that the trimmed level-block move familyUp ((S\T).erase y) ((T\S).erase x) A fixes A setwise. Proved (or to be proved) via the trivial-move characterization familyUp_eq_self_iff and a contradiction against the symmetric-difference minimality hmin.

theorem BooleanIsoperimetry.minDelta_pair_admissible_dual_A {N : ℕ} {A : Finset (Cube N)} {T S : Cube N} (hdown : IsCoordinateDownFixed A) (hT : T ∉ A) (hS : S ∈ A) (hcard : Finset.card T < Finset.card S) (hmin : ∀ (T' S' : Cube N), T' ∉ A → S' ∈ A → Finset.card T' < Finset.card S' → Finset.card (S \ T) + Finset.card (T \ S) ≤ Finset.card (S' \ T') + Finset.card (T' \ S')) (x : Fin N) : x ∈ S \ T → ∃ y ∈ T \ S, familyUp (Finset.erase (S \ T) x) (Finset.erase (T \ S) y) A = A

theorem BooleanIsoperimetry.minDelta_pair_admissible_dual {N : ℕ} {A : Finset (Cube N)} {T S : Cube N} (hdown : IsCoordinateDownFixed A) (hT : T ∉ A) (hS : S ∈ A) (hcard : Finset.card T < Finset.card S) (hmin : ∀ (T' S' : Cube N), T' ∉ A → S' ∈ A → Finset.card T' < Finset.card S' → Finset.card (S \ T) + Finset.card (T \ S) ≤ Finset.card (S' \ T') + Finset.card (T' \ S')) (x : Fin N) : x ∈ S \ T → ∃ y ∈ T \ S, familyUp (Finset.erase (T \ S) y) (Finset.erase (S \ T) x) A.compls = A.compls

theorem BooleanIsoperimetry.minDelta_pair_admissible {N : ℕ} {A : Finset (Cube N)} {T S : Cube N} (hdown : IsCoordinateDownFixed A) (hT : T ∉ A) (hS : S ∈ A) (hcard : Finset.card T < Finset.card S) (hmin : ∀ (T' S' : Cube N), T' ∉ A → S' ∈ A → Finset.card T' < Finset.card S' → Finset.card (S \ T) + Finset.card (T \ S) ≤ Finset.card (S' \ T') + Finset.card (T' \ S')) : (∀ x ∈ T \ S, ∃ y ∈ S \ T, familyUp (Finset.erase (S \ T) y) (Finset.erase (T \ S) x) A = A) ∧ ∀ x ∈ S \ T, ∃ y ∈ T \ S, familyUp (Finset.erase (T \ S) y) (Finset.erase (S \ T) x) A.compls = A.compls

theorem BooleanIsoperimetry.downFixed_not_lowerSat_exists_admissibleBlock {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) (h : ¬IsLowerLevelSaturated A) : ∃ (T : Cube N) (S : Cube N), T ∉ A ∧ S ∈ A ∧ Finset.card T < Finset.card S ∧ (∀ x ∈ T \ S, ∃ y ∈ S \ T, familyUp (Finset.erase (S \ T) y) (Finset.erase (T \ S) x) A = A) ∧ ∀ x ∈ S \ T, ∃ y ∈ T \ S, familyUp (Finset.erase (T \ S) y) (Finset.erase (S \ T) x) A.compls = A.compls

theorem BooleanIsoperimetry.downFixed_not_lowerSat_exists_levelBlock {N : ℕ} {A : Finset (Cube N)} (hdown : IsCoordinateDownFixed A) (h : ¬IsLowerLevelSaturated A) : ∃ (U : Cube N) (V : Cube N), IsPaperLevelBlockMove A (familyUp U V A) U V

Terminalization core for lower-level-saturation failure.

The previous singleton "near-miss" formulation was too strong: a down-closed family can fail lower-level saturation because of an absent block T that differs from every larger present block in several new coordinates. The PDF-faithful move is the full block replacement U = S \ T, V = T \ S, with V.card < U.card.

This leaf is the remaining local terminalization content: from a coordinate Down-fixed, non-lower-saturated family, select an admissible Frankl-Furedi level block move. It is intentionally a pure move statement; boundary monotonicity is still proved from IsPaperLevelBlockMove, not bundled into the predicate.

theorem BooleanIsoperimetry.not_lowerLevelSaturated_exists_paperLevelBlock {N : ℕ} (A : Finset (Cube N)) (hdown : IsCoordinateDownFixed A) (h : ¬IsLowerLevelSaturated A) : ∃ (A' : Finset (Cube N)) (U : Cube N) (V : Cube N), IsPaperLevelBlockMove A A' U V

theorem BooleanIsoperimetry.neighborhood_card_le_of_layers_upperShadow_le {N r : ℕ} {A A' : Finset (Cube N)} (hr : 1 ≤ r) (hA_le : ∀ w ∈ A, Finset.card w ≤ r) (hA'_le : ∀ w ∈ A', Finset.card w ≤ r) (hA_full : ∀ (z : Cube N), Finset.card z < r → z ∈ A) (hA'_full : ∀ (z : Cube N), Finset.card z < r → z ∈ A') (h_shadow : (upperLayerShadow N r A').card ≤ (upperLayerShadow N r A).card) : (neighborhood 1 A').card ≤ (neighborhood 1 A).card

General layer-localized neighborhood monotonicity. If A and A' are both concentrated in layers ≤ r and both contain every set of card < r, then comparing their unit neighborhoods reduces to comparing their layer-(r+1) upper shadows. (This is the swap-free generalization of the body of the old neighborhood_card_le_of_upperLayerShadow_le_of_colexShift.)

theorem BooleanIsoperimetry.upperLayerShadow_eq_filter_layer {N r : ℕ} (B : Finset (Cube N)) : upperLayerShadow N r B = upperLayerShadow N r ({z ∈ B | Finset.card z = r})

Slice-reduction dictionary lemma. The upper layer shadow at layer r depends only on the card-r slice of the family, because a card-(r+1) set lies in upShadow B iff it contains some card-r member of B. This is a direct specialization of upShadow_filter_layer_eq at k = r + 1.

theorem BooleanIsoperimetry.simplicialInitSeg_zero {N : ℕ} : simplicialInitSeg N 0 = ∅

simplicialInitSeg N 0 = ∅.

theorem BooleanIsoperimetry.rank_empty {N : ℕ} : rank ∅ = 0

rank (∅) = 0.

theorem BooleanIsoperimetry.simplicialInitSeg_one {N : ℕ} : simplicialInitSeg N 1 = {∅}

simplicialInitSeg N 1 = {∅}.

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

Lower-saturated KK-jump. For a lower-level-saturated family A, the simplicial initial segment of size A.card has unit neighborhood no larger than A's. Proof: A is a full ball below its top layer r plus a card-r slice L; the initial segment shares that ball and carries the colex-initial r-slice layerInitSeg N r |L|, whose upper shadow is minimal by the Kruskal–Katona theorem upperLayerShadow_min. neighborhood_card_le_of_layers_upperShadow_le then transfers the layer bound to the full neighborhood.

theorem BooleanIsoperimetry.simplicialInitSeg_isFullyCompressed {N m : ℕ} : IsFullyCompressed (simplicialInitSeg N m)

The simplicial initial segment is fully compressed (lower-level saturated and colex-shift fixed): it is a rank-downward-closed set, so no colex shift or level fill can apply.

theorem BooleanIsoperimetry.lowerSatDownFixed_descent_step {N : ℕ} (A : Finset (Cube N)) (h : ¬(IsCoordinateDownFixed A ∧ IsLowerLevelSaturated A)) : ∃ (A' : Finset (Cube N)), A'.card = A.card ∧ (neighborhood 1 A').card ≤ (neighborhood 1 A).card ∧ compressionPotential A' < compressionPotential A

Reduction step to a lower-saturated, down-fixed family (no colex shift). If A is not yet both coordinate-Down-fixed and lower-level saturated, one coordinate Down-compression or one level-block fill gives a family of the same size, no larger neighborhood, and strictly smaller potential. Both moves are sorry-free; no within-layer colex swap is used.

theorem BooleanIsoperimetry.exists_lowerSatDownFixed_le_aux {N : ℕ} (n : ℕ) (A : Finset (Cube N)) : compressionPotential A = n → ∃ (A₁ : Finset (Cube N)), IsCoordinateDownFixed A₁ ∧ IsLowerLevelSaturated A₁ ∧ A₁.card = A.card ∧ (neighborhood 1 A₁).card ≤ (neighborhood 1 A).card

Well-founded descent (strong induction on potential) to a lower-saturated, Down-fixed family, using only coordinate-Down and level-block moves.

theorem BooleanIsoperimetry.exists_fullyCompressed_le {N : ℕ} (A : Finset (Cube N)) : ∃ (C : Finset (Cube N)), IsFullyCompressed C ∧ C.card = A.card ∧ (neighborhood 1 C).card ≤ (neighborhood 1 A).card

Every family compresses to a fully-compressed family of the same size whose unit neighborhood is no larger — now via the honest Kruskal–Katona jump. Reduce A to a lower-saturated, Down-fixed A₁ (coordinate-Down + level-block moves, sorry-free), then replace A₁ by the simplicial initial segment of its size; the neighborhood does not increase by simplicialInitSeg_neighborhood_le_of_lowerSaturated (whose crux is the mathlib theorem Finset.kruskal_katona via upperLayerShadow_min).

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

Single-family vertex isoperimetry (dimension N), via compression. The simplicial initial segment of size A.card has the smallest unit neighborhood among all families of that size. This is H N A.card ≤ |N A| in unfolded form.

It is proved here independently of the scalar Macaulay route: by compressing A to a fully-compressed family C (exists_fullyCompressed_le, boundary non-increasing), which by fullyCompressed_eq_initSeg is the simplicial initial segment of size C.card = A.card. It does NOT use harper_compression_descent or harper_macaulay_min (both downstream of this file). The compression bottoms out at the honest Kruskal–Katona jump: exists_fullyCompressed_le reduces A to a lower-saturated, Down-fixed family (coordinate-Down + level-block moves) and then replaces its top slice by the colex-initial segment, whose upper shadow is minimal by mathlib's Finset.kruskal_katona (upperLayerShadow_min). This replaced the earlier single-swap colex descent, whose selection leaf (exists_colex_swap_upperLayerShadow_le_of_layerUpShifted) was false — up-shifted-but-not-colex-initial layers are stuck under single swaps (verify_colex_singlelayer_false_small.py), so the Kruskal–Katona jump to the whole initial segment is essential.

theorem BooleanIsoperimetry.compress_to_simplicial_pair {N : ℕ} (A B : Finset (Cube N)) : PairShadowCost N (simplicialInitSeg N A.card) (simplicialInitSeg N B.card) ≤ PairShadowCost N A B

Phase 1 — within-slice compression to simplicial slices (the paper's "compress each family to a Hamming sphere of its own size").

For arbitrary slices (A, B), replacing each by the simplicial initial segment of its own cardinality does not increase the two-slice boundary cost. Individual cardinalities are preserved (card (simplicialInitSeg N A.card) = A.card), so this is a within-slice move and the second arguments of the two max's are unchanged; the inequality then follows term-by-term from single-family vertex isoperimetry simplicialInitSeg_neighborhood_card_min applied to each slice.

This is now sorry-free: it is a direct consequence of the single-family compression result simplicialInitSeg_neighborhood_card_min, which in turn rests on the Kruskal–Katona jump exists_fullyCompressed_le (via upperLayerShadow_min = mathlib Finset.kruskal_katona).

theorem BooleanIsoperimetry.H_exchange_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

Degenerate (q = 0) regime of the cross-slice exchange — proved by pure cascade arithmetic, no Kruskal–Katona needed. When the canonical cascade split of a + b puts the whole mass in one slice (q = 0, hence p = a + b), the canonical cross-boundary cost H N p + p is already at most the arbitrary-split functional. The cascade arithmetic lives upstream in Macaulay.harper_bc_min_q_zero_core (it depends only on Cube/Cascade/Macaulay); this restatement discharges the degenerate regime of the Phase-2 leaf below.

theorem BooleanIsoperimetry.PairShadowCost_initSeg_eq_layerWindowCost {N a b : ℕ} (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : PairShadowCost N (simplicialInitSeg N a) (simplicialInitSeg N b) = initSegPairLayerWindowCost N a b

Phase-2 layer-window bridge (now sorry-free). On simplicial initial segments the geometric two-slice cost PairShadowCost is exactly the explicit layer-window cost initSegPairLayerWindowCost from LayerWindows.lean.

This is pure proof engineering, not Kruskal–Katona: on initial segments PairShadowCost collapses to max (H N a) b + max (H N b) a (PairShadowCost_initSeg_eq_max_H), and each boundary term H N · is by neighborhoodLayerCost_eq_H the finite sum over Hamming layers of the neighborhood's per-layer window counts. Filling the bridge removes the previous "definition still missing" hole: initSegPairLayerWindowCost is now a real layer-window sum, and the only remaining Phase-2 obligation is the genuine cross-slice Kruskal–Katona minimization cascade_layerWindowCost_min below.

structure BooleanIsoperimetry.CascadeLayerData (N r p q : ℕ) : Type

The genuine residual Phase-2 Kruskal–Katona/Macaulay leaf.

For a positive canonical cascade split (p, q) (with q ≥ 1) of a + b, the canonical cascade pair has no larger layer-window cost than the arbitrary sphere pair of sizes (a, b). Both sides are now genuine layer-window sums (initSegPairLayerWindowCost, defined in LayerWindows.lean), so this is the honest cross-slice Macaulay/Kruskal–Katona shadow-sum minimization stated over explicit Hamming-layer windows.

This is the single remaining Phase-2 obligation. By neighborhoodLayerCost_eq_H it unfolds to the scalar exchange max (H N p) q + max (H N q) p ≤ max (H N a) b + max (H N b) a, but its intended proof goes through the per-layer windows layerCount N r (neighborhood 1 ·), discharging each Hamming layer with the upstream single-layer Kruskal–Katona minimum upperShadowVal_numeric_min / upperLayerShadow_min (KruskalKatona.lean) and summing across layers. The degenerate q = 0 companion is already discharged sorry-free by H_exchange_q_zero; this file does not route through any downstream Harper/Macaulay-minimality theorem. The blueprint records that single-layer KK plus pure cascade telescoping is insufficient on its own: the multi-layer Macaulay summation is the remaining content.

• pRem : ℕ

  The remainder of p after the binomial prefix through layer r - 1.

• qRem : ℕ

  The remainder of q after the binomial prefix through layer r - 2.

• hp : p = binomPrefix N r + self.pRem
• hq : q = binomPrefix N (r - 1) + self.qRem
• hrange : self.pRem ≤ N.choose r ∧ self.qRem ≤ N.choose (r - 1)

def BooleanIsoperimetry.CascadeLayerWindow (N r p q : ℕ) : Prop

The assertion that p and q lie in the corresponding adjacent cascade windows.

Equations

• BooleanIsoperimetry.CascadeLayerWindow N r p q = Nonempty (BooleanIsoperimetry.CascadeLayerData N r p q)

noncomputable def BooleanIsoperimetry.PairLayerWindowSlack (N r a b p q : ℕ) : ℤ

The signed slack between two pair-layer window costs.

Equations

• BooleanIsoperimetry.PairLayerWindowSlack N r a b p q = ↑(BooleanIsoperimetry.PairLayerWindowCost N r a b) - ↑(BooleanIsoperimetry.PairLayerWindowCost N r p q)

noncomputable def BooleanIsoperimetry.PairWindowSlackSum (N a b p q : ℕ) : ℤ

The total pair-window slack summed over all relevant layers.

Equations

• BooleanIsoperimetry.PairWindowSlackSum N a b p q = ∑ r ∈ Finset.range (N + 2), BooleanIsoperimetry.PairLayerWindowSlack N r a b p q

theorem BooleanIsoperimetry.PairLayerWindowCost_eq_maxInitSeg (N r a b : ℕ) : PairLayerWindowCost N r a b = layerWindowRemainder N r (max (H N a) b) + layerWindowRemainder N r (max (H N b) a)

Per-layer Macaulay closed form of the pair-window cost (sorry-free bridge).

The opaque double-max cost PairLayerWindowCost N r a b is, layer by layer, the sum of the layer-r counts of two nested simplicial initial segments simplicialInitSeg N (max (H N a) b) and simplicialInitSeg N (max (H N b) a).

The identification uses only two sorry-free dictionary facts already in LayerWindows.lean:

• layerWindowShadowCost_eq_remainder_H: the shadow window of a is the remainder window of the neighborhood size H N a (the unit neighborhood of an initial segment is again an initial segment); and
• max_layerWindow_eq_union_card: since simplicial initial segments are nested, the per-layer max of two remainder windows is the remainder window of the segment of the larger size.

This turns every cross-slice window into an honest Macaulay layer window of a single initial segment, so the cascade leaf below is a genuine Kruskal–Katona initial-segment comparison rather than a scalar H inequality (rule 3). It needs no capacity hypotheses.

theorem BooleanIsoperimetry.sum_Ico_PairLayerWindowCost_eq (N a b k : ℕ) (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : ∑ r ∈ Finset.Ico k (N + 2), PairLayerWindowCost N r a b = max (H N a) b - binomPrefix N k + (max (H N b) a - binomPrefix N k)

Suffix layer-window sum in closed form (sorry-free Macaulay bridge).

The upper-tail (Hamming layers ≥ k) sum of the per-layer pair-window cost is, exactly, the sum of the two truncated Macaulay neighborhood values max (H N a) b - binomPrefix N k and max (H N b) a - binomPrefix N k (truncated ℕ subtraction). This is the composition of the two proved dictionary facts PairLayerWindowCost_eq_maxInitSeg (each layer cost is a sum of two nested initial-segment layer counts) and suffix_layerWindowRemainder_eq (the suffix sum of an initial segment's layer counts is m - binomPrefix N k). It turns the opaque suffix window sum into an explicit truncated-neighborhood comparison over the Macaulay layer threshold binomPrefix N k.

theorem BooleanIsoperimetry.sum_Ico_layerWindowRemainder_max_eq (N x y k : ℕ) : ∑ r ∈ Finset.Ico k (N + 2), layerWindowRemainder N r (max (H N x) y) = {z ∈ neighborhood 1 (simplicialInitSeg N x) ∪ simplicialInitSeg N y | k ≤ Finset.card z}.card

Suffix layer-window sum as a Hamming upper-tail count of a neighborhood union.

The upper-tail (Hamming layers ≥ k) sum of the remainder windows of the value max (H N x) y is exactly the number of vertices of cardinality ≥ k in the union of the unit neighborhood of the initial segment of size x with the initial segment of size y. This is a sorry-free dictionary identity: the unit neighborhood of an initial segment is again an initial segment (neighborhood_initSeg_eq), initial segments are nested so their union is the initial segment of the larger size, and the suffix layer sum of an initial segment counts exactly its vertices of cardinality ≥ k (sum_Ico_layerCount_eq_filter_card_ge). It converts the opaque window sum into the genuine set-family Hamming upper-tail count on which the dimension recursion operates.

theorem BooleanIsoperimetry.slice0_union {N : ℕ} (A B : Finset (Cube (N + 1))) : slice0 (A ∪ B) = slice0 A ∪ slice0 B

The genuine Kruskal–Katona vertex-boundary upper-tail leaf (set-family form).

This is the honest Frankl–Füredi/Macaulay content of cascade_KK_tail_min, stated directly on Boolean-cube set families, Hamming layers, and unit neighborhoods — no ℤ, no window bookkeeping, no scalar H arithmetic. For a canonical cascade split (p, q) of a + b that Macaulay-interleaves the arbitrary split (a, b), the number of high-Hamming-layer (card ≥ k) vertices in the two cross-slice neighborhood unions of (p, q) is no larger than that of (a, b): |{z ∈ N(IS p) ∪ IS q : |z| ≥ k}| + |{z ∈ N(IS q) ∪ IS p : |z| ≥ k}| ≤ |{z ∈ N(IS a) ∪ IS b : |z| ≥ k}| + |{z ∈ N(IS b) ∪ IS a : |z| ≥ k}|, where IS m := simplicialInitSeg N m.

At k = 0 this is Harper's vertex-boundary recursion (neighborhood_succ gives |N(IS p) ∪ IS q| + |N(IS q) ∪ IS p| = H (N+1) (a+b)); for k ≥ 1 it is the same comparison restricted to the upper Hamming layers, the Macaulay grid tail. The faithful proof is the dimension recursion on N (H_succ_slice / neighborhood_succ): slicing at the top coordinate reduces the level-N upper-tail count with cutoff k to the level-(N-1) counts of the two slices with cutoffs k (slice 0) and k - 1 (slice 1), and the interleaving majorization is inherited by the slice sub-splits via CascadeInterleaves.lower_succ. This is the exact dimension recursion + single-layer KK route requested by the Frankl–Füredi PDF, not a scalar reduction.

theorem BooleanIsoperimetry.slice1_union {N : ℕ} (A B : Finset (Cube (N + 1))) : slice1 (A ∪ B) = slice1 A ∪ slice1 B

theorem BooleanIsoperimetry.slice0_simplicialInitSeg_eq_cascadeSplit {N x p q : ℕ} (h : CascadeSplit N x p q) : slice0 (simplicialInitSeg (N + 1) x) = simplicialInitSeg N p

theorem BooleanIsoperimetry.slice1_simplicialInitSeg_eq_cascadeSplit {N x p q : ℕ} (h : CascadeSplit N x p q) : slice1 (simplicialInitSeg (N + 1) x) = simplicialInitSeg N q

theorem BooleanIsoperimetry.cascade_upper_slice_subset_neighborhood_lower {N x p q : ℕ} (h : CascadeSplit N x p q) : simplicialInitSeg N q ⊆ neighborhood 1 (simplicialInitSeg N p)

theorem BooleanIsoperimetry.slice0_neighborhoodUnion {N x y px qx py qy : ℕ} (hx : CascadeSplit N x px qx) (hy : CascadeSplit N y py qy) : slice0 (neighborhood 1 (simplicialInitSeg (N + 1) x) ∪ simplicialInitSeg (N + 1) y) = neighborhood 1 (simplicialInitSeg N px) ∪ simplicialInitSeg N py

theorem BooleanIsoperimetry.slice1_neighborhoodUnion {N x y px qx py qy : ℕ} (hx : CascadeSplit N x px qx) (hy : CascadeSplit N y py qy) : slice1 (neighborhood 1 (simplicialInitSeg (N + 1) x) ∪ simplicialInitSeg (N + 1) y) = neighborhood 1 (simplicialInitSeg N qx) ∪ simplicialInitSeg N px ∪ simplicialInitSeg N qy

theorem BooleanIsoperimetry.card_filter_neighborhoodUnion_initSeg (N x y k : ℕ) (hy : y ≤ 2 ^ N) : {z ∈ neighborhood 1 (simplicialInitSeg N x) ∪ simplicialInitSeg N y | k ≤ Finset.card z}.card = max (H N x) y - binomPrefix N k

theorem BooleanIsoperimetry.card_filter_neighborhoodUnion_initSeg_three (N x y z k : ℕ) (h_le : H N x ≤ y) (hy : y ≤ 2 ^ N) (hz : z ≤ 2 ^ N) : {z ∈ neighborhood 1 (simplicialInitSeg N x) ∪ simplicialInitSeg N y ∪ simplicialInitSeg N z | k ≤ Finset.card z}.card = max y z - binomPrefix N k

theorem BooleanIsoperimetry.cascade_split_reaches_canonical {N : ℕ} (a b : ℕ) (ha : a ≤ 2 ^ N) (hb : b ≤ 2 ^ N) : ∃ (A' : Finset (Cube N)) (B' : Finset (Cube N)), IsCanonicalCascadePair A' B' ∧ A'.card + B'.card = a + b ∧ PairShadowCost N A' B' ≤ PairShadowCost N (simplicialInitSeg N a) (simplicialInitSeg N b)

Phase-3 cascade exchange (sorry-free).

A pair of simplicial initial segments (simplicialInitSeg N a, simplicialInitSeg N b) of total a + b can be compressed across the top coordinate to the canonical cascade pair (simplicialInitSeg N p, simplicialInitSeg N q) of the same total, without increasing the two-slice boundary cost.

The proof embeds both pairs into the (N + 1)-cube via embeddedPair, where the two-slice cost becomes a plain neighborhood size; the canonical pair embeds to the simplicial initial segment of size a + b (embeddedPair_eq_of_slice_eq), so the cost comparison is exactly the dimension-(N + 1) Harper minimality simplicialInitSeg_neighborhood_card_min.

The existence/total parts are immediate from the chosen canonical witnesses.

theorem BooleanIsoperimetry.pairedCompression_reaches_canonical {N : ℕ} (A B : Finset (Cube N)) : ∃ (A' : Finset (Cube N)) (B' : Finset (Cube N)), IsCanonicalCascadePair A' B' ∧ A'.card + B'.card = A.card + B.card ∧ PairShadowCost N A' B' ≤ PairShadowCost N A B

Frankl–Füredi terminalization theorem.

For any two slice families (A, B) there is the canonical cascade pair (A', B') of the same total volume |A| + |B| with two-slice boundary cost no larger than that of (A, B). This is the genuine set-family heart of the Frankl–Füredi proof of Harper's theorem, stated as an existence/termination statement so that the downstream scalar Macaulay leaves are corollaries of it rather than the root of the development.

It is now assembled (sorry-free at this level) from the two PDF phases:

• compress_to_simplicial_pair — compress the arbitrary slices to simplicial initial segments of their own sizes (dimension-N single-family Harper);
• cascade_split_reaches_canonical — compress the resulting sphere pair across the top coordinate to the canonical cascade split (Kruskal–Katona/Macaulay).

Everything Harper-facing (franklFuredi_pairedCompression_exchange, H_exchange_max_form_pos, H_shadow_LE_sum / H_shadow_GT_sum, the scalar leaves macaulay_extremal_pos_step_LE/GT, harper_macaulay_min, harper_compression_descent, harper_vertex_iso) is a sorry-free consequence of these two phases.

theorem BooleanIsoperimetry.franklFuredi_pairedCompression_exchange {N : ℕ} (A B : Finset (Cube N)) (p q : ℕ) (hpq : CascadeSplit N (A.card + B.card) p q) : PairShadowCost N (simplicialInitSeg N p) (simplicialInitSeg N q) ≤ PairShadowCost N A B

The Frankl-Füredi exchange theorem: arbitrary slices A, B can be paired-compressed into the canonical cascade split (p, q) of the total volume |A| + |B| without increasing the two-slice boundary cost.

This is now a sorry-free bridge from the set-family terminalization theorem pairedCompression_reaches_canonical: the reached canonical pair has the same total volume |A| + |B|, so by cascadeSplit_unique its two slices are exactly the canonical initial segments simplicialInitSeg N p, simplicialInitSeg N q of the cascade split (p, q), and the cost bound transfers verbatim. It no longer routes through harper_compression_descent, so the dependency direction is the genuine PDF one (paired compression ⟹ scalar Macaulay leaves).