{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": null,
  "author_total": 1,
  "authors": [
    {
      "name": "Fukuhiro Ueda"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/3r1c95n8a2yz7.bib",
  "cited_by": 0,
  "doi": null,
  "fulltext_url": null,
  "id": "3r1c95n8a2yz7",
  "issns": [],
  "landing_url": "https://hal.science/hal-05746185v1",
  "language": "en",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [
    [
      "hal",
      "0.math"
    ]
  ],
  "openalex": null,
  "pdf_url": "https://hal.science/hal-05746185/document",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-11",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/3r1c95n8a2yz7.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:33Z",
      "native_id": "hal-05746185",
      "source": "hal",
      "url": "https://hal.science/hal-05746185v1"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "hal:0.math",
      "subfield": "general"
    }
  ],
  "title": "FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS",
  "title_text": "FORMALIZATION OF LANGLANDS'S FIRST MAIN LEMMA FOR LOCAL EPSILON FACTORS",
  "type": "preprint",
  "updated_at": "2026-10-30T12:17:33Z",
  "url": "https://research.draconitic.com/paper/3r1c95n8a2yz7",
  "venue": "HAL",
  "versions": []
}