Formalization of Langlands's Second Main Lemma for Local Epsilon Factors
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.30301
curl -X POST /api/v1/records/arxiv/2609.30301/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.30301/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'