Layer-window accounting for the cross-slice Kruskal–Katona bridge. #
This module provides the layer-window (Macaulay) decomposition of the unit
neighborhood of a simplicial initial segment, organized by Hamming layer. It is
the language in which the cross-slice exchange bridge
(PairShadowCost_initSeg_eq_layerWindowCost, Compression.lean) relates the
geometric two-slice cost to the single-layer Kruskal–Katona minimum
upperShadowVal_numeric_min (KruskalKatona.lean).
The key object is neighborhoodLayerCost N a: the size of the unit neighborhood
of simplicialInitSeg N a, written as an explicit finite sum over Hamming
layers of the per-layer counts layerCount N r (·). This sum is provably equal
to H N a (neighborhoodLayerCost_eq_H), so it is a faithful re-expression of
the boundary functional H that exposes the per-layer windows the
Kruskal–Katona core operates on — not an opaque scalar. The pair functional
initSegPairLayerWindowCost then assembles the two slice costs exactly the way
PairShadowCost does on simplicial initial segments.
The Hamming-layer-r part of a family: the sets of cardinality r in A.
Equations
- BooleanIsoperimetry.layerPart N r A = {x ∈ A | Finset.card x = r}
Instances For
The number of layer-r sets in A (the layer-r window count).
Equations
- BooleanIsoperimetry.layerCount N r A = (BooleanIsoperimetry.layerPart N r A).card
Instances For
Layers above the top Hamming level of the N-cube are empty.
Layer-window form of the boundary functional H.
The unit neighborhood of the simplicial initial segment of size a, counted as a
finite sum over Hamming layers r = 0, …, N+1 of its per-layer window counts.
Every layer summand layerCount N r (neighborhood 1 (simplicialInitSeg N a)) is
the number of boundary vertices in Hamming layer r; for an initial segment the
fully covered low layers contribute Nat.choose N r and the single partially
covered top layer contributes the genuine upper-shadow window. This is exactly
the Macaulay layer accounting, and it equals H N a (neighborhoodLayerCost_eq_H).
Equations
Instances For
The layer-window sum reconstructs the boundary functional H: summing the
per-layer window counts of the neighborhood over all Hamming layers recovers its
cardinality H N a. (Every vertex of the N-cube has cardinality ≤ N < N+2,
so the layers 0, …, N+1 partition the neighborhood.)
The per-layer window counts of the neighborhood are the layer counts of the
neighborhood-as-initial-segment simplicialInitSeg N (H N a). This makes the
windows manifestly the Macaulay/binomial windows that the Kruskal–Katona core
upperShadowVal_numeric_min minimizes layer by layer.
Layer-window pair cost. The two-slice Frankl–Füredi cost of the
simplicial initial segments of sizes a and b, written in layer-window terms:
each slice's boundary is the layer-window neighborhood cost
neighborhoodLayerCost, and the cross terms are the slice volumes, exactly as in
PairShadowCost. By neighborhoodLayerCost_eq_H this equals the scalar
max (H N a) b + max (H N b) a on initial segments, but it is defined through
the explicit per-layer windows so the cross-slice Kruskal–Katona minimization can
be carried out layer by layer.
Equations
Instances For
The number of layer-r sets in the initial segment of size a.
Equations
Instances For
The number of layer-r sets in the neighborhood of the initial segment of size a.
This exactly matches the Kruskal--Katona upper shadow (plus the elements of the set itself).
Equations
Instances For
The cross-slice layer window cost for a single Hamming layer r.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The remainder window is zero above the top Hamming layer.
The shadow-cost window is zero above the top Hamming layer.
The pair layer-window cost is zero above the top Hamming layer.
The per-layer window counts of any family A sum to its cardinality over the
Hamming layers 0, …, N+1 (every vertex of the N-cube has cardinality ≤ N).
This is the reusable fiberwise-partition identity already used inside
neighborhoodLayerCost_eq_H.
Per-layer max collapses to the global boundary value. Summing the
per-layer max of the shadow-cost window of a against the remainder window of
b over all Hamming layers recovers max (H N a) b, provided b ≤ 2^N.
The key structural fact is that both per-layer windows are layer counts of
nested simplicial initial segments: the shadow window of a is the layer count
of simplicialInitSeg N (H N a) (layerCount_neighborhood_initSeg), and the
remainder window of b is the layer count of simplicialInitSeg N b. Initial
segments are nested, so on each layer the two counts are comparable and their
max is the layer count of simplicialInitSeg N (max (H N a) b)
(max_layerWindow_eq_union_card). Summing over layers gives the cardinality
min (max (H N a) b) (2^N) = max (H N a) b, the last equality using b ≤ 2^N
and H N a ≤ 2^N. This is exactly the statement that the global max commutes
with the per-layer decomposition for nested initial-segment windows.
Kruskal–Katona identification of the layer windows #
These lemmas connect the layer-window objects above to the single-layer
Kruskal–Katona core (upperShadowVal_numeric_min / upperLayerShadow_min in
KruskalKatona.lean). They make the per-layer shadow windows manifestly the
KK upper-shadow windows, so the cross-slice leaf cascade_window_sum_min
(Compression.lean) routes through the genuine Kruskal–Katona minimum rather
than through opaque scalar H arithmetic.
The shadow-cost window of a in layer r is the remainder window of the
neighborhood size H N a in the same layer: the unit neighborhood of an initial
segment is again an initial segment (neighborhood_initSeg_eq), so its per-layer
counts are literally the per-layer counts of simplicialInitSeg N (H N a).
The layer-r part of a simplicial initial segment is r-uniform.
The layer-r window of an initial segment never exceeds the number of
r-subsets Nat.choose N r.
Thin Kruskal–Katona wrapper in layer-window language. For any r-uniform
family A with r ≥ 1, the numeric upper-shadow value at its own cardinality is
a lower bound for the size of its actual upper shadow in layer r+1. This is
exactly upperShadowVal_numeric_min specialized to t := A.card, packaged so
the cross-slice layer-window leaf can invoke single-layer KK directly: the
simplicial layer initial segment of the same size achieves this lower bound, so
no r-uniform family has a smaller layer-(r+1) upper shadow.
Layer-window decomposition of the pair cost. The
scalar two-slice cost initSegPairLayerWindowCost N a b is the sum over Hamming
layers of the per-layer pair window costs PairLayerWindowCost N r a b. This is
the bookkeeping bridge exposing the Macaulay/Kruskal–Katona layer windows that
the cross-slice leaf cascade_window_sum_min (Compression.lean) operates on
it requires a, b ≤ 2^N (otherwise the literal cross terms a/b exceed the
saturated initial-segment cardinality 2^N and the identity fails).
Suffix (upper-tail) closed form of the Macaulay layer windows #
The cascade suffix leaf compares upper-tail sums ∑_{r ≥ k} of the per-layer
remainder windows. The following two lemmas give a completely explicit closed
form for such a tail: it is the number of vertices of cardinality ≥ k in the
simplicial initial segment, and for a segment of size m ≤ 2^N this is exactly
the truncated difference m - binomPrefix N k. Both are Macaulay
dictionary facts (the simplicial order fills the lower Hamming layers first, so
the layer-< k part of simplicialInitSeg N m is simplicialInitSeg N (binomPrefix N k)
capped at m, via rank_lt_binomPrefix_iff).
Hardy–Littlewood–Pólya pair majorization for truncated (ℕ) tails.
For two ℕ-pairs, if the pair (a', b') weakly majorizes (a, b) — i.e. the
sums satisfy a + b ≤ a' + b' and the maxima satisfy max a b ≤ max a' b' —
then every truncated-tail pair sum is dominated:
(a - c) + (b - c) ≤ (a' - c) + (b' - c) for all thresholds c (ℕ truncated
subtraction). This is the two-point Hardy–Littlewood–Pólya / Karamata fact for
the increasing convex family x ↦ (x - c)⁺, specialised to a pair; it is the
final pair-combination step of any Macaulay upper-tail argument once the two
neighborhood-slice values have been compared.
Caveat (recorded so it is not misused). The two hypotheses are strictly
stronger than what the cascade tail leaf cascade_KK_tail_min actually needs:
that leaf only requires the truncated inequality at the Macaulay grid points
c = binomPrefix N k, and the max-slice hypothesis max a b ≤ max a' b' is
not available there — it is verified false on genuine cascade configurations
(smallest witness N = 3, a = b = 2, neighborhood slices (7,4) vs (6,6); see
verify_cascade_KK_tail_weakMaj_insufficient_small.py). Hence this lemma is a
sound but incomplete tool for that leaf: it closes the tail only in the
weak-majorized regime, and the genuine remaining content lives in the grid
structure of H, to be handled by the dimension recursion H_succ_cascade and
the single-layer minimum layerWindowShadowCost_KK_min.
Dimension recursion for the Hamming upper-tail count. #
The following lemma is the reusable slice-recursion brick requested for the
dimension induction of the cascade upper-tail leaf. It says the number of
vertices of Hamming weight ≥ k in a family A ⊆ Cube (N+1) splits, along the
top coordinate, into the weight-≥ k count of the lower slice slice0 A and the
weight-≥ k-1 count of the upper slice slice1 A (the upper slice already
carries the top coordinate, so its members have one extra active coordinate).
This is the tail-count analogue of slice_card_add.