WIP: import Stafford 3.8

[Vilin97]

Imports Stafford 3.8 from itpplasma/stafford38-formal.

Formalizes Stafford’s Conjecture 3.8 over every characteristic-zero field and every Weyl-algebra rank: each nonzero d admits F, R, and S with 1 = d*R + F*d*S. It also proves an exact Bernstein-degree fixed-source strengthening and derived localization, adjoint, and evolutionary results.

Preserves all 346 production and supporting modules plus the project entry point, including the completed solution bridges. Duplicate open comparator specifications and documentation-only blueprint modules are recorded outside the proof import. Includes the pinned Apache-2.0 AlgebraicAnalysis dependency at 4aae47967f6ba02ffe2f639ab06564c9a9d1ecc8, its retained NOTICE and detailed provenance links. Original attribution and the newly supplied dependency notice remain intact.

The pre-migration checkpoint passed a warning-free complete build, all 15 declaration linters, style, index, metadata, recursive size/static checks and compiled axiom/environment audits. The current module-system migration exports the data interfaces used by public canonical complexes, Ore stages and completion coordinates, and keeps private proof terms inside proposition-valued proof blocks.

Current checkpoint b909115d6 preserves all 347 files and concurrent attribution/main updates. The latest aggregate build at bafeb85cc compiled the previous matrix proof repair and reached five subsequent module-visibility failures. Those constructors now pass private proofs in explicit proposition-valued arguments; two local instance registrations remain private, and the concrete two-jet data used by public statements has a documented public interface. Mathematical data and theorem statements are unchanged.

Recursive source, header, file-size and proof-size checks pass with zero findings. These five repairs await compiled verification under the shared bounded-build queue. Final declaration/style/index/metadata/axiom/environment checks and aggregate CI are still pending at this checkpoint. The existing independent review passes faithfulness, novelty, significance and sources, with advisory code-quality discussion; it is not an approval of this new head. No gates, waivers or proof budgets changed.

Part of the requested 42-project import batch. The existing ready-for-review state is preserved. Do not merge.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head 987700c67ff565d8a54f29690573d643dc319e0b for this draft pooled-project/content import, WIP: import Stafford 3.8. The changed tree is a substantial source import (including LeanPool/Stafford38.lean) with the pinned upstream source, project metadata, and generated index present. Observed exact-head required checks have no failures; profile evidence: no proof-profile comment was posted for this exact head.

No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval.

