WIP: Import Local and global class field theory

[Vilin97]

Imports all 1,655 source modules from n-yamaguchi-0729/ClassFieldTheory, represented by 1,822 pooled Lean files. The scope includes local and global class field theory, reciprocity, Lubin–Tate theory, ramification, and the required Galois-cohomology and valued-field libraries. Original copyright and author notices are retained under Apache-2.0.

The port preserves the source statements and uses the repository's module system; norm, fixed-field, ramification, and cohomology proofs have been factored without dropping the original statements. The source index covers all 1,822 pooled files.

Current published head (2026-10-01): 90e7949e44cc7cd7f8db817f01884d28466c9965 contains the automatic merge of current main and its compact generated project-root index. The old aggregate-index line-cap failure is resolved. Protected CI for this head is running or queued; its final result is not yet known. The prior hosted build reported proof whnf timeouts in FixedFieldLocalData and IdeleClassDirectLimitExtension plus a dependent unknown theorem.

The local Lean 4.35.0-rc3 worktree has eleven unpushed source repairs. The corrected norm-quotient module passed a scoped exact build; a source-guarded diagnostic is locating the remaining fixed-field timeout. Structural timeout repairs, full build, declaration/style lint, compiled axiom audit, and final-head checks remain outstanding. The local card now records provenance: mix, based on the upstream authorship and AI-assistance disclosure; that card edit is not yet published. Gates, limits, compiler options, and waiver settings are unchanged.

Part of the requested 42-project import batch. Do not merge yet.

[Vilin97]

Changes requested by automated review

Reviewed exact head f4bc899af6cb444bd49fb18f8e8bf37d8b14532c. The exact-head ClassFieldTheory build fails in KroneckerWeber/RationalRayClassFieldCyclotomic.lean with parser errors, unknown rationalRayClassFieldCyclotomicLevelAbelianGalois, unsolved goals, and repeated instance synthesis failures. Repair this proof-bearing file and its dependent closure before requesting merge, then rerun all gates.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds mathematical library code for class field theory.

No new blocking defect was established; this incomplete review does not establish that the PR is safe to merge.

Findings

1.  Missing proof provenance ▶

Summary

Adds class field theory modules, public import indexes, and a project card naming local and global reciprocity as its main results.

• The inspected headline statements match their stated field-norm and topological-quotient claims.
• Review coverage is incomplete: most of the large diff was not individually inspected. Full source fidelity, attribution, novelty, completeness, and measured cost remain unverified.
• Vilin97 explicitly acknowledged the unpublished provenance: mix edit, fixed-field and direct-limit proof timeouts, eleven unpushed repairs, and pending build, lint, and axiom checks. These are not repeated as findings.
• This review concerns 0196edb2b9a75ca9290817fffa7d6afcab367f8e, not the different published head described in the PR.

_{Reviews (2) · Last reviewed commit: "Merge current main and migrate PR #506 t..." · Reviewed by Greptile}

[greptile-apps]

Missing proof provenance

The new project entry ends with status: verified but does not declare whether its Lean proofs have human, AI, or mix provenance. This violates the contribution directive that every project card must classify proof provenance, so the repository requirement must be satisfied before merging.

File Used: CONTRIBUTING.md (source)

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: 1a19b5c6405e942305a3e704da1161426bd62f24

Verdict: 🤔 needs_discussion — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Both card headlines match their Lean statements, with no undisclosed substantive assumptions found.
Novelty	✅ pass	Searches of pinned Mathlib 4.34.0 and the existing pool found no duplicate of either headline reciprocity theorem.
Significance	✅ pass	The local and global reciprocity and existence theorems constitute a substantial theory-building project suitable for the pool.
Sources	✅ pass	The explicitly credited pinned upstream source supports the claimed results; no citation mismatch or uncredited formalization was identified.
Code quality (advisory)	🤔 discuss	The code is broadly competent, but duplicated proofs and unused private transfer helpers warrant a cleanup pass.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The local theorem assumes a finite abelian Galois extension of a nonarchimedean local field; the global theorem assumes a number field, consistent with the card’s scope. The internal class-field axioms are proved and supplied by constructions, not assumed by the headlines.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	algebraic number theory
Mode	theory_building
Code quality	3 / 5

Statement check: Local reciprocity supplies a continuous surjective homomorphism with precisely the field-norm kernel; global reciprocity supplies the stated topological group isomorphism for number fields.

Develops class field theory through reciprocity and classification of abelian extensions, with major results including Hasse–Arf, the cyclic Hasse norm theorem, and Kronecker–Weber.

Code quality findings (2)

• duplicate-proof — LeanPool/ClassFieldTheory/ClassFieldTheory/GlobalClassFieldTheory/Reciprocity/CyclotomicUnramifiedGeometricRestriction.lean:659
  This private restriction lemma duplicates the statement and proof of restrictNormalHom_infiniteGlobalArtinMonoidHom_of_scalarTower in InfiniteGlobalArtin.lean:728, which is already transitively imported. CyclotomicUnramifiedLocalGlobalCompatibility.lean:92 repeats the argument again after applying MonoidHom.ext. Another substantial duplication is the bounded-naturals proof in Valuation/AbsoluteValue/Nonarchimedean.lean and Valuation/AbsoluteValue/Theory/AbsoluteValues.lean, including the binomial estimate, root bound, and limiting argument. Share these implementations and retain thin interface lemmas; otherwise API changes require repairing multiple copies.
  Evidence: The private restrictNormalHom_infiniteGlobalArtinMonoidHom_of_tower and public restrictNormalHom_infiniteGlobalArtinMonoidHom_of_scalarTower both conclude AlgEquiv.restrictNormalHom E (infiniteGlobalArtinMonoidHom K Ω a) = globalArtinMonoidHom (K := K) (L := E) a := by and start with let j : E →ₐ[K] Ω := IsScalarTower.toAlgHom K E Ω. The third copy follows apply MonoidHom.ext; intro a. In the absolute-value files, private theorem add_le_root_bound_of_bounded_nat at line 145 and theorem add_le_root_bound_of_bounded_nat at line 624 have identical statements and bodies, including rw [Real.mul_rpow hcoef_nonneg (pow_nonneg hM_nonneg n)] and rw [Real.pow_rpow_inv_natCast hM_nonneg hn].
• dead-code — LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Reciprocity/Construction/MainTransferFrobenius.lean:922
  Both transferNormNaturalityTransferNormFiber_sum here and transferNormNaturalityNorm_eq_sum_transferOrbitRepresentatives at line 100 are substantial private lemmas with no references or automation attributes. The final transferNormNaturalityNorm_eq_sum_transferNorms instead reconstructs their norm-expansion and reindexing arguments. Use the helpers in that proof or remove the unused variants so maintainers do not have to preserve parallel, inaccessible implementations.
  Evidence: The diff declares private theorem transferNormNaturalityNorm_eq_sum_transferOrbitRepresentatives and private theorem transferNormNaturalityTransferNormFiber_sum; each name occurs only at its declaration. The latter proof contains rw [relativeNorm_apply_coe, relativeNormValue] and finishes with exact Internal.transferNormNaturalityTransferNormFiber_term D A E L hL σ q π hSβC kq. The final public theorem repeats that rewrite and concludes the corresponding calculation with exact Internal.transferNormNaturalityTransferNormFiber_term D A E L hL σ qT π hSβC kq.

---

Tokens: 4,166,841 in / 34,996 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $85.9615 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

CI was not green for this commit at review time; this review does not replace CI.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 57b50b3579566a2c384c7490c6943ec8779cdfe6. ClassFieldTheory still fails in KroneckerWeber/RationalRayClassFieldCyclotomic.lean with parser/unknown-constant errors, unsolved goals, and repeated instance synthesis failures. Repair the proof-bearing closure and rerun all gates.

[Vilin97]

Changes requested by automated review

Reviewed head 92c31417fde0f2d9c4d40f964e5e6e15b6b6179b. Major reciprocity targets with real implementation failures; size alone is not a blocker.

1. Complete the pinned-toolchain integration. The previous source-identical build failed at 7a2d402a15a1a85d4756cdb4abb08ebbc15d213d. The same source-level blocker is present at this reviewed head; its error includes:

   error: LeanPool/ClassFieldTheory/ClassFieldTheory/KroneckerWeber/RationalRayClassFieldCyclotomic.lean:212:13: unexpected token '/--'; expected 'lemma'
   

   The file/dependency audit finds 1821 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The build reports syntax failures around the interposed doc comments after noncomputable in RationalRayClassFieldCyclotomic.lean:212,223, followed by dependent unknown constants. Repair the definitions and rebuild their closure; resolve the first real errors rather than suppressing diagnostics or counting downstream declarations as proved.

Review coverage: complete changed-file inventory and full diff retained; 1821 changed project files, 519,861 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Local/global class-field and cyclotomic infrastructure. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

Exact-head reconciliation: the automatic main merge left all project Lean source and the pinned toolchain unchanged. This run restored the original parsed project card after the rebase parser dropped the title-first entry; parsed-card equality and the generated module-index check pass. The restoration is a narrowly scoped fast-forward commit from an isolated worktree. It does not repair the substantive blockers above; new CI is not assumed green.