A witnessed minimal-non-face count bounds the vertex count of any flag stellar refinement
ProvedHirsch.flag_refinement_vertex_lower_boundLet be a finite simplicial complex with a witnessed set of minimal non-faces, and let a finite chain of stellar subdivisions (each at a face of the current complex, using a fresh vertex unused so far) turn into a flag complex . Then
Combined with stellar_injects_minimal_nonfaces (minimal non-faces only accumulate, never disappear, along the chain, up to relabeling by the injection at each step) and the definition of flagness (every minimal non-face of has exactly vertices, so there are at most of them), this gives a lower bound on how many vertices any stellar path to a flag complex must eventually use, in terms of 's own non-face complexity.
Scope caveat, preserved from the research notes: vertexCard growth per stellar step is not simply in general — a singleton- step nets (one vertex removed, one added), a step nets ; the statement's vertexCard correctly measures the actual final support size of regardless, so the bound is not weakened by this, but a "simplification" assuming would be incorrect and is not made here.
import Mathlib import Definitions.Def_Hirsch_simplicial_complex_flag
namespace Hirsch
theorem flag_refinement_vertex_lower_bound {V : Type*} [DecidableEq V] [Fintype V]
(K : SComplex V) (μ : ℕ)
(hμ : ∃ Ms : Finset (Finset V), Ms.card = μ ∧ ∀ M ∈ Ms, K.IsMinimalNonface M)
(L : List (Finset V × V))
(Ks : List (SComplex V))
(hlen : Ks.length = L.length + 1)
(h0 : Ks.head? = some K)
(hstep : ∀ i (hi : i < L.length),
(Ks.get ⟨i + 1, by omega⟩).faces = SComplex.stellar (Ks.get ⟨i, by omega⟩) (L.get ⟨i, hi⟩).1 (L.get ⟨i, hi⟩).2 ∧
(L.get ⟨i, hi⟩).1 ∈ (Ks.get ⟨i, by omega⟩).faces ∧ (L.get ⟨i, hi⟩).1.Nonempty ∧
∀ F ∈ (Ks.get ⟨i, by omega⟩).faces, (L.get ⟨i, hi⟩).2 ∉ F)
(hflag : ∀ Klast, Ks.getLast? = some Klast → Klast.IsFlag) :
∀ Klast, Ks.getLast? = some Klast → μ ≤ Klast.vertexCard.choose 2 := by sorry
end Hirsch