Protected-facet intervals bound the number of visited uniform states
ProvedHirsch.protected_facet_state_countFor a finite injective sequence P of n distinct d-element subsets of a finite ground set V, suppose every label outside a specified finite exception set B occurs during at most one interval of the sequence. Then n <= (|V|-d+1)2^|B|. More precisely, for any finite collection C covering all exceptional signatures P(i) intersect B, n <= (|V|-d+1)|C| and n <= sum over S in C of (|V minus B| - (d-|S|)+1), with natural-number truncated subtraction. The proof constructs the encoding (current exceptional signature, count of previously seen protected labels no longer active) and proves it injective. No bound on visits per signature is an assumption. No adjacency, geometric realization, small exception-set existence, flagness, or polynomial diameter is assumed or concluded. This is the positive finite counting core of the project's conditional facet-confinement route bound.
import Mathlib open scoped BigOperators
namespace Hirsch
theorem protected_facet_state_count
(n d : ℕ) (V B : Finset ℕ) (P : Fin n → Finset ℕ)
(hV : ∀ i, P i ⊆ V)
(hcard : ∀ i, (P i).card = d)
(hinj : Function.Injective P)
(hinterval : ∀ a, a ∉ B → ∀ i j k : Fin n, i ≤ j → j ≤ k →
a ∈ P i → a ∈ P k → a ∈ P j) :
n ≤ (V.card - d + 1) * 2 ^ B.card ∧
∀ C : Finset (Finset ℕ), (∀ i, P i ∩ B ∈ C) →
n ≤ (V.card - d + 1) * C.card ∧
n ≤ ∑ S ∈ C, ((V \ B).card - (d - S.card) + 1) := by sorry
end Hirsch