Commit 2026-06-30 17:51 ca158545

refactor(Computability.Encoding): unbundle Γ and remove FinEncoding (#37928) This PR unbundles the alphabet Γ from the Encoding structure and completely removes FinEncoding. Encoding: The alphabet Γ is now an explicit parameter: structure Encoding (α : Type u) (Γ : Type v). FinEncoding: Removed. Finiteness is now handled via standard typeclasses (e.g., [Fintype Γ] (e : Encoding α Γ)). Combinators: Functions like finEncodingPair are simplified to encodingPair, dropping the fin prefix and [Fintype] requirements where no longer needed. Downstream: Mechanically updated Mathlib.Computability and Mathlib.ModelTheory to pass the explicit Γ and use [Fintype Γ] where FinEncoding was previously required.