Flag γ-vectors that are not f-vectors, total nonnegativity for Bose–Burton geometries, and Chow polynomials of projective deletions

Each of 121 computed Chow polynomials is palindromic and has the stated gamma-vector, which is nonnegative (gamma-positivity)

Each of the 121 gamma-vectors satisfies the Kruskal-Katona inequalities, i.e. is the f-vector of a simplicial complex

Each of the 121 Chow polynomials is real-rooted, with simple roots – instances of CFL Conjecture 1.1, which is open

Negative controls: the Kruskal-Katona check is tight on real data, strictly stronger than gamma-positivity, refuted independently by mathlib's Kruskal-Katona, and the source's own hypotheses are necessary

Search: no flag built matroid found whose gamma-vector violates Kruskal-Katona (CFL Question 8.7)

CFL Question 9.8 refuted: a flag, non-complete built matroid (U(7,8), 19-element building set) whose Chow gamma-vector (1,5,2,1) is not an f-vector; verified at ranks 7 through 11 by coloop padding

Correction: Kruskal-Katona is provably vacuous below rank 5, so the earlier scan (U(3,4), U(3,5), U(4,5)) could not bear on Question 9.8

The Question 9.8 counterexample is a rank-7 family with unbounded ground set: for four lines U(2,sᵢ), sᵢ ≥ 2, truncated to rank 7, the building set (atoms, lines, two opposite line-joins, all triple joins, E) of size n+11 is flag, non-complete, and has γ = (1,5,2,1), which is not an f-vector — twelve members, n = 8..12, eleven of them non-uniform

The k-block partition family on U(2k−1,2k): flag iff the complement of Γ is triangle-free (k ≥ 4), γ = (1, 3+m, m, 1) at k = 4 with Kruskal–Katona holding iff m = | Γ | ≥ 3, and slack exactly 0 at the minimum for k = 5, 6 — so k = 4 is the unique crossing point

Negative controls: blocks of rank ≥ 3 lose flagness and γ-positivity together (17 rows, none γ-positive); a Kruskal–Katona failure off the flag class (k = 3, γ = (1,1,1)) proves nothing; and the rank-7 truncation is what bites (rank 6 and rank 8 both pass)

What the counterexample does not kill: (1,5,2,1) is an M-vector, so Question 9.8 fails at the f-vector step and nowhere earlier; MacOk is defined from the family's own binRep and separates from KKOk on exactly this vector

The Kruskal–Katona pseudopower of Defs.lean obeys proved thresholds, not just decide on cases: largestBinom is the largest a with C(a,k) ≤ m, m^((k)) = 0 for m ≤ k, m^((1)) = C(m,2), 1 ≤ m^((i)) ↔ m ≥ i+1, and m^((i)) = 1 ↔ i+1 ≤ m ≤ 2i — for every m below the definition's 2¹28 fuel bound

The k-block family obeys one law for every k: with γ of the family's shape (1,…,m,1), the top Kruskal–Katona inequality holds iff m ≥ k−1 and is tight iff m ≤ 2k−4; flagness forces m ≥ mantelMin k = ⌊(k−1)²/4⌋ (Mantel), and comparing the quadratic bound with the two linear thresholds gives mantelMin k ≥ k−1 ↔ k ≥ 5 and mantelMin k ≤ 2k−4 ↔ k ≤ 8 — so k = 4 is the only k whose flag members fail the top Kruskal–Katona inequality, and the minimum flag member is exactly tight precisely for 5 ≤ k ≤ 8

The k-block scan extended from k ≤ 6 to k = 12: 168 rows over the whole flag range, each palindromic with expand γ = H, γ-positive, an M-vector, of γ-length k with γ_(k−2) = |Γ| and γ_(k−1) = 1; the k ≤ 6 part reproduces every landed bsPartTable row, and Kruskal–Katona fails exactly once, at (k,m) = (4,2)

