Harper's vertex-isoperimetric theorem #
This file assembles the compression, Macaulay, Kruskal-Katona, and scalar recurrence layers into the final sorry-free proof of Harper's theorem.
The number of vertices whose gShift rank lies in the half-open interval
[lo, hi). This is the set-level form of an HIncrement window.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Exact vertex-weight form of a Macaulay shadow window. This is the same window
count as gShiftIntervalCount, but with each rank vertex weighted by its
explicit gShift-fibre size (macaulayShadowWeight).
The local non-circular boundary-cost functional used by the positive Macaulay
kernel. This intentionally duplicates the later boundaryCost definition so
the remaining inductive step can be expressed without referring to downstream
theorems.
Equations
- BooleanIsoperimetry.boundaryCostH N a b = max (BooleanIsoperimetry.H N a) b + max (BooleanIsoperimetry.H N b) a
Instances For
Exact slack decomposition of the max-form boundary cost. The two truncated
terms are precisely the slack that is needed in the GT regime, where the simpler
sum-form H N a + H N b is false.
The four-block prefix profile exposed by lowering a level-n+1
interleaving to the two level-n slices. The first pair (x0, y0) is read
one layer ahead of the second pair (x1, y1), matching the Pascal shift in
CascadeInterleaves.lower_succ.
Window additivity for the Macaulay shadow count gShiftIntervalCount:
adjacent rank windows [lo, mid) and [mid, hi) add to [lo, hi). A reusable
block-decomposition tool for splitting shadow windows along layer boundaries.
Whole-block value of the Macaulay shadow count between complete binomial
prefixes: the shadow window between binomPrefix n r and binomPrefix n s
counts exactly the complete Macaulay layers r+1, …, s. This connects the
set-level shadow count to the explicit Nat.choose layer sizes, which is the
form the layer-by-layer comparison of the two shadow windows needs.
Lower block bound (dual of gShiftIntervalCount_le_binomPrefix_window_of_endpoints).
If a shadow window [lo, hi) contains the complete binomial prefix block
[binomPrefix n r, binomPrefix n s) (that is, lo ≤ binomPrefix n r and
binomPrefix n s ≤ hi), then its shadow count is at least the complete-layer
block sum ∑_{i = r+1}^{s} C(n, i).
This is the missing companion of the existing upper bound: together they let a
Macaulay shadow comparison lower-bound the upper window and upper-bound the
lower window by explicit Nat.choose layer sums. It is the reusable
accounting helper named in Aristotle's Cycle 1 plan, and is the set-level form
of "a window that swallows whole layers counts at least those layers".
Block-domination ⇒ shadow-window domination.
Two shadow windows compared through their enclosing/enclosed complete binomial
blocks. If the lower window [lo₁, hi₁) is enclosed in the layer band
[r₁, s₁] (so it is upper-bounded by the block sum over r₁+1 .. s₁) and the
upper window [lo₂, hi₂) swallows the layer band [r₂, s₂] (so it is
lower-bounded by the block sum over r₂+1 .. s₂), and the first block sum is no
larger than the second, then the lower window's shadow count is no larger than
the upper window's.
This is the reusable whole-block comparison engine that the Frankl–Füredi /
Macaulay window comparison (harper_macaulay_LE_sum, harper_macaulay_GT_sum)
reduces to once the partial-layer boundary pieces of each window have been
absorbed into the enclosing layer band. It is ih-free and purely Nat.choose
arithmetic at the block level, isolating exactly the layer-index bookkeeping from
the set-level shadow content.
Single-layer shadow-window bound. A length-L shadow window contained in
a single Macaulay layer r has shadow count at most L * (n - r). This is the
set-level form of HIncrement_window_le_of_layer: it is the reusable upper bound
for the upper shadow window of the Frankl–Füredi/Macaulay comparison whenever
that window stays inside one cardinality band (which, computationally, is exactly
the regime of the reversed-orientation leaf harper_macaulay_reversed).
Endpoint arithmetic for the left-oriented equal-length Macaulay windows. If
the canonical split (p,q) and the arbitrary split (a,b) have the same total
and p ≤ a, then the lower endpoint also moves inward, b ≤ q, and the two
shadow windows [b,q) and [p,a) have the same length.
Endpoint arithmetic for the right-oriented equal-length Macaulay windows. If
a ≤ p, then q ≤ b, and the two shadow windows [a,p) and [q,b) have the
same length.
The GT regime gives the left-oriented window order together with equal lengths.
This is the arithmetic shape of the Frankl-Füredi slack comparison: the lower
window [b,q) and the upper window [p,a) have common length q-b = a-p.
The boundary cost is monotonically increasing with respect to cascade interleaving. This is the core mathematical reduction of the Macaulay window bounds.
Two-layer confinement (LE regime). If b lies at or below the top of
Macaulay layer r and a ≤ H N b, then a lies at or below the top of layer
r+1. Equivalently the LE-regime shadow comparison is confined to the two
adjacent Macaulay layers r and r+1. This is the reusable cascade-layer
increment fact behind the Case-I Kruskal–Katona/Macaulay window comparison.
Degenerate q = 0 branch of the Case-I Macaulay sum leaf. This removes
the non-positive canonical split from the Frankl–Füredi/Macaulay core: a
canonical split with q = 0 has total mass at most one, so the inequality is a
finite 0/1 calculation.
Frankl–Füredi lowered four-block exchange step (human-proof leaf).
The genuine local compression/Macaulay step in the form used by the Harper
induction: for the canonical cascade split (p,q) of a+b at level n+1,
in the ordered regime b ≤ a, with the four level-n cascade slice
decompositions of p,q,a,b and the lowered prefix-mass (Macaulay) domination
h_lower provided by CascadeInterleaves.lower_succ, and the level-n Harper
inequality ih, the canonical cross-boundary cost is minimal. This carries
exactly the PDF's inductive inputs (within-slice optimality from
ih/harper_extremal_n, and cross-layer prefix-mass majorization from
h_lower). The unordered case is recovered by harper_macaulay_exchange_step
via the symmetry of the right-hand side under swapping a, b.
Frankl–Füredi / Macaulay extremal step (max-form).
For the canonical cascade split (p,q) of a+b at level n+1, the canonical
cross-boundary cost is minimal. This is now a sorry-free consequence of the
single human-proof leaf boundaryCost_le_of_lower_interleaves_step_live: choose
the four level-n cascade slice decompositions of p,q,a,b via
exists_cascade_split, obtain the lowered prefix-mass domination from
canonicalSplit_interleaves and CascadeInterleaves.lower_succ, and apply the
leaf.
Positive-cascade Case-I (LE) sum leaf. Sorry-free corollary of
harper_macaulay_exchange_step: collapse the outer maxs
(canonical_boundaryCost_eq_H_add on the left; b ≤ a ≤ H b on the right).
Positive-cascade Case-II (GT) sum leaf. Sorry-free corollary of
harper_macaulay_exchange_step: the outer maxs collapse via
canonical_boundaryCost_eq_H_add (left) and the GT case H (n+1) b < a
(right, max (H (n+1) b) a = a).
Frankl-Füredi inductive boundary monotonicity for a cascade-interleaving profile.
This is the remaining local compression/Macaulay step in the form actually used
by the Harper induction: the arbitrary split has capacity bounds, and the proof
may use the already-established lower-dimensional Harper inequality. The older
capacity-free, ih-free version was stronger than the live proof route and hid
the PDF's inductive input.
Frankl–Füredi joint Macaulay kernel — the single unified leaf (LE ∪ GT).
For the canonical cascade split (p, q) of a + b at level n + 1 (so (p,q)
is the split of a + b in the (n+2)-cube, while the boundary values live in
the (n+1)-cube), in the ordered regime b ≤ a, the canonical boundary sum
H (n+1) p + H (n+1) q is bounded by the arbitrary-split boundary functional
H (n+1) a + max (H (n+1) b) a.
Frankl–Füredi Case I, joint-sum Macaulay kernel (the LE corollary).
Now a proved corollary of the unified kernel harper_macaulay_joint: in the
LE regime a ≤ H (n+1) b the boundary max (H (n+1) b) a collapses to
H (n+1) b (max_eq_left).
Frankl–Füredi Case II, GT joint slack kernel (the GT corollary).
Now a proved corollary of the unified kernel harper_macaulay_joint: in the
GT regime H (n+1) b < a the boundary max (H (n+1) b) a collapses to a
(max_eq_right).
This is the genuine joint slack bound; the previously-exposed split into
H (n+1) q ≤ a and H (n+1) p ≤ H (n+1) a is false (see the commented note
above), so the GT bound must keep H (n+1) p + H (n+1) q ≤ H (n+1) a + a intact.
GT Macaulay shadow slack comparison (PDF-faithful shadow-count form). Now a
proved corollary of the joint slack kernel harper_macaulay_slack_gt:
harper_gt_split_between supplies b ≤ q ≤ p ≤ a, the shadow windows rewrite to
H differences, and the goal follows by arithmetic (H_mono plus omega).
Frankl–Füredi Case I, canonical-sum core.
For the canonical cascade split (p, q) of a + b at dimension n + 1, in the
LE regime b ≤ a ≤ H (n+1) b, the canonical boundary sum H(n+1)p + H(n+1)q
is bounded by the arbitrary-split boundary sum H(n+1)a + H(n+1)b.
This is the genuine max-free Macaulay heart of the LE case. It is strictly
narrower than harper_step_total: it adds the ordering hypothesis b ≤ a and
the case hypothesis a ≤ H (n+1) b, fixes the canonical split, and has the two
outer maxs already collapsed. It mentions only H, CascadeSplit, and the
level-n induction hypothesis ih, and is non-circular.
NOTE (cycle37.aristotle). This replaces the previous leaf
harper_step_le_window_shift, which asserted the endpoint order a ≤ p together
with a gShiftIntervalCount window inequality. An exact computational model of
H via the cascade recursion shows a ≤ p is false in the LE regime (176
counterexamples for n ≤ 4, smallest n = 1, a = 4, b = 2 with (p,q)=(3,3)):
the canonical split can place less than a in its lower slice, so the windows
[a,p) and [q,b) are not nested as that lemma required. The sum form proved
here is true (0 counterexamples for n ≤ 6) and is the correct LE leaf.
Frankl–Füredi LE/GT decomposition of the Harper inductive step #
NOTE (cycle36.aristotle). A previous cycle exposed the kernel as a single
Int "profile shadow" leaf franklFuredi_profile_residual_nonneg, asserting
weightedNestedLayerCost n (binomLayerWeight n) p0 p1 q0 q1
- weightedNestedLayerCost n (binomLayerWeight n) a0 a1 b0 b1
≤ (boundaryCostH (n+1) a b : ℤ) - (pairedCascadeBoundary n p0 p1 q0 q1 : ℤ)
with binomLayerWeight n l = n + 1 - l. An exact computational model of H
via the cascade recursion shows this residual statement is false (187
counterexamples for n ≤ 3, the smallest being n = 0, a = 0, b = 2). The
reason is structural: the only antitone layer weights w for which
Σ w l · (massₚ l − mass_a l) is sandwiched in [0, B − P] over all profiles
are the constant weights — and for those the sum is identically 0 because
total layer mass is conserved. Hence no single per-layer Abel weight can
bridge the coarse layer gap to the boundary deficit; the linear weight
n + 1 − l over-counts. (The coarse direction
franklFuredi_profile_coarse_layer_gap_nonneg, i.e. Wₚ ≥ W_a, is genuinely
true and kept above as reusable Abel infrastructure, but it is not sufficient.)
The false leaf has therefore been removed and the kernel re-decomposed along the
standard Frankl–Füredi case split (which collapses the two outer maxs of
boundaryCostH): a max-free LE case (harper_step_le) and a max-free GT
case (harper_step_gt). Both statements are true (verified by the exact
cascade model for all b ≤ a with a, b ≤ 2^(n+1) and n ≤ 4) and strictly
narrower than harper_step_total, and harper_step_total is now a proved
consequence of them via boundaryCostH_eq_H_add_slack.
Frankl–Füredi Case I, sum form.
In the LE regime a ≤ H (n+1) b, the max-form boundary cost collapses to the
plain sum H (n+1) a + H (n+1) b. This lemma is now a proved reduction to
the canonical-sum core harper_step_le_canonical_sum: after choosing the
canonical split (p,q) of a+b and dispatching the degenerate q = 0 branch,
the positive branch rewrites H (n+2) (a+b) to H(n+1)p + H(n+1)q and applies
the core.
Frankl–Füredi Case II (the GT regime). Under b ≤ a and H (n+1) b < a,
the boundary cost boundaryCostH (n+1) a b collapses to H (n+1) a + a. This
is the max-free combinatorial heart of Harper's n → n+1 step in the GT regime.
It is strictly narrower than harper_step_total (adds b ≤ a and the case
hypothesis H (n+1) b < a, with the outer maxs eliminated), mentions only
H and ih, and is non-circular.
The b ≤ a branch of harper_step_total, assembled from the two max-free case
lemmas by collapsing the slack form of boundaryCostH
(boundaryCostH_eq_H_add_slack). Sorry-free.
The four-block Frankl-Furedi profile bridge, now a proved consequence of
the pure-H kernel harper_step_total. Using
pairedCascadeBoundary_pos_eq_H_succ, the four-block boundary on the left is
exactly H (n+2) (a+b), and the conclusion is then harper_step_total.
The four-block Macaulay/cascade interleaving comparison with explicit witnesses.
This exposes the nested canonical splits at level n for all components, reducing
the H (n+1) expressions to purely n-level max combinations.
The single remaining open step. The Harper/Macaulay extremal inequality at
level n + 1, derived from the same inequality at all lower levels (ih).
This is exactly harper_extremal_n shifted one dimension up (note the identical
shape: the conclusion is the cross boundary cost of the canonical cascade split
being minimal), so it is the genuine n → n+1 inductive step of Harper's
vertex-isoperimetric theorem, with nothing else attached.
Compared with the original _core lemmas, this statement is strictly narrower:
it has no case hypothesis, no ordering b ≤ a, no positivity 1 ≤ q, and none
of the eight level-n sub-component variables / their cascade splits / bounds.
It mentions only H, CascadeSplit, and ih, and is non-circular (it does not
refer to any later result such as harper_core, harper_bc_min,
macaulay_optimization, or H_inequality_core).
It has no elementary proof: H (n+1) is neither convex nor concave and the cross
boundary cost is not a unimodal function of the split, so the genuine
Kruskal–Katona / Macaulay cascade-interleaving argument is required.
Clean H (n+1)-level form of Case I of the n → n+1 inductive step. Given the
canonical cascade split (p, q) of a + b at level n+1, and that the larger
part a still fits inside the neighbourhood of the smaller part (a ≤ H (n+1) b),
the split boundary sum is no larger than H (n+1) a + H (n+1) b.
This is now a short consequence of harper_extremal_step (the unified extremal
step) together with canonical_boundaryCost_eq_H_add and the case hypotheses.
Clean H (n+1)-level form of Case II of the n → n+1 inductive step. Given the
canonical cascade split (p, q) of a + b at level n+1, and that the larger
part a exceeds the neighbourhood of the smaller part (H (n+1) b < a), the
split boundary sum is no larger than H (n+1) a + a.
This is now a short consequence of harper_extremal_step together with
canonical_boundaryCost_eq_H_add and the case hypotheses.
Clean subadditivity form of Case I of Harper's inductive step.
This is the genuine combinatorial content (non-circular: it mentions only H
and the lower-dimensional induction hypothesis ih). It says that when the
larger part a already fits inside the neighborhood of the smaller part
(a ≤ H n b), the closed neighborhood of the initial segment of size a + b
in the (n+1)-cube is no larger than H n a + H n b. Via H_succ_cascade and
canonical_boundaryCost_eq_H_add this is exactly harper_bc_min_case_le.
Clean form of Case II of Harper's inductive step.
Non-circular: mentions only H and the lower-dimensional ih. When the larger
part a exceeds the neighborhood of the smaller part (H n b < a), the closed
neighborhood of the size-(a+b) initial segment in the (n+1)-cube is no larger
than H n a + a. Via H_succ_cascade and canonical_boundaryCost_eq_H_add
this is exactly harper_bc_min_case_gt.
Harper's vertex-isoperimetric recursion inequality (the genuine combinatorial
core): the initial segment of size a + b in the (n+1)-cube has the smallest
closed 1-neighborhood among all sets obtained by taking initial segments of
sizes a, b in the two slices. Equivalently, in H-terms,
H (n+1) (a+b) ≤ max (H n a) b + max (H n b) a.
This is proved independently of boundaryCost, CascadeInterleaves,
H_inequality_core, H_inequality, macaulay_optimization, and
interleaving_boundaryCost_mono (all of which are stated later and ultimately
depend on this lemma), so there is no circularity.
The boundary cost of a split (a, b) in dimension n.
Equations
- BooleanIsoperimetry.boundaryCost n a b = max (BooleanIsoperimetry.H n a) b + max (BooleanIsoperimetry.H n b) a
Instances For
Macaulay interleaving theorem: if (p, q) interleaves (a, b), then its
boundary cost is smaller. Through the cascade recursion H_succ_cascade this
reduces to Harper's recursion inequality harper_core.
The Harper boundary inequality, stated directly on H:
H (n+1) (a+b) ≤ max (H n a) b + max (H n b) a.
Via H_succ_cascade this is equivalent to macaulay_optimization (the canonical
cascade split of a+b minimises the cross boundary expression), so it is the
genuine combinatorial heart of Harper's vertex-isoperimetric theorem for the
discrete cube.
The supporting structure for this statement is fully developed above:
H_succ_cascade— the slice recursionH (n+1) k = max (H n p) q + max (H n q) p;cascade_p_le_H_q— the compression propertyp ≤ H n qof the canonical split;cascade_q_le_p—q ≤ p;H_mono,H_ge_self,H_le_cube,H_add_self_mono— monotonicity / growth ofH;H_eq_gShift_count— the explicit boundary count formula.
The core Kruskal-Katona / Macaulay optimization inequality for the cascade split.
For any canonical split (p, q) of a + b, the cross-sum of their boundary sizes
is bounded by the sum of boundary bounds for the original sizes a and b.