RE Non-Closure Under Complement

Key results: haltingUnary_complement_not_RE gives a concrete RE language whose complement is not RE, and RE_notClosedUnderComplement packages this as failure of complement closure.

The concrete witnesses come from Langlib.Classes.RecursivelyEnumerable.Examples.Halting (haltingUnaryLanguage is RE) and Langlib.Classes.RecursivelyEnumerable.Examples.NonHalting (its complement is not RE); this file only assembles them into the closure statements.

theorem RE_notClosedUnderComplement : ¬ClosedUnderComplement is_RE

Recursively enumerable languages over the unary alphabet are not closed under complement.

theorem RE_notClosedUnderComplement_of_nonempty {T : Type} [Fintype T] [Nonempty T] : ¬ClosedUnderComplement is_RE

RE languages over any nonempty finite alphabet are not closed under complement.