γ₂ ≤ C(γ₁,2) is the level-1 Kruskal–Katona inequality (m^((1)) = C(m,2)); it holds with margin ≥ 2 on all 234 landed γ-positive rows and all 168 new ones; and it does not follow from H being a palindromic γ-positive M-vector — h = (1,6,12,6,1) is all three and has γ = (1,2,2) with γ₂ = 2 > 1 = C(γ₁,2)

Negative controls and one correction: the landed HuntBuildSets.lean docstring's "k = 6 … slack 0 at |Γ| = 6,.., 9" is off by one — at |Γ| = 9, 9^((4)) = 2 and the slack is 1, so the range is 6, 7, 8; the thresholds are sharp (2^((2)) = 0, 3^((2)) = 4^((2)) = 1, 5^((2)) = 2); raising the top entry of a tight member breaks Kruskal–Katona; and mantelMin 4 = 2 is exactly the failing |Γ|

The dual of the lattice of flats of every Bose–Burton geometry B_(r,k)(q) is a TN-poset: the q-Pascal matrix with bottom row the Whitney numbers Wᵣ₋ⱼ is totally nonnegative, for every r, every 0 ≤ k ≤ r-1 and every real q > 1. Proof: an explicit nonnegative resolving array in closed form, λⱼ = q^(C(s,2)-C(j,2)-j(r-1-j)) (∏ᵢ₌ₛʲ(qⁱ-1)) Σ(r,s,j) with Σ = ∑ₘ₊ₙ₌ᵣ₋ⱼ₋₁ qʲⁿ [j-s+m, m]_q > 0. In Lean: the certificate verified for 381 matrices, and total nonnegativity checked from the definition, over every one of the C(2n,n) minors, for 14 of them (corrected 2026-08-28) plus 17 perturbed matrices in the controls (r ≥ 6 priced at 8.1 GB and parked).

The Chow polynomial uH_(B_(r,k)(q)) of a Bose–Burton geometry is palindromic, has the stated γ-vector, is γ-positive, satisfies the Kruskal–Katona inequalities and is real-rooted with rk − 1 simple roots — 41 instances (q ∈ 2,3,4,5,7,9, r ≤ 8), 29 of them in the range 2 ≤ k ≤ r-2, each with a kernel-checked sign-alternation certificate.

The Chow polynomials of Bose–Burton geometries, computed inside the kernel from the Gaussian binomials by the O(r²) chain recursion rather than supplied as data: 41 instances reproduced by bbChow, 8 literature/ledger anchors, and the exact identity uH_(B_(r,1)(q)) = uH_(PG(r-1,q)) (q ≤ 5, r ≤ 8).

Kurtz's criterion γᵢ² > 4γᵢ₋₁γᵢ₊₁ holds on all 41 Bose–Burton γ-vectors, so each of those instances has a second, elementary proof of real-rootedness independent of the total-nonnegativity route; and it is strictly sufficient — it fails on CFL Example 9.5's (1,7,5,1) (correctly, that h is not real-rooted) and on γ(A₁₅) (which is real-rooted).

Negative controls for the total-nonnegativity layer: a random nonnegative bottom row usually destroys TN (45/60 at r = 4, 59/60 at r = 5; four explicit failures in Lean, two with their negative 2×2 minors exhibited), no single-entry +1 perturbation does, the admissible window for two entries is pinned exactly on both sides, the resolvability identity fails when paired with the wrong deletion, different k give different Chow polynomials, and the alternation-certificate checker rejects a truncated, a mis-signed and a reversed certificate.

For every prime power q ≥ 3 there is an explicit matroid whose Kazhdan–Lusztig polynomial is not unimodal and whose Chow polynomial equals that of a Bose–Burton geometry, hence is real-rooted: k = 6, s = [6,2]_q − [6,1]_q + 1, S a cap of size baseᵗ in AG(2t,q), r = 7 + 2t — tabulated for 17 prime powers, with both Cheng–Liu hypotheses, both cap inequalities, the strict local valley, and total nonnegativity of R(L(B_(r,6)(q))*) at r = 21 (q = 3) and r = 25 all decided in the kernel

