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. [Low impact] No blocking issue was established in the recent edits, but this limited review does not establish whole-project merge readiness. Findings
SummaryThe PR imports Eichler–Shimura material and supporting results from the FLT formalization. Since the previous review, six documentation edits clarify textbook comparisons without changing declarations or proofs.
Reviews (14) · Last reviewed commit: "Correct constant-extension and elliptic-..." · 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 six headlines match the inspected Lean contracts; current-head CI remains pending, the reported declaration-scanner defect reproduces, and local Lean validation was blocked by a Mathlib-fetch HTTP 403. |
| Novelty | ✅ pass |
No duplicate of the six headlines was established in the inspected Mathlib, Tau Ceti, or pool declarations; exhaustive Tau Ceti comparison remains unverifiable, and current-head CI remains pending. |
| Significance | ✅ pass |
The completed structural results meet the research-level significance bar; current-head CI remains pending, and no local build was run. |
| Sources | ✅ pass |
Full-text scanning and comparison with the cited repository support the headline citations and attribution; the earlier citation errors are corrected, some textbook and historical provenance checks remain unverifiable, and exact-head CI is pending. |
| Code quality (advisory) | 🤔 discuss |
Repeated proof libraries and unused public bundles warrant human review; coverage was full-diff scanning with targeted source reading, local Lean validation was blocked by a Mathlib HTTP403, current-head CI is unfinished, and an earlier run failed repository quality checks. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The Frobenius theorem takes the explicitly disclosed p-power torsion cardinalities, a valuation over the good prime, and an arithmetic Frobenius lift; the torsion-count theorem is present separately. The endomorphism headline quantifies over the disclosed IsogenyEndDatum, while its point/place correspondence, Abel theorem, and norm formula are constructed. Hecke descent and Fricke generation are proved rather than supplied as hypotheses. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | arithmetic geometry |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The Lean establishes Hecke-equivariant Eichler–Shimura for positive levels and weights at least two, Frobenius characteristic polynomials for integral models over ℚ, integer multiplication for the specified isogeny data, both function-field models, and the genus formula for levels at least five; coverage comprised complete-diff scanning and detailed inspection of these interfaces and key dependencies.
The Lean develops Hecke-equivariant Eichler–Shimura theory, explicit modular-curve function fields and genus formulas, and Frobenius characteristic polynomials on elliptic-curve Tate modules under the stated torsion-cardinality hypothesis.
Code quality findings (2)
- duplicate-definition —
LeanPool/FLTEichlerShimura/Theorems/Thm_AlgebraicCurve_finiteDimensional_lSpace.lean:257
Substantial helper proofs are copied across endpoint modules. The 60-line finrank_adeleBdd_quotient proof is byte-identical in this module, both indexOfSpecialty endpoints, functionFieldRiemannRoch_of_residueTheoremK_of_isAlgClosed, and both RationalFunctionField_stichtenothGenusExists endpoints; the 110-line adeleBddQuotSingleEquivResidueField also repeats across these six modules. The same pattern affects hall_all across exists_phiIrreducible, finrank_adjoin_jqN_eq_dedekindPsi, functionFieldGeneration, modularFunctionField_eq_full, and relfinrank_full_eq_dedekindPsi, and finiteDimensional_restrictScalarsQuot_pow across tateAgreement, tateChainRule, tateCommFinite, and tateTraceCompat_of_isSeparable. Extract shared helper modules so fixes and Mathlib migrations require one repair per argument.
Evidence: def adeleBddQuotSingleEquivResidueField (D : Divisor K F) (P : Place K F) :
(adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
≃ₗ[K] P.ResidueField := by
classical
theorem finrank_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) ∧
(finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
= Divisor.degree D₂ - Divisor.degree D₁ := by
classical
private theorem hall_all : ∀ N : ℕ, N ≠ 0 → Hall N := by
intro N
induction N using Nat.strong_induction_on with
theorem finiteDimensional_restrictScalarsQuot_pow [u.FiniteResidue]
(hCot : KwF4gRRTateDVRCotangentKFinite K L)
(πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
FiniteDimensional K (u.adicCompletionIntegers ⧸
(Ideal.span {πh ^ M} : Ideal u.adicCompletionIntegers).restrictScalars K) := by
induction M with
- unused-structure —
LeanPool/FLTEichlerShimura/Definitions/Def_HeckeGalois_EichlerShimura.lean:237
MultiplicityOneData has no construction or consumer in the retained Lean code. The same holds for IsKummerGenerator at LeanPool/FLTEichlerShimura/Definitions/Def_ModularCurve_IgusaFunctionField.lean:112 and W4Conclusions at LeanPool/FLTEichlerShimura/Definitions/Def_ModularCurve_TatePoint.lean:143: their names occur only in declarations and comments. These public interfaces add maintenance obligations without exercising their design. Trim them from the extraction or introduce them alongside their consumers.
Evidence: structure MultiplicityOneData (𝔪 : Ideal HeckeAlg) : Prop where
isMaximal : 𝔪.IsMaximal
resChar : (p : HeckeAlg) ∈ 𝔪
finrank_two : Module.finrank (HeckeAlg ⧸ 𝔪) (heckeTorsion J 𝔪) = 2
structure IsKummerGenerator (n : ℕ) (K₀ : IntermediateField κ Ω) (a : Ω) : Prop where
pos : 0 < n
ne_zero : a ≠ 0
pow_mem : a ^ n ∈ K₀
structure W4Conclusions (data : ModularPolynomialData p) : Prop where
oddVeluSet : ∀ i, (basePoint K p).IsOddVeluSet (veluSlotSet i)
slotCurve_succ : ∀ b : Fin p,
((tateLaurent K).map (qTwist (ζ ^ (b : ℕ)))).j = PhiGen.conj p ζ b.succ
slotCurve_zero : ((tateLaurent K).map (qExpand K (p * p))).j = PhiGen.conj p ζ 0
Tokens: 9,594,758 in / 64,342 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $39.3442 (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,860 maxHeartbeats units across 1143 valid files (395,718 added LOC). Sum of Count-heartbeats wall-clock total: 17906.20 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 |
138.00 s |
LeanPool.FLTEichlerShimura.Definitions.Def_ModularCurve_CharLFrobeniusGeomLevel |
136.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_exists_intermediateField_countable_map_eq_and_finrankAlong_eq |
132.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WLight_exists_levelFraction_of_stable_family |
122.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateAgreement |
115.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateTraceCompat_of_isSeparable |
113.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateChainRule |
103.00 s |
LeanPool.FLTEichlerShimura.Definitions.Defs_IsogenyBaseChange_sharedLibrary |
100.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_Affine_exists_intermediateField_countable_map_eq_of_isAddCyclic_ker_pointMapOfPushforward |
99.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_ModularCurve_exists_transcendental_finiteDimensional_qExpFunctionFieldC_residueField |
97.00 s |
LeanPool.FLTEichlerShimura.Definitions.Defs_modularFunctionField_sharedLibrary |
89.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_residueTheoremK_ratFunc_of_isAlgClosed |
86.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.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent Source review at eae921e: approved.
The earlier changes request is resolved: the current source removes the 104 resource overrides and the option-API routing issue, and repairs the file headers and generated Main declarations line. I authenticated the complete current file set and old-to-current diff, with detailed review of changed contracts and model definitions, all four new shared libraries, and the six advertised result closures. A second reviewer checked the six headline interfaces and their stated scope.
The card accurately discloses the Tate torsion-cardinality premise and restricts the transcendental-j result to endomorphisms induced by IsogenyEndDatum. The Eichler–Shimura endpoint constructs the descended Hecke operators; the function-field and genus results use the concrete models and field/level assumptions described by the card. Fresh comparisons with actual Mathlib, Tau Ceti and pool contracts acknowledge the existing local Frobenius/inertia work and identify the additional global characteristic-polynomial, cohomological and function-field results.
One optional documentation cleanup remains: the MazurStepThreeInputs paragraph still refers to the removed MazurStepThree consumer. Describing it as retained vocabulary would avoid that stale reference.
This is a source assessment, not an independent reproof of every imported line or a compilation/performance certificate. Current-head configured review and all applicable CI, current-main and protected native-queue requirements remain separate.
|
/review Please evaluate exact head eae921e under all five current project rubrics. Independent current-source review is 5733196567: the old resource-option/header findings are resolved, with the six advertised result scopes and actual nearest prior contracts reviewed afresh. The authored run still fails repository quality because audit results are missing; that technical check and all other current-head/current-main/protected native-queue gates remain required. This is a source-review request, with no merge or auto-merge action. |
|
CI follow-up for Repository quality reported 15,027 missing axiom-audit results across 1,053 files. These messages do not establish forbidden axioms. There is a reproducible checker defect: its textual declaration scanner ignores The current source approval stands, and the required quality check remains failed. Audit-tooling repair and successful revalidation are still needed. The separately reviewed compiled-declaration auditor in #719 addresses these failure classes structurally; its existing authorization and validation requirements remain in force. |
Correct Stichtenoth 3.6.3(d) references and distinguish the current constant-extension hypotheses. Describe the cyclic-kernel argument as a consequence of the stated endomorphism hypothesis, with Silverman III.4.12 cited for quotient/isogeny background. Documentation only; all mathematical statements, proofs, imports and quality gates are unchanged.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Source continuation: APPROVE at bd4ffd887db8d78e84a219970c87817396a30b05 after fixing the two configured citation findings.
The findings were valid. Stichtenoth, p. 114, Theorem 3.6.3(d), gives the Riemann–Roch dimension/basis statement for algebraic constant extensions; part (a) concerns unramifiedness. Five related comments now cite (d) and explicitly distinguish these declarations’ generation/place-lifting hypotheses and broader constant-extension scope.
Silverman, p. 74, III.4.12, supplies quotient/isogeny background. The sixth comment now describes the cyclic-subgroup injectivity argument as proved here using hEnd, the constructed quotient maps, and their kernel/norm properties. It no longer attributes a rank-one Hom statement to that proposition.
The maintainer-enabled fork received one normal commit containing only those six documentation changes. The complete hosted patch reconstructs all six prepared files exactly; replacing the new paragraphs by the old ones recovers every original byte. Independent verification also reproduces the full commit tree. The current mathematical statements, proofs, hypotheses, imports, card and gates are unchanged, so the detailed source review remains applicable with these citation repairs resolved. The duplicate-helper and unused-interface observations remain advisory maintenance follow-ups.
The failed EAE quality run and scanner diagnosis remain recorded; this commit does not repair that auditor. The new head needs its own configured review and applicable hosted checks. Current-main qualification and normal protected native-queue requirements remain outstanding.
|
/review |
|
Current-head CI diagnosis for A read-only replay of the checker used by this exact run reproduces a concrete scanner bug in That explains these three targets, not all missing results. Module visibility and preservation of actual Lean lookup diagnostics also need checking. No checker, theorem, gate or cache was changed, and no retry was started. The next repair belongs in the audit tooling, with complete coverage and the existing axiom policy preserved. |
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.