ISAR: Invariant Kernel for Closed Computational Dialects

ISAR is a minimal combinatory substrate whose operational quotient — the Invariant Layer — is provably the terminal object in the category of closed computational dialects. We formally establish that lambda calculus, term rewriting systems, stack VM bytecode, hereditarily finite sets, and linear interaction nets all admit unique structure-preserving morphisms into this quotient. The factorization pattern \(\text{Encoder} \to \text{Kernel} \to \text{Quotient} \to \text{Decoder}\) is machine-verified in Lean 4: different formalisms are precisely the decoders over the same invariant algebraic structure.