The 21 rank-7 projective deletions PG(6,2) ∖ (P(W) ⊔ S) whose lattice of flats is not upper rank-uniform have real-rooted Chow polynomials, each with a sign-alternation certificate on 7 rational points

The rank-7 Cheng–Liu census: 26 projective deletions PG(6,2) ∖ (P(W) ⊔ S), Chow polynomial computed from the actual lattice of up to 29 211 flats, each palindromic with expand γ = H, γ-positive, Kruskal–Katona-feasible, Newton- and Kurtz-passing; Cheng–Liu Proposition 2.6 reproduced on every row

Proposition A and A′ as computed instances: the Chow polynomial of a projective deletion sees only the flat spans of rank ≥ 2, so uH_M = uH_(B_(r,k)(q)) on all 10 computed δ ≡ 0 instances (q = 2,3,5, ranks 4, 5, 7) while P_M moves by s·t, and also on 3 δ ≢ 0 instances where a partial line deletion mimics a full one; it fails on all 5 computed δ ≢ 0 instances that do not, matching Lemma B's thresholds exactly

Negative controls: the sign-alternation certificate rejects a short list, a reversed list and a point moved into a region with no sign change; the γ-vectors are pinned by expand (a ±1 perturbation of either entry breaks it); Kurtz's criterion is sharp at γ₃ = 19 851 141 against an actual 2 323 260; the resolvability identity fails when paired with the wrong Whitney row at ranks 21 and 25; the unimodality predicate is non-vacuous on both sides

Proposition A, formalized over an arbitrary field: if the deleted set contains P(W), is line-separated from W and has delta == 0, then a subspace of dimension >= 2 is a flat span iff it is not contained in W — the same condition as for the Bose–Burton geometry — hence uH_M = uH_(B_(r,k)(q)) identically in Z[X]

Lemma B, formalized in both of its forms and both characteristics: over a field with at least 3 elements and W ⊓ X = 0, S ⊆ X, the Chow polynomial does not move — uH_M = uH_(B_(r,k)(q)) identically in Z[X] — either when S is a cap (no projective line carries three of its points), or, for S a cone inside an affine chart X ∖ H with H a hyperplane of X, when S contains no full affine line; both converses hold; and over F₂ the lattices of flat spans differ already in rank 2 as soon as k >= 1, s >= 1 or k = 0, s >= 2, so delta!= 0 always

Proposition A-prime, formalized: the chain sum defining the Chow polynomial is blind to flats of rank 1, so two projective deletions whose flat spans agree in every rank >= 2 have equal Chow polynomials with no hypothesis on either; and the named instance — deleting all points of a projective line except one gives uH = uH_(B_(r,2)(q)) for every rank and every field, while delta!= 0

The abstract chain sum is the family's Chow polynomial, in two characteristics: over the computed flat-span lattices of PG(2,2) and three of its deletions it reproduces the landed bbChow 2 3 0 = 1+8t+t² and bbChow 2 3 2 = 1+7t+t² at t = 1,2,3; over PG(2,3) and four of its deletions it reproduces bbChow 3 3 0 = 1+14t+t² and bbChow 3 3 2 = 1+13t+t²; and over the Boolean lattice of rank 3 the Eulerian polynomial A₃

Negative controls for the formalization layer: the weight hypothesis w 1 = 0 is load-bearing (with w m = m the transfer fails, 95!= 86); not all projective deletions share a Chow polynomial (10 vs 9 at t = 1); agreement in rank >= 2 is strictly weaker than equality of lattices; delta!= 0 is realized; and Proposition A's hypotheses are non-vacuous on both sides

Formalization cost of this pull, measured: 3 prose theorems became 8 Lean files, 2132 lines, 91 theorems, in about 3 h 40 min of wall time and 217 s of total kernel checking