Formalization of Langlands's Second Main Lemma for Local Epsilon Factors

Abstract

We describe the Lean 4 formalization of Langlands's Second Main Lemma for local epsilon factors over nonarchimedean local fields, in mixed and equal characteristic. The lemma compares the induction expressions attached to compatible characters of the intermediate fields of a bicyclic extension of prime-square degree. We explain the mathematical constructions and comparisons that constitute the proof, and identify their Lean declarations.

arXiv commentCompanion formalization to "A Local Proof of Langlands's Second Main Lemma for Local Epsilon Factors over Nonarchimedean Local Fields" (arXiv:2609.13960)