Repository navigation
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] The confirmed documentation issue is non-blocking, but this review does not establish whole-project merge readiness. Findings
SummaryImports Eichler–Shimura material and supporting results about modular curves and elliptic curves. The latest changes mostly remove unused proof helpers and shorten proofs.
Reviews (13) · Last reviewed commit: "remove redundant material" · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Retain applicable upstream attribution; preserve every mathematical source file.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Scoped source review at 7860bd069f06153b6c96d46f6f6fcbbdb44e7b4f of the four advertised results and their supporting constructions.
The Eichler–Shimura result proves injective holomorphic and antiholomorphic maps with complementary ranges in the actual parabolic cocycle quotient. Its Hecke intertwining clauses quantify over a supplied cohomology operator and require that operator to descend from coeffHeckeFun (the all-primes theorem, lines 204–237). The card now states that condition. The good-prime Tate-module results use the genuine inverse-limit torsion representation; their cardinality hypothesis is already disclosed in the card.
The submitted head named a missing LeanPool.FLTEichlerShimura entry. Commit 7860bd069f06153b6c96d46f6f6fcbbdb44e7b4f adds that entry with the four headline imports and applicable upstream attribution, regenerates the project index, and corrects the card. The actual index/card checks and complete import DAG pass. All 1,192 mathematical files remain byte-identical; no hypothesis, proof, option, or gate changes.
Maintenance advisory: five RationalFunctionField modules contain roughly 2,600 matching helper lines after only solution-namespace normalization. A shared helper module would avoid repeating future repairs. I am retaining that finding as advisory while the independent project review weighs the import.
This audit covers the complete file inventory, the headline statements, selected supporting definitions/proofs, provenance samples, and the complete import graph. It does not claim a line-by-line review of all 1,192 proof modules or a completed build. Whole-import acceptance remains pending the independent configured review and complete current-head protected validation; current-main validation is also pending.
|
/review Please review exact head 7860bd0 under the current five project rubrics, including prior-art comparison and explicit coverage limits. The scoped source audit is review 5592057176. The card/entry/index repair preserves all 1,192 mathematical files. Current-head CI and current-main qualification remain independent pending requirements. |
Refresh the generated project card and retain all author proof changes and attribution.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Follow-up source review at 8b9383bc75adcdca8e3bdb81567651dbfd7bbfcb.
The author's da8d283 adds six complete proofs. The transfer formula preserves cocycles and coboundaries; the finite-orbit argument establishes parabolicity. The quotient construction then supplies actual cohomology operators, and exists_eichlerShimura_heckeEquivariant uses them to prove both the away-from-level T and at-level U compatibility. This constructively discharges the earlier descent hypothesis, so the new unconditional card headline is supported.
We reviewed all 1,244 added mathematical lines and the required existing intertwining supplier. The one-file entry update imports the new wrapper and refreshes the generated card. Its public import preserves the old conditional API, all 1,198 mathematical files are unchanged from da8d283, and the 1,200-module import graph and actual index/card checks pass.
The six-proof delta is favorable. The earlier scoped audit and advisory maintenance decision remain recorded; whole-import acceptance still awaits the independent configured review and complete protected validation at this exact head. Earlier-head CI or review results do not supply that acceptance.
|
/review Please review exact current head 8b9383b under the current five project rubrics, with explicit coverage limits. This new-head request follows the author’s six-proof Hecke-descent addition and final entry refresh. Earlier request 6302060076 was ingested for da8d283 and supplies no acceptance for this revision. The follow-up scoped source audit is review 5592216989. Current-head CI and current-main qualification remain independent requirements. |
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
The four card headlines match the Lean statements and constructions; current-head CI is still running, with no reported failure. |
| Novelty | 🤔 discuss |
The good-reduction Tate-module headline substantially overlaps Tau Ceti, but its global formulation has not been established as an exact duplicate. |
| Significance | ✅ pass |
The Eichler–Shimura and Tate-module results meet the significance bar; head CI remains pending, and local validation was blocked by a Mathlib dependency-fetch HTTP 403. |
| Sources | ✅ pass |
Checked FLT source statements and prior-work attributions agree with the diff; textbook references and exhaustive historical provenance remain unverifiable. |
| Code quality (advisory) | 🤔 discuss |
Duplicated proof libraries and widespread linter suppression merit human review; the full diff was scanned with sampled detailed inspection, and current-head CI remains pending. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Both Tate-module headlines assume the p-power torsion cardinalities, explicitly disclosed in the card and supported by WeierstrassCurve.card_torsionBy_eq_sq_of_isAlgClosed. The characteristic-polynomial theorem also takes a valuation above the prime and an arithmetic Frobenius lift. Complementarity takes maps satisfying the canonical-map and conjugation identities; the PR constructs witnesses for these inputs. The new headline constructs the descended Hecke operators rather than requiring descent as a hypothesis. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | arithmetic geometry and modular forms |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: For nonzero levels and weights at least two, the code constructs the Hecke-equivariant decomposition and establishes canonical complementarity, while the Tate-module results apply to integral models at primes away from their discriminant and p (complete diff scanned; detailed audit focused on headlines, definitions, and witness/descent constructions; no local build because dependencies are absent).
Develops parabolic cohomology and Hecke actions through the Eichler–Shimura decomposition, alongside Frobenius characteristic-polynomial and good-prime unramifiedness theorems for elliptic-curve Tate modules.
Novelty findings (1)
- partial-overlap —
LeanPool/FLTEichlerShimura/Theorems/Thm_WeierstrassCurve_tateModuleRep_isUnramifiedAt_of_isGoodPrimeFor.lean:211
This headline concludes((W.map (Int.castRingHom ℚ)).tateModuleRep p hcard).IsUnramifiedAt qunder good reduction andq ≠ p. Tau Ceti already proves trivial inertia action on Tate modules at good reduction over nonarchimedean local fields. The global formulation over ℚ using valuation subrings is distinct; whether it warrants a parallel headline requires a maintainer decision, since a formal subsumption has not been verified.
Evidence: WeierstrassCurve.tateModuleGaloisRepresentation_eq_one_of_mem_inertiaSubgroup proves that every inertia element acts identically on the Tate module when the curve has an integral model with unit discriminant over a nonarchimedean local field and the coefficient prime is nonzero in its residue field: declaration and hypotheses.
Code quality findings (2)
- duplicate-definition —
LeanPool/FLTEichlerShimura/Theorems/Thm_HeckeEis_coeffHeckeFun_mem_coeffCocycles.lean:68
This module and Thm_HeckeEis_coeffHeckeFun_mem_coeffCoboundaries.lean contain an identical 132-line Sh2 library, although each exports a different endpoint. The pattern extends throughout the extraction: lSpaceShiftEquiv has 16 identical copies, finrank_adeleBddSup_quotient has 15, and roots_prime_at_slot_nodup has two repeated variants with 19 and 6 copies. Maintaining separate proofs multiplies Mathlib migration and repair work. Extract shared helper modules and import them from the endpoints.
Evidence: The identical blocks occupy lines 68–199 here and 69–200 in Thm_HeckeEis_coeffHeckeFun_mem_coeffCoboundaries.lean, including:
include ha in
theorem mem_coeffCocycles {z : Gamma0 N → V} (hz : z ∈ coeffCocycles ρ) :
coeffHeckeFun N ℓ ρ a z ∈ coeffCocycles ρ := by
let := (heckeUpper N ℓ).fintypeQuotientOfFiniteIndex
The repeated rational-function helper begins at Thm_AlgebraicCurve_RationalFunctionField_ord_X_nonneg_of_ne_placeInfty.lean:375:
def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
{Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
LSpace D ≃ₗ[K] LSpace (D + Dg) where
- linter-suppression —
LeanPool/FLTEichlerShimura/Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:57
The PR introduces 82 active unused-variable suppressions across 52 files, frequently covering whole proof sections. These disable feedback that would otherwise expose unused binders and proof residue during maintenance. Restore the checks and address individual unused variables instead of suppressing their detection across these libraries.
Evidence:set_option linter.unusedVariables falseappears here at line 57, in Theorems/Thm_AlgebraicCurve_tateAgreement.lean at lines 1717, 1864, 2002, 2271, 2340, 2535, 3214, and 3506, and in Theorems/Thm_ModularCurve_LevelN_exists_place_ord_neg_forall_smul_eq.lean at line 69, all under LeanPool/FLTEichlerShimura/. The same active suppression occurs across the algebraic-curve, modular-curve, period, and isogeny proof sections.
Tokens: 7,588,708 in / 52,008 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $31.1350 (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
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head 8b9383bc75adcdca8e3bdb81567651dbfd7bbfcb.
Changes are required under the existing quality rules. I independently checked the complete Git blobs of the 52 affected files and confirmed 82 active set_option linter.unusedVariables false commands: 80 section-scoped commands and two command-local wrappers. These are active code, not comments or strings. Examples include Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:57 and Theorems/Thm_WeierstrassCurve_exists_velu2FunctionFieldHom_restrictAlong_placeOfPoint_veluPointMap2.lean:703, under LeanPool/FLTEichlerShimura/.
The same 52 files contain 76 additional active option commands, including maxHeartbeats, synthInstance.maxHeartbeats and backward.isDefEq.respectTransparency.types. Current .github/CODE_QUALITY.md:39–40 and python/lean_pool/quality.py forbid active set_option commands; CONTRIBUTING.md also prohibits adding linter waivers. This is an existing deterministic gate, independent of the advisory 2/5 quality assessment.
Please remove forbidden option commands throughout the import and fix the actual unused-binder/elaboration diagnostics under the unchanged checks. Preserve the mathematical statements, assumptions, proof arguments, public named-argument API and source credits. The affected scopes span 82,507 lines, so deleting the 82 suppression lines alone does not establish a warning-free repair. Validate the repaired exact head with the normal build, lint, style and quality checks.
The favorable scoped review of the six new Hecke descent proofs remains valid at this head. Whole-import acceptance remains pending; no waiver or new benchmark is being requested.
|
CI follow-up for The complete build-step log contains 137 distinct warning sites across 82 files:
Lint, text-style lint and repository quality checks were subsequently skipped, so those gates remain unvalidated. Please include these warning-cleanliness repairs alongside the existing request to remove 82 unused-variable suppressions across 52 files. Preserve mathematical statements, assumptions and the normal limits/checks while repairing the code. The existing changes request remains in force. |
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 115,427,852 maxHeartbeats units across 1143 valid files (395,707 added LOC). Sum of Count-heartbeats wall-clock total: 13909.24 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.FLTEichlerShimura.Definitions.Defs_WeierstrassCurve_veluSharedLibrary |
117.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateAgreement |
102.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_exists_intermediateField_countable_map_eq_and_finrankAlong_eq |
99.00 s |
LeanPool.FLTEichlerShimura.Definitions.Def_ModularCurve_CharLFrobeniusGeomLevel |
97.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateTraceCompat_of_isSeparable |
94.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WLight_exists_levelFraction_of_stable_family |
93.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateChainRule |
82.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_Affine_exists_intermediateField_countable_map_eq_of_isAddCyclic_ker_pointMapOfPushforward |
82.00 s |
LeanPool.FLTEichlerShimura.Definitions.Defs_IsogenyBaseChange_sharedLibrary |
79.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_residueTheoremK_ratFunc_of_isAlgClosed |
70.00 s |
LeanPool.FLTEichlerShimura.Definitions.Defs_modularFunctionField_sharedLibrary |
68.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_ModularCurve_exists_transcendental_finiteDimensional_qExpFunctionFieldC_residueField |
68.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 1207 files; the per-file table shows only the 315 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
|
I have pushed fixes for the 82 unused-variable warnings; and I removed one of the two elliptic-curve "main results" (unramifiedness of the Tate module), since it overlaps somewhat with existing results in Tau Ceti, + is subsumed by the other, much more important elliptic-curve result here (computing char poly of Frobenius). |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head 5b7008d795c9c6733aa878083f54038cc4d6de23 and the complete 56-file follow-up.
The 82 linter.unusedVariables false commands and one other option command were removed; no option command was added. The YAML also genuinely withdraws unramifiedness as a separate headline. The remaining Eichler–Shimura, complementarity and Frobenius results remain substantial within the scoped mathematical review.
Changes are still required under the existing deterministic gates:
- A comment/string-aware scan of all 1,200 current Lean source files finds 1,065 active
set_optioncommands in 949 files. This includes 946backward.isDefEq.respectTransparency.types, 77synthInstance.maxHeartbeatsand 30maxHeartbeatscommands. For example,Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:51,55retains heartbeat and transparency overrides. The original 52-file review scope alone still contains 76 option commands. Remove forbidden overrides throughout the import and repair the underlying elaboration/resource issues under the unchanged settings. - The same checker also rejects
modifyScopeinDefinitions/Def_P2M_Util.lean:90and the remaining@[nolint unusedArguments]inTheorems/Thm_ModularCurve_LevelN_exists_linearMap_regularDifferentials_mdifferentiable.lean:363. Replace the namespace-routing mechanism with permitted source constructs and fix the unused arguments without a waiver. LeanPool/FLTEichlerShimura.lean:20still advertises the withdrawn unramifiedness headline in its generated project card. Regenerate that card from the updated YAML, preserving the public imports and source attribution.
Paths above are under LeanPool/FLTEichlerShimura/ unless fully qualified. These source requirements are independent of the advisory quality score. The cleanup spans 949 modules, so deleting option lines alone is not a validated repair: preserve the mathematics and pass the normal warning-free build, lint, style and quality checks on the repaired exact head. Current-head configured review and protected queue validation remain separate requirements.
|
CI update for The current head has 133 distinct warning locations in 80 files:
Please repair the warnings in the Lean code under the existing contribution rules. Lint, text-style and repository-quality steps were skipped after this failure, so they still need successful execution. The current Source changes-requested review and its remaining cleanup requirements remain in effect. |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed exact head 6edd1119c65013bb9e25cefef2b23cb5d497594a and authenticated the complete 960-file, 1,778-hunk follow-up against the previous head.
The generated project card now agrees with the three YAML headlines, the old nolint waiver is removed, and most option overrides are gone. Those previous findings are resolved or reduced; the old CI failure and old 1,065-option count are not evidence about this revision.
Two current quality requirements still need repair:
- A comment/string-aware scan of all 1,200 current Lean files finds 104 active
set_optioncommands across 64 files: 29maxHeartbeatsand 75synthInstance.maxHeartbeatsoverrides. The existing policy forbids these, including command-localinforms. Examples includeDefinitions/Defs_IsogenyEndDatum_sharedLibrary.lean:51(800000) andTheorems/Thm_AlgebraicCurve_Divisor_degree_le_finrank_adjoin_of_eq_max_neg_ord.lean:61(8000000). Remove the overrides and repair the affected proofs under the unchanged repository defaults, preserving their statements and assumptions. Definitions/Def_P2M_Util.lean:48still callsmodifyScope. The current quality checker explicitly rejects that token and its compiled constant, even though this helper changes namespace openings. Express the opening/scoped/hiding behavior through permitted commands or syntax expansion; do not rename, wrap or waive the forbidden primitive.
Paths above are under LeanPool/FLTEichlerShimura/. This remains a substantial defaults-preserving repair across 64 files, rather than a validated bulk deletion. The inspected mathematical changes were favorable, but I have not approved every nonmechanical proof change or the whole import. The new seven-shard CI run is separate and was still running at inspection; normal exact-head build, lint, style, quality, configured review and protected integration requirements remain.
|
CI follow-up for Shard 00 and the assembly job both report completed compilation, then reject the same 85 distinct warnings: 49 unscoped-option warnings, 35 heartbeat-justification warnings, and one line-length warning. Lint, text-style lint and repository quality checks were subsequently skipped. The existing source request still applies to all 104 option overrides and the |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "32e287344f0b7026e12a2a138c207122a7bd129d",
"summary": "The scope-helper repair uses native rooted open/open scoped elaboration, and the update adds five mathematical interface modules. Large code-quality repairs remain before this import is acceptable.",
"verdict": "request_changes",
"findings": [
{
"priority": "P1",
"file": "LeanPool/FLTEichlerShimura/Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean",
"line": 51,
"title": "Remove the remaining content set_option commands",
"body": "This current file still contains set_option maxHeartbeats 800000. The complete new-head tree comparison preserves all 104 previously identified option commands in 64 files; none of those files changed in this update. CODE_QUALITY.md forbids content set_option commands. Refactor the affected proofs to work under ordinary repository settings while preserving their statements and hypotheses. Scoping or documenting the same overrides does not satisfy that rule."
},
{
"priority": "P2",
"file": "LeanPool/FLTEichlerShimura/Theorems/Thm_ModularCurve_exists_modularForm_eventuallyEq_div_of_meromorphic_of_finiteIndex.lean",
"line": 1,
"title": "Add the required standard file header",
"body": "This new module begins with a provenance/license block instead of the required four-line Copyright/License/Authors header. Add the standard header while retaining the existing provenance and attribution below it; check the utility module's existing header form too."
}
],
"resolved_findings": [
"The new P2M scope utility removes modifyScope and activateScoped in favor of native open/open scoped commands; the previous forbidden-scope-API finding is resolved at this head."
],
"mathematics": "The five new mathematical modules (1,481 lines) and their card descriptions were reviewed, including the pole-clearing quotient construction, Fricke-fraction bridge, function-field presentation, Riemann–Roch wrapper and transcendental-j isogeny result. No new mathematical defect or card mismatch was identified in that scope. In particular, the isogeny claim explicitly concerns endomorphisms represented by IsogenyEndDatum. This is a scoped assessment, not approval of every historical module in the import.",
"validation": {
"source": "All nine changed/new full file bodies are authenticated to their Git blobs. Reconstructing the complete 1,206-leaf current import from the previous tree verifies all 1,197 other leaves unchanged.",
"CI": "Current-head CI is still running. The previous head's CI failure is historical and is not used as the current result."
},
"generator_clarification": "The current card generator emits Main declarations on one line. The facade matches that generated contract; preserve generated-card consistency when addressing any actual style diagnostics.",
"marker": "permanent-review-source:895:32e287344f0b7026e12a2a138c207122a7bd129d"
}
|
CI follow-up for The assembly index check passed. Lint, text style and repository quality checks were skipped after the build stage failed; the required Build project check failed. The current source change request remains: repair the 104 resource overrides through default-preserving proof changes, together with the requested header cleanup. Also shorten the facade metadata line while preserving its declarations, card metadata and generated-index consistency. Adding scopes or explanation comments alone does not resolve the source request. The repaired macro and generator-produced facade remain acknowledged. |
|
Want your agent to iterate on Greptile's feedback? Try greploops. |
| **Where it is used.** These predicates isolate, as propositions carrying no proof, the inputs from | ||
| Mazur's study of the Eisenstein ideal and from Tate uniformisation that are consumed by the | ||
| reduction proving [`MazurStepThree p`](../def/ModularCurve_MazurStepThree.html#L8): the finiteness |
There was a problem hiding this comment.
This paragraph still says the predicates are consumed by a reduction proving MazurStepThree p, but this update deletes the only definition of MazurStepThree. Readers following the link reach removed material.
This is non-blocking. Update the paragraph to describe the retained predicates and clarify that their former consumer is not included.
Extracting a chunk of material from the Claude formalization of Fermat's Last Theorem (which is Apache-2.0 licensed), with the intention to use it as the basis for a subsequent formalization of p-adic modular symbols following Mazur-Tate-Teitelbaum.