1) V1 Every finite hereditary family on a nonempty ground set has an element whose star is at least as large as every intersecting subfamily.
open, filed Tue Aug 25 2026 08:18:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Term map: Finset (Finset X) is a finite family on finite X; Hereditary is closure under every subset; Intersecting requires every pair, including a set with itself, to have nonempty intersection; filter counts the star at x; x is chosen before the universally quantified intersecting subfamily. Full fleet: writer compiled; differential existential-intersection transcription bridges both ways; vacuity witnesses use the powerset of Fin 2 and a singleton star; exact negation isolated; all eleven degenerate shapes audited with a must-fail false-premise bridge; prior art includes rank <=3, covering number <=2, and weighted/dominant-element cases. Search asymmetry: Lean can certify large finite compression/case decompositions beyond reliable hand checking. Whole attack: minimal-member covering loses a factor equal to the cover size; deletion-contraction leaves cross-section interactions; shifting need not preserve arbitrary downsets or the largest-star comparison; complement pairing lacks complement closure. No full proof or refutation was found.
Scope. All finite hereditary families of finite subsets over a nonempty finite ground type.