FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS
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.
Related
- FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS
- A LOCAL PROOF OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS OVER NONARCHIMEDEAN LOCAL FIELDS
- A LOCAL PROOF OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS OVER NONARCHIMEDEAN LOCAL FIELDS
- Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
- Langlands-Shahidi gamma factors and local transfer in families
BibTeX
@misc{ueda2026formalization,
title = {{FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS}},
author = {Fukuhiro Ueda},
howpublished = {HAL},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.30301},
eprint = {2609.30301},
archivePrefix = {arXiv},
url = {https://hal.science/hal-05756351v1},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS
AU - Fukuhiro Ueda
PY - 2026
DA - 2026/09/21
PB - HAL
DO - 10.48550/arxiv.2609.30301
UR - https://hal.science/hal-05756351v1
AB - 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.
ER -