Formalization of Langlands's Second Main Lemma for Local Epsilon Factors
Fukuhiro Ueda
math.GM
Sep 20, 2026 · v1
TL;DR
Formalizes Langlands's Second Main Lemma for local epsilon factors in Lean 4 with Mathlib, building on a prior Lean formalization of the First Main Lemma.
Abstract
We formalize in Lean 4 Langlands's Second Main Lemma for local epsilon factors over nonarchimedean local fields. The lemma compares local constants of characters of distinct intermediate fields in a bicyclic Galois extension. The proof follows the author's companion mathematical paper and uses the formalization of the First Main Lemma. The First Main Lemma gives only a power relation, leaving a root-of-unity ambiguity. Resolving this ambiguity is the main part of the proof and requires further analysis according to ramification. The wild dyadic case is the mathematically new part of the companion proof, and its Lean formalization provides a machine-checked verification of this new case. Both mixed and equal characteristic are included. We give the exact Lean statement, identify the declarations used in the individual cases, and describe six simplifications of the mathematical proof suggested by the formalization. ChatGPT assisted with transferring formulas and citations from the mathematical manuscript and with adding references to the corresponding Lean source, and suggested improvements to the wording of the paper.
Problem
Langlands's Second Main Lemma compares local constants of characters of distinct intermediate fields in a bicyclic C_ℓ×C_ℓ Galois extension of nonarchimedean local fields. The wild dyadic case is mathematically new in the author's companion paper and needed machine-checked verification.
Approach
The proof is formalized in Lean 4 and Mathlib, following the companion paper's case division and reusing the formalized First Main Lemma. That lemma gives only a power relation, leaving a root-of-unity ambiguity. The ambiguity is resolved by ramification analysis: tame, wild odd-prime, and biquadratic (dyadic) cases. The dyadic sign is determined by comparing critical functions via Lamprecht's formula.
Results
A complete machine-checked proof is obtained in both mixed and equal characteristic, for all residue characteristics and primes ℓ. The paper states the exact Lean theorem, maps the declarations used in each case, and describes six simplifications of the mathematical proof suggested by the formalization.