[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 algebraic analysis.

No outstanding review finding was identified, but the PR should not merge before current-head compilation and final audits pass.

Summary

Imports the Stafford 3.8 formalization, including the universal Weyl-algebra identity, a fixed-source strengthening, supporting modules, and dependency provenance.

• The Stafford files have not changed since the previous review. The changes since then come from a concurrent main-branch merge.
• All three previous Greptile threads are resolved; no new finding was established.
• Current-head compilation and the final audits remain pending.

_{Reviews (23) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

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

Reviewed head: b862ca25b4ba9059ba21a251744d534fe3b7d19f

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

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Both headline results match the card, with no undisclosed substantive assumptions.
Novelty	✅ pass	Direct searches of the pinned Mathlib source and existing pool found no declaration subsuming either headline result.
Significance	✅ pass	The universal Stafford identity and exact Bernstein-degree strengthening anchor a substantial research-level development; no generated-bulk concern was identified.
Sources	✅ pass	Stafford’s Conjecture 3.8, p. 438 supports the stated identity; stronger project results are explicitly labelled, supporting citations are consistent, and upstream formalizations are credited.
Code quality (advisory)	🤔 discuss	Thirty tactic-suggestion commands, a dead central interface, and unnecessarily strong reusable assumptions leave material cleanup debt for a maintainer.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The headlines require a characteristic-zero field and nonzero d; the fixed-source form uses positive rank. Intermediate support-vanishing and bundled paper inputs are discharged by proved theorems.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	research
Branch	noncommutative algebra
Mode	theory_building
Code quality	2 / 5

Statement check: The Lean proves the identity over every characteristic-zero field and every rank, and for positive rank proves the strengthening F = ell^bernsteinDegree(d), where ell is a linear symplectic coordinate chosen for d.

The project addresses Stafford’s named Weyl-algebra generator conjecture, discussed in Bellamy’s survey, through substantial PBW, characteristic-support, conormal-geometry, and localization theory.

Code quality findings (4)

• agent-slop — LeanPool/Stafford38/Stafford38/Characteristic/SymplecticCompletion.lean:79
  There are 30 active simp? commands across the imported production modules (including seven in SymplecticCompletion and occurrences in MonicNormalization, RightDivision, CanonicalTotalGradedActionCompatibility, and others). These are interactive suggestion tactics left in library proofs, so the source emits search advice and does not record a deliberate simp set. Replace each with an explicit simp/simpa proof (or remove it if redundant) and keep the required rewrite lemmas visible.
  Evidence: theorem phasePairing_add_left {n : ℕ} (u v w : PhaseVar n → k) : followed by simp? [phasePairing] at line 79; other active additions include simp? at hdc in Weyl/MonicNormalization.lean:133 and simp? [commutatorDerivation] in AlgebraicAnalysis/Ore/RightDivision.lean:770.
• unused-definition — LeanPool/Stafford38/Stafford38/CanonicalSupportVanishingReduction.lean:57
CanonicalCoordinateCancellation is declared as a universal interface but has no consumer anywhere in the PR; the closure actually constructs and passes CanonicalStrictUnitCoordinatePreimage instead. Leaving an unconnected public wrapper makes the intended proof boundary unclear. Remove it or wire it into the assembly if it is meant to be the canonical interface.
  Evidence: Lines 57–61 define CanonicalCoordinateCancellation with conclusion CoordinateCancellation k n N d. The actual closure input is let hunit : CanonicalSupportVanishingReduction.CanonicalStrictUnitCoordinatePreimage := by ... in LeanPool/Stafford38/Stafford38/FoundationClosure.lean:55.
• overstrong-typeclass — LeanPool/Stafford38/AlgebraicAnalysis/Ore/RightDivision.lean:815
pRightMulLinear and pRightMulRange require [Field k], although their bodies only use the algebra scalar action, addition, and associativity. This needlessly prevents the reusable right-multiplication API from working over general commutative-semiring scalars (and semiring coefficient rings); keep field hypotheses on the later p-free theorems that need them, and weaken these definitions and their membership lemma.
  Evidence: def pRightMulLinear {k A : Type*} [Field k] [Ring A] [Algebra k A] (p : A) : A →ₗ[k] A has map_add' ... rw [add_mul] and map_smul' ... [Algebra.smul_def] ... rw [mul_assoc]; pRightMulRange repeats the same [Field k] signature.
• namespace-collision — LeanPool/Stafford38/AlgebraicAnalysis/RingTheory/TwoGeneratorIdentity.lean:26
  The vendored AlgebraicAnalysis layer exports reusable declarations directly in the global AlgebraicAnalysis namespace. If a downstream pool project imports both this tree and the separately distributed AlgebraicAnalysis library named in the project notice, matching declarations can collide and the import boundary becomes order-dependent. Put the vendored copy under a Stafford38-specific namespace or make the pinned library the single shared dependency.
  Evidence: namespace AlgebraicAnalysis at line 26 and def TwoGeneratorIdentity (R : Type u) [Ring R] : Prop := ... at lines 30–33; the project root imports this vendored tree as LeanPool.Stafford38.AlgebraicAnalysis.

---

Tokens: 11,047,594 in / 54,455 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $225.0360 (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.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 8b2c82c6d74cde28f3205168c2101bedb383bd07.

The exact-head Build pool/project checks fail because LeanPool.Stafford38 is not module-compatible. Port the imported closure and regenerate the index, then rerun full CI. The prior review also identified diagnostic commands, a dead interface, and unnecessarily strong assumptions that should be removed or justified.

Acceptance condition: the named defects are repaired on a new head and all required protected checks are green. Do not change repository policy or add waivers.

[Vilin97]

Changes requested by automated review

Reviewed head 31d203145960b9d3b611733950218ff7b62af2b6. Substantial full characteristic-zero nonzero-rank Weyl-algebra generation theorem.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.Stafford38 from `module`
   

   The file/dependency audit finds 347 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.

Review coverage: complete changed-file inventory and full diff retained; 347 changed project files, 67,745 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: Noncommutative algebra, Ore and Bernstein-degree 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.

[Vilin97]

Source and static review of 19ecd98dda79c45817cec97f1fdabf2563344c8b:

• Replaced all 30 production simp? commands with explicit simplification sets recorded in existing compiler logs. The goals and subsequent proof steps are unchanged.
• Removed the unused CanonicalCoordinateCancellation wrapper; the actual CanonicalStrictUnitCoordinatePreimage interface remains.
• Kept the three right-multiplication helper names, reused LinearMap.mulRight, and generalized only those helpers to commutative-semiring scalars and semiring coefficients. Later field-dependent theorem assumptions are unchanged.

Independent source review passed. Local checks passed for whitespace, headers, forbidden text, file sizes, project metadata/card consistency, and the actual mk_all --module --check. All 218 current-main cards plus this project remain present, and the dependency pin, license, and verbatim notices are preserved.

This is a source/static recommendation for the cleanup, not full merge approval. Fresh proof compilation and required CI remain pending while the existing module-port work continues; no cold duplicate project build was launched. The vendored global namespace is retained deliberately: the current dependency manifest contains no parallel AlgebraicAnalysis package. Its possible collision with a separately imported downstream copy remains a conditional integration concern, accepted here as nonblocking rather than claimed fixed.

[Vilin97]

Scoped validation update for 359ae1104b48a94572163c0142debd062a760094: the modified AlgebraicAnalysis.Ore.RightDivision module now compiles locally with the pinned Lean/Mathlib configuration, exit 0 and no warnings. This validates the three named right-multiplication helpers using the canonical LinearMap.mulRight map in the generalized semiring context. The source checked is byte-identical at this head.

The incoming commit intentionally restores the public CanonicalCoordinateCancellation wrapper; I accept that as a nonblocking compatibility choice and have preserved it. The 30 logged explicit simp replacements and helper reuse remain intact. This is a focused compiler result, not a claim that the full project has built: current required CI and the remaining advisory disposition still govern final acceptance.

[Vilin97]

Reviewed incoming 50b7b8e4 and published its attribution-only main refresh at ee569cd7a1e92dd42eb06a03b9b1868908b80734.

The incoming two-file patch addresses the current build failures: scalarEnd is now a documented public abbreviation, so the public residual-support statement can refer to it; the Weyl commutator proof establishes equality of the shifted matrix entries and applies congrArg to the algebra map, avoiding invalid rfl steps for mapped zero and one. I read the complete patch. The mathematical statements and scalar map are preserved.

The refresh adds only main's NOTICE and NOTICE.extra.yml changes. All incoming Lean source and project cards are byte-identical; the actual pinned mk_all --module --check passes. The earlier generic-helper and simplifier repairs remain, and the intentionally restored CanonicalCoordinateCancellation API is preserved. RightDivision's completed single-file, warning-free check still applies because that source is unchanged.

Fresh CI must compile the two incoming repaired modules and certify the full project before merge. This review does not claim those fresh compiled checks have passed.

[Vilin97]

Reviewed and preserved the importer's one-line fix in oldGenerator_commutator: adding Matrix.one_apply exposes the identity-matrix entries, allowing simplification to use injectivity of Fin.succ. This addresses the two explicit unsolved entry-equality goals without changing the statement, maps, or surrounding proof. No new local compilation is claimed; the complete port still requires full CI.

Integrated current main 854da85a8bc6c9219c2c04ec9d43d4a49f43aef8 at a70cffe0bab99131e10d69b2a785950c0660f7a2. All 347 project files remain byte-identical to source commit fdea30d4965a7fdc53434246371d7b39b87fb55a; all 219 main cards and this project's card preserve their values and original payload bytes. The actual pinned mk_all --module --check passed. The subsequent main metadata update changed only NOTICE and README; all source and index bytes remained unchanged. The prior substantive review carries forward; merging remains conditional on all required checks at this exact integration head.

[Vilin97]

Changes requested by automated review

Reviewed head bafeb85cc383de6d4f0945b036d778ff0164c642.

The corrected freeWeylLinearCombination proof resolves the earlier reported error, but the exact-head Build pool log reveals further module-interface failures. Geometry/ScalarExtensionPoints.lean:308 cannot find orderDecompositionExtension; Characteristic/CanonicalTangentialPageOperators.lean:150,160 cannot find oldGenerator_mem_orderPiece; CanonicalTotalGradedBridge.lean:97,122,133 cannot find natDirectSumToNonpositive_lof. The CanonicalUnitPreimageFromInitialTop and ConcreteLocalizedTwoBlockSpecialFibre modules also fail after these interface changes.

Acceptance condition: provide the intended public imports/lemmas and repair the dependent module interfaces, then obtain a warning-free required build on the new head. Keep the substantive right-multiplication abstraction and source/license corrections already completed. Stafford's theorem is a significant, suitable result; this is a concrete build blocker, not a maintainer-policy question.

[Vilin97]

Changes requested by automated review

Reviewed b909115d64d5d0cf9410bf4f007d2bd198145a57. The Stafford characteristic/coisotropy endpoint is significant; the imported mathematical scope and source remain worth preserving.

Blocking finding: Characteristic/CanonicalLaurentSymbolControl.lean:92 cannot resolve orderDecompositionGroundExtension, followed by missing instances. ConcreteEquation33SourceMatrices.lean:559,609,618 refers to an unavailable private concreteData constant. Repair module visibility/namespace references at the public bridge and check importing consumers; the current endpoint closure does not build.

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.

[Vilin97]

Changes requested by automated review

Reconciled to exact current head e372bd9b7b4a2327e5e7753d922914179287b039. The main-branch integration leaves this project’s Lean sources byte-identical to the reviewed source; the existing substantive findings and acceptance conditions remain unresolved. The missing ground-extension order decomposition and inaccessible concreteData declarations still prevent the Stafford theorem closure from compiling.

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]

{
"reviewed_head": "e372bd9b7b4a2327e5e7753d922914179287b039",
"review_type": "focused incoming-source follow-up",
"assessment": "Read the complete six-file incoming delta and the underlying constructors/maps. The two tangential PageOperator definitions retain the same generators, degrees, right-multiplication maps, and proof arguments, now supplied directly. nonpositiveDirectSumLinearEquiv retains both maps, all assumptions, and the complete inverse proofs, using explicit proof arguments. normalForm_linearCombination now unfolds the existing linear-combination definition and Algebra.smul_def at the same equality step. concreteData exposes the identical existing abbreviation; two named local grading instances become private while retaining their bodies and local instance behavior. A project-wide name search found no external use of those two instance names. Existing mathematical endpoint types and data maps are preserved; the visibility changes are intentional.",
"scope": "Compared all own-project changes after reviewed a70cffe. All 347 project files including the umbrella remain; project card and own generated index are unchanged. This source follow-up carries forward the prior substantive review without claiming full-port validation.",
"validation": "Full incoming-diff and relevant constructor/proof-context review, project inventory/card/index comparison, and git diff --check passed. No fresh local compilation is claimed. Existing unresolved review findings and full CI, lint, and compiled trust requirements remain; this comment is not whole-project approval.",
"findings": []
}

[Vilin97]

{
"reviewed_head": "6056cd3c3da2cb69f912a986f467921d93717d22",
"review_type": "focused CI visibility and warning repair follow-up",
"assessment": "The three-file patch addresses the two root visibility failures reported by run36226818077/job108362545485. orderGradedAlgebraGroundExtensionInstance is now explicitly private and remains local, with its original type and body; its private decomposition helper is used only by that instance and one theorem proof. The matrix module removes its private duplicate concreteData alias and uses the already-imported public ConcreteLocalizedTwoBlockSpecialFibre.concreteData through D. Both aliases have exactly the same filteredQuotientTwoJetTraceData k I body and parameters, preserving the public matrix types, constructions, multiplication orientation and proof arguments. The same existing simp step loses only Nat.add_left_cancel_iff and DirectSum.of_eq_same, the two arguments reported unused by CI.",
"family_audit": "Searched all347 project files for both implicated helper families and inventoried the D-bearing exported headers. The named local instance has no other named consumer; no additional private concreteData variant remains. This intentionally changes one local instance name to private and removes one private alias; it adds no new public interface. Public mathematical statements and data remain definitionally unchanged.",
"validation": "Independent full source/context review, four scoped repository static checks (headers, forbidden text, file sizes, proof sizes), and git diff --check passed. All347 project files remain; all bytes outside the three exact replacements, the complete project registry/root index and compiler configuration are preserved. No fresh local compilation, declaration-linter, style or compiled-trust pass is claimed: the available103-module dependency cache includes legacy non-module outputs and was not reused. Fresh required CI remains necessary.",
"remaining_scope": "This is not whole-project approval. ConcreteInducedZActionIdentity remains explicitly an unproved proposition defining the source-specific bridge; this patch neither supplies that bridge nor changes the prior substantive review conditions. The author's do-not-merge instruction and existing aggregate validation/review requirements remain in force.",
"diagnostic_source": "https://github.com/Vilin97/lean-pool/actions/runs/36226818077/job/108362545485",
"findings": []
}