Indexed languages are not closed under complement

If indexed languages were closed under complement, their closure under union would imply closure under intersection by De Morgan's law. This contradicts the binary intersection witness, and the same argument applies after its transport to every alphabet with at least two symbols.

theorem IndexedComplementNonclosure.Indexed_notClosedUnderComplement : ¬ClosedUnderComplement is_Indexed

Indexed languages over the binary alphabet are not closed under complement.

theorem IndexedComplementNonclosure.Indexed_notClosedUnderComplement_of_embedding {α : Type} (e : Bool ↪ α) : ¬ClosedUnderComplement is_Indexed

An embedding of the binary alphabet gives complement nonclosure over the target alphabet.

theorem IndexedComplementNonclosure.Indexed_notClosedUnderComplement_of_two {α : Type} (a b : α) (hab : a ≠ b) : ¬ClosedUnderComplement is_Indexed

Indexed languages are not closed under complement over any alphabet containing two specified distinct symbols.

theorem IndexedComplementNonclosure.Indexed_notClosedUnderComplement_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderComplement is_Indexed

Indexed languages are not closed under complement over every finite alphabet with at least two symbols.