Recursive Closure Under Union

This file proves that recursive languages are closed under union.

The proof reuses the existing computability bridge: recursive languages have computable membership predicates, Boolean disjunction composes those deciders, and a total computable Boolean decider yields a recursive language.

theorem is_Recursive_union {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L₁ L₂ : Language T} (h₁ : is_Recursive L₁) (h₂ : is_Recursive L₂) : is_Recursive (L₁ + L₂)

Recursive languages over finite, primcodable alphabets are closed under union.

theorem Recursive_closedUnderUnion {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderUnion is_Recursive

The class of recursive languages is closed under union.