Conversation
…d complete production scope
Changes requested by automated reviewReviewed exact head |
|
/review |
|
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, but the PR should await declared proof provenance and validation at the current head before merge. Findings
SummaryThe PR imports the local and global class-field-theory formalization and registers it in Lean Pool.
Reviews (26) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| github_repo: n-yamaguchi-0729/ClassFieldTheory | ||
| commit: 01b4614ee76fa6f50e7f3ea3e1cff93b85693345 | ||
| license: Apache-2.0 | ||
| status: verified |
There was a problem hiding this comment.
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!
🤖 LLM review (
|
| 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 ofrestrictNormalHom_infiniteGlobalArtinMonoidHom_of_scalarTowerinInfiniteGlobalArtin.lean:728, which is already transitively imported.CyclotomicUnramifiedLocalGlobalCompatibility.lean:92repeats the argument again after applyingMonoidHom.ext. Another substantial duplication is the bounded-naturals proof inValuation/AbsoluteValue/Nonarchimedean.leanandValuation/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 privaterestrictNormalHom_infiniteGlobalArtinMonoidHom_of_towerand publicrestrictNormalHom_infiniteGlobalArtinMonoidHom_of_scalarTowerboth concludeAlgEquiv.restrictNormalHom E (infiniteGlobalArtinMonoidHom K Ω a) = globalArtinMonoidHom (K := K) (L := E) a := byand start withlet j : E →ₐ[K] Ω := IsScalarTower.toAlgHom K E Ω. The third copy followsapply MonoidHom.ext; intro a. In the absolute-value files,private theorem add_le_root_bound_of_bounded_natat line 145 andtheorem add_le_root_bound_of_bounded_natat line 624 have identical statements and bodies, includingrw [Real.mul_rpow hcoef_nonneg (pow_nonneg hM_nonneg n)]andrw [Real.pow_rpow_inv_natCast hM_nonneg hn]. - dead-code —
LeanPool/ClassFieldTheory/ClassFieldTheory/AbstractClassFieldTheory/Reciprocity/Construction/MainTransferFrobenius.lean:922
BothtransferNormNaturalityTransferNormFiber_sumhere andtransferNormNaturalityNorm_eq_sum_transferOrbitRepresentativesat line 100 are substantial private lemmas with no references or automation attributes. The finaltransferNormNaturalityNorm_eq_sum_transferNormsinstead 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 declaresprivate theorem transferNormNaturalityNorm_eq_sum_transferOrbitRepresentativesandprivate theorem transferNormNaturalityTransferNormFiber_sum; each name occurs only at its declaration. The latter proof containsrw [relativeNorm_apply_coe, relativeNormValue]and finishes withexact Internal.transferNormNaturalityTransferNormFiber_term D A E L hL σ q π hSβC kq. The final public theorem repeats that rewrite and concludes the corresponding calculation withexact 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.
# Conflicts: # LeanPool.lean
Changes requested by automated reviewReviewed exact current head |
Changes requested by automated reviewReviewed head
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. |
…ieldtheory # Conflicts: # LeanPool/projects.yml
…ieldtheory # Conflicts: # LeanPool/projects.yml
Vilin97
removed
the
needs-manual-rebase
Changes requested by automated reviewReviewed The complete source check finds one remaining blocking 285-code-line proof at I inspected the full changed-file census, advertised declarations and dependency closure, prior source reviews and repairs, and reconciled the incoming delta. The quoted counts were reproduced locally from this exact head with the unchanged repository source checker. Pending CI is not represented as success. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_commit": "f9255fdda770ca8a8522a8f9850d9d078d730617",
"scope": "Complete source review of the 12-file incoming repair since f8639ee; 46 insertions and 50 deletions. This does not repeat or replace the full-project review.",
"conclusion": "The incoming repair is accepted on source review. This PR remains unready for merge: proof provenance, the remaining 285-line proof and full final-head validation are still pending.",
"source_evidence": [
"Seven unused witness names become anonymous while retaining every existential or let-bound finiteness witness. No assumptions or existence conclusions are removed.",
"The local T2Space instance is derived from krullTopology_t2. Six norm-residue/restriction/transfer definitions retain their instances and exact construction arguments while replacing tactic-based inferred results with direct terms.",
"The explicit power-series coefficient homomorphism and inverse-unit Frobenius RingEquiv are the same maps required by the existing proofs. The discrete UniformSpace definition remains a local instance. The theta coefficient identity uses explicit multiplication commutativity with the same semilinearity fact.",
"All 1,822 project paths and the complete registry bytes are unchanged from the reviewed base. The reported missing AmbientPrimeTargetComparison import is absent from the current root index."
],
"validation": "Inspected the author/importer frontier90 artifact at this exact head: all 12 target modules passed, 4,624 jobs, exit 0, zero warnings or errors. This is inspected existing evidence, not a new independent compilation. Full build, complete scoped declaration/style lint, compiled axiom/environment checks and required CI remain pending.",
"remaining": "Proof provenance remains unset pending evidence. numberFieldTowerFinitePadicAuxiliaryLocalGlobalRepresentative_nonempty is still the unchanged 285-line block. A separate proof-split proposal is not published or claimed compiled."
}
Changes requested by automated reviewReviewed Blocking finding: Evidence: exact-head build log. Acceptance condition: the complete project, repository quality/axiom gates and required protected checks pass on the repaired head, and the remaining substantive/maintainability findings are resolved. The prior bot verdict does not override these reproduced source/build failures. |
# Conflicts: # LeanPool/projects.yml
Changes requested by automated reviewReconciled to exact current head Preserve the valid completed repairs. Merge requires the cited author-actionable defects to be resolved and all protected checks to pass at the resulting head; this is not a needs-maintainer handoff. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "9a2bc40705df6ada374c78fc7c930a9b13bdf9ea",
"verdict": "needs_discussion",
"scope": "Focused follow-up on the two ClassFieldTheory compiler-repair modules; this is not a new full-project or five-rubric acceptance review.",
"source_evidence": [
"The existing finiteGaloisAbstractExtensionOfEmbedding_bundle_finite and equalCharacteristicDirectThetaCompletedLevelCharP instances are public, with their original propositions and proof witnesses. The completed-base characteristic and conjugation proof helpers remain private.",
"The quotient-conjugation and norm-conjugation constructions retain the same equivalence/homomorphism compositions. Explicit local Normal witnesses come from the original finite-Galois bundles; AddZeroClass values are the same canonical finiteNormQuotientAddCommGroup projections.",
"The final reciprocity independence proof uses the existing Hausdorff instance and unchanged diagram chase. The private helper type-variable rename removes a notation collision without changing its mathematical type. All public endpoint contracts are retained."
],
"validation": {
"project_modules": "ThetaLocalInverse, ConcreteReciprocityCanonical and DirectThetaAtCompletedLevel compile warning-free under the original repository options and pinned Lean 4.34.0.",
"cache_provenance": "193 closed prerequisite modules certified against exact native source hashes and 1,158 artifact hashes; all 664 internal dependency fingerprints independently match. Subsequent continuations preserve all 1,176 artifact parts by SHA guards.",
"api_and_axioms": "Two downstream public-instance synthesis examples and all four exact-name axiom checks pass without warnings. Each report contains only Classical.choice, Quot.sound and propext.",
"static": "Header, forbidden-text, file-size, proof-size and diff checks pass for the two edited files. The 1,822-module inventory and raw project card, aggregate index, project umbrella and toolchain/configuration bytes are unchanged."
},
"limits": [
"No fresh full-project build, module-linter run or native index execution is claimed; current-head CI remains necessary.",
"The explicit WIP/first-party proof-provenance hold remains. No source acquisition or proof-authorship uncertainty is resolved by this compiler repair.",
"The separate earlier proof-splitting draft and importer checkout were left untouched."
],
"findings": [],
"ci_context": {
"diagnostic_head": "cbed49b0a9dd43328f6813a32452fc9998891dd0",
"run": "https://github.com/Vilin97/lean-pool/actions/runs/36226656608",
"limitation": "Fresh CI on the published head is still required."
}
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "702b0053b89035c65580aa3cbe2763c37ff7d4d4",
"verdict": "needs_discussion",
"scope": "Focused repair of the current ClassFieldTheory CI failure families; prior source assessment and WIP/proof-provenance holds remain. This is not whole-project acceptance.",
"diagnostic_evidence": {
"head": "9a2bc40705df6ada374c78fc7c930a9b13bdf9ea",
"job": "https://github.com/Vilin97/lean-pool/actions/runs/36233242983/job/108380277870",
"result": "The two previously repaired modules ConcreteReciprocityCanonical and DirectThetaAtCompletedLevel built successfully. The build then reported 42 error headers and 12 warning headers across 12 modules. Six sorry notices were elaboration-recovery cascades; the two implicated source modules contain no sorry/admit."
},
"changes": [
"Correct the scoped decomposition-group theorem namespace to its actual root HilbertRamification namespace.",
"Expose only the required existing action providers, quotient topology, tower embedding and descended Hilbert-symbol homomorphism data. Their bodies, maps and mathematical parameters are unchanged; the quotient-topology instance registration remains local.",
"Keep the private finiteness proof behind an explicit by/exact boundary, and supply unramifiedFrobenius with the same finite-Galois bundle Normal witness. No caller hypothesis is added.",
"Use the canonical Hausdorff Krull-topology proof in a named local instance before the PrimeNorm theorem; reuse the already-public completed-level CharP proof in two existing private instances. No compiler limits or global instance registrations are changed.",
"Finish the Adele pure-tensor comparison with the already-imported infinitePlaceCompletionAlgEquiv_algebraMap commuting square, evaluated at the original coefficient and unwrapped with Completion.ext.",
"Make three unused existential binder names anonymous while retaining the same existential propositions."
],
"validation": {
"source": "All three disjoint components independently source-reviewed, including canonical topology/normality/characteristic witnesses and the existing completion-map bridge.",
"static": "The four existing scoped source gates (headers, forbidden text, file sizes and proof sizes), diff whitespace check and changed-line length check pass.",
"preservation": "All 1,822 project source files remain. The other 1,810 source files are byte-identical; the full registry/card bytes, aggregate index, project umbrella and toolchain/configuration bytes are unchanged.",
"compilation": "No local compiler, module linter, native index or compiled trust run was performed for this 12-file follow-up. Fresh exact-head CI must validate elaboration and determine whether all downstream cascades clear."
},
"limits": [
"The failing prior run skipped challenge/solution builds, declaration lint, text style and repository quality after its build failure; those are not passes.",
"The existing WIP and first-party proof-authorship/provenance hold remain. No source acquisition uncertainty is settled here.",
"The separate proof-split draft and importer were untouched; no gates, options, waivers, queue state or labels were changed."
]
}
# Conflicts: # LeanPool/projects.yml
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review_type": "scoped compiler repair and incoming-main reconciliation",
"verdict": "needs_discussion",
"scope": "Eight Lean source files: six modules with compiler errors and two scoped-open formatting warnings.",
"repair_assessment": "The fixed-field notation names its existing field projection explicitly. Two existing data providers used by exposed interfaces become public without changing their values, and two inference-sensitive maps use their unchanged algebraic term bodies. Proposition-valued arguments explicitly elaborate the existing private proofs. The completed-level characteristic instance reuses the existing public provider. The completion-map isometry is proved through its public continuity and dense-coercion laws, retaining the original composed isometry rather than unfolding an imported opaque definition. Two empty lines are removed.",
"preservation": "The incoming main integration preserves the complete 1,822-file project, its card and its index entries. Existing theorem statements, mathematical assumptions, map constructions and imports are retained; the two deliberate data visibility changes are identified above.",
"validation": "At the previous source checkpoint, eleven of twelve earlier repaired modules compiled; the build then reported 47 errors across six modules and two formatting warnings. The new completion-map proof separately compiles against pinned Mathlib in 2.54 seconds and depends only on propext, Classical.choice and Quot.sound. This standalone check does not establish a complete project build; fresh current-head CI is still required. The four existing scoped source/header/file-size/proof-size gates, diff whitespace and new-line-length checks pass; all 1,814 untouched project files and the complete registry, index, compiler settings and gate trees are preserved.",
"hold": "This approval is confined to the reviewed repair. The current WIP and first-party provenance hold remains; do not merge on this repair alone.",
"findings": [],
"repair_verdict": "pass",
"merge_ready": false,
"reviewed_head": "e3449747fc6b2fe4a0c837ae4183a14cfb246473",
"baseline": "ae50279f3f953b67f827d65aa41ac05d07085499"
}
# Conflicts: # LeanPool/projects.yml
This branch has not been deployed
1 participant
WIP: complete ClassFieldTheory import
Preserves all 1,655 upstream source modules from
n-yamaguchi-0729/ClassFieldTheory
at
01b4614ee76fa6f50e7f3ea3e1cff93b85693345, 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; the upstream license is Apache-2.0.
The import ports the complete source to Lean/Mathlib 4.34.0 and the repository's module
system. Norm, fixed-field, ramification, and cohomology arguments are extracted into
smaller proof components. Public data interfaces retain their original constructions;
private proof helpers remain private where direct proof arguments permit it. No substantive
source modules or proved results are omitted. This is a content-only PR; gates, limits,
compiler options, and waiver settings are unchanged.
Validation at
f9255fdda770ca8a8522a8f9850d9d078d730617: the twelve changed modules pass atargeted build covering 4,624 jobs, with zero warnings or errors. This includes all five
modules that failed in the previous complete 6,147-job build, together with seven harmless
unused witness-name cleanups. All original finiteness and existence hypotheses are retained.
The source index exactly covers all 1,822 pooled files.
One oversized proof remains, reduced from the original 66. Its semantic norm/Artin transport
split is prepared and undergoing a bounded kernel check; it is not yet applied or claimed to
compile. The complete source audit otherwise passes header, forbidden-text and size checks.
The exact-module linter driver is validated with all fifteen official linters and batches
capped at 128 declarations; a fresh complete build, full scoped declaration/style lint,
compiled axiom/environment audits, and checks at the final remote head remain pending.
Proof provenance still needs explicit evidence or the submitter's answer. It remains unset
rather than inferred from author names. The current remote lifecycle is preserved.
Do not merge.