Skip to content
DraconiticResearch
Search Sources API
197,788 studies31 sourcesUpdated 22 min ago
PreprintCC BY 4.0HAL

FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS

  • Fukuhiro Ueda
Open at sourcePDFCite

Abstract

We formalize in Lean 4 Langlands's First Main Lemma for local epsilon factors over all nonarchimedean local fields. This equality of local constants in cyclic extensions of prime degree is one of the four Main Lemmas used in Langlands's construction of epsilon factors of local Weil representations. The proof follows the author's companion paper, which reconstructs and completes the local arguments of Dwork and Langlands, including the equal-characteristic case. The First Main Lemma also follows from Deligne's construction of local epsilon factors by global methods; here we formalize a purely local proof. The development includes the finite-sum and Haar-integral constructions of local constants, the required ramification and finite-field identities, and the comparison of stationary representatives under twisting and norm.ChatGPT and Codex assisted with parts of the Lean development. The author used ChatGPT to check the manuscript for consistency and to suggest improvements to wording and organization of materials.

Related

  1. FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS
    Fukuhiro Ueda
    HALPreprintCC BY 4.0Full textMathematical physicsHALarXiv
  2. A LOCAL PROOF OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS OVER NONARCHIMEDEAN LOCAL FIELDS
    Fukuhiro Ueda
    HALPreprintCC BY 4.0Full textMathematical physicsHALarXiv
  3. A LOCAL PROOF OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS OVER NONARCHIMEDEAN LOCAL FIELDS
    Fukuhiro Ueda
    HALPreprintPublisher termsFull textAlgebra & number theoryHALarXiv
  4. Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
    Zoltán Gábor Molnár, Csaba Tóth
    arXivPreprintarXiv licenceFull textAlgebra & number theoryLogic & foundationsarXiv
  5. Langlands-Shahidi gamma factors and local transfer in families
    Johannes Girsch, Robert Kurinczuk
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv

Cite

BibTeXRIS
BibTeX
@misc{ueda2026formalization,
  title = {{FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS}},
  author = {Fukuhiro Ueda},
  howpublished = {HAL},
  year = {2026},
  month = sep,
  url = {https://hal.science/hal-05746185v1},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS
AU  - Fukuhiro Ueda
PY  - 2026
DA  - 2026/09/11
PB  - HAL
UR  - https://hal.science/hal-05746185v1
AB  - We formalize in Lean 4 Langlands's First Main Lemma for local epsilon factors over all nonarchimedean local fields. This equality of local constants in cyclic extensions of prime degree is one of the four Main Lemmas used in Langlands's construction of epsilon factors of local Weil representations. The proof follows the author's companion paper, which reconstructs and completes the local arguments of Dwork and Langlands, including the equal-characteristic case. The First Main Lemma also follows from Deligne's construction of local epsilon factors by global methods; here we formalize a purely local proof. The development includes the finite-sum and Haar-integral constructions of local constants, the required ramification and finite-field identities, and the comparison of stationary representatives under twisting and norm.ChatGPT and Codex assisted with parts of the Lean development. The author used ChatGPT to check the manuscript for consistency and to suggest improvements to wording and organization of materials.
ER  -