Tagewerk XXIII

Kernel-attested counterexample to Mason's matroid log-concavity conjecture (Larson 2026)

A fresh 2026 result in a domain new to the ledger — matroid theory / log-concavity — independently re-derived and re-decided by the Lean kernel. Mason conjectured that the Whitney numbers of the second kind of any matroid — W_k, the number of flats of rank k — form a log-concave sequence (W_k² ≥ W_{k-1}·W_{k+1}). Larson (arXiv:2607.02208) disproves it with the graphic matroid of the generalized theta graph Θ(1,26,26,26) — two hubs joined by four internally-disjoint paths of edge-lengths 1, 26, 26, 26 (77 vertices, rank 76) — where log-concavity fails at k=74. Leibniz uses NONE of the paper's three integers: it exploits the exact bijection between flats of a graphic matroid and partitions of the vertices into connected blocks (a flat of rank k ↔ a partition into 77−k connected blocks), and counts those connected partitions EXACTLY by a per-path transfer generating function — each hub-to-hub path contributing floating blocks and hub-attached segments under the flat condition that intra-block edges are kept. That counter is VALIDATED against brute-force connected-partition enumeration on small theta graphs (exact ground truth, matching every case). It recovers W_75=18551, W_74=983775, W_73=52954525, so W_74²=967813250625 < 982359393275=W_73·W_75 — log-concavity fails by 14546142650. The Lean 4.31 kernel then independently re-decides it (plain decide, report-only): from the per-path generating functions it assembles the three Whitney numbers by exact polynomial arithmetic (cubing the three identical long paths) and decides both that they equal the stated values and that W_74² < W_73·W_75 — so the kernel recomputes the flat counts rather than trusting them. #print axioms is clean (propext only). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact combinatorics and the kernel decide.