Repository navigation
Import brauergroup_new formalization - #88
Conversation
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 26,920 maxHeartbeats units across 25 files (3,644 added LOC). Sum of Count-heartbeats wall-clock total: 132.99 s. Repeated import cost inside Heartbeat values come from Mathlib's 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.BrauerGroupNew.ExtendScalar |
40.00 s |
LeanPool.BrauerGroupNew.BrauerGroup |
37.00 s |
LeanPool.BrauerGroupNew.Wedderburn |
15.00 s |
LeanPool.BrauerGroupNew.MatrixEquivTensor |
15.00 s |
LeanPool.BrauerGroupNew.CentralSimple |
15.00 s |
LeanPool.BrauerGroupNew.MatrixCenterEquiv |
8.40 s |
LeanPool.BrauerGroupNew.Centralizer |
6.50 s |
LeanPool.BrauerGroupNew.Subfield.Defs |
5.60 s |
LeanPool.BrauerGroupNew.TwoSidedIdeal |
4.70 s |
LeanPool.BrauerGroupNew.LemmasAboutSimpleRing |
4.60 s |
LeanPool.BrauerGroupNew.Mathlib.Algebra |
4.10 s |
LeanPool.BrauerGroupNew.FieldCat |
3.70 s |
Per-file `lean --profile` output
LeanPool/BrauerGroupNew.lean
import took 1.89s
cumulative profiling times:
elaboration 0.124ms
import 1.89s
initialization 26.9ms
interpretation 197ms
linting 0.219ms
parsing 0.0279ms
real 2.71
user 1.61
sys 1.12
LeanPool/BrauerGroupNew/BrauerGroup.lean
import took 1.85s
interpretation of elabSuppressCompilationDecl._boxed took 121ms
typeclass inference of CoeFun took 111ms
typeclass inference of CoeFun took 116ms
typeclass inference of MulActionHomClass took 229ms
interpretation of elabSuppressCompilationDecl._boxed took 216ms
interpretation of elabSuppressCompilationDecl._boxed took 239ms
simp took 232ms
simp took 357ms
typeclass inference of HMul took 126ms
typeclass inference of HMul took 122ms
tactic execution of Lean.Parser.Tactic.change took 134ms
typeclass inference of MulZeroClass took 162ms
typeclass inference of Distrib took 161ms
typeclass inference of RightDistribClass took 104ms
typeclass inference of MulZeroClass took 159ms
typeclass inference of Distrib took 160ms
typeclass inference of LeftDistribClass took 104ms
typeclass inference of MulZeroClass took 158ms
typeclass inference of Distrib took 159ms
typeclass inference of RightDistribClass took 103ms
typeclass inference of MulZeroClass took 159ms
typeclass inference of Distrib took 157ms
typeclass inference of LeftDistribClass took 102ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 180ms
interpretation of elabSuppressCompilationDecl._boxed took 247ms
type checking took 157ms
interpretation of elabSuppressCompilationDecl._boxed took 188ms
interpretation of elabSuppressCompilationDecl._boxed took 1.15s
type checking took 128ms
type checking took 209ms
tactic execution of Lean.Parser.Tactic.refine took 144ms
simp took 263ms
typeclass inference of MulZeroClass took 536ms
typeclass inference of MulZeroClass took 435ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 646ms
typeclass inference of Distrib took 532ms
typeclass inference of RightDistribClass took 404ms
simp took 1.11s
typeclass inference of MulZeroClass took 514ms
typeclass inference of MulZeroClass took 413ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 629ms
typeclass inference of Distrib took 541ms
typeclass inference of LeftDistribClass took 399ms
simp took 1.1s
simp took 586ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 133ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 482ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 437ms
simp took 111ms
type checking took 184ms
type checking took 115ms
tactic execution of Lean.Parser.Tactic.exact took 189ms
cumulative profiling times:
aesop 223ms
attribute application 12.8ms
compilation (IR) 0.299ms
compilation (LCNF base) 3.74ms
compilation (LCNF impure) 1.62ms
compilation (LCNF mono) 4.16ms
congr simp thm 47.4ms
dsimp 18.9ms
elaboration 360ms
fix level params 20.7ms
import 1.85s
initialization 26.6ms
instantiate metavars 27.9ms
interpretation 4.35s
let-to-have transformation 105ms
linting 68.9ms
norm_num 0.138ms
parsing 52.9ms
process pre-definitions 265ms
share common exprs 44.5ms
simp 4.96s
tactic execution 5.24s
type checking 3.34s
typeclass inference 25s
real 37.80
user 45.67
sys 1.25
LeanPool/BrauerGroupNew/CentralSimple.lean
import took 1.55s
typeclass inference of AddMonoidHomClass took 146ms
typeclass inference of ZeroHomClass took 215ms
simp took 103ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 165ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 189ms
tactic execution of Lean.Parser.Tactic.eqRefl took 145ms
type checking took 130ms
tactic execution of Lean.Parser.Tactic.refine took 117ms
simp took 221ms
elaboration took 201ms
typeclass inference of OneHomClass took 102ms
typeclass inference of AddHomClass took 151ms
cumulative profiling times:
aesop 35ms
attribute application 2.1ms
blocked (unaccounted) 10.2ms
compilation (IR) 0.218ms
compilation (LCNF base) 7.96ms
compilation (LCNF impure) 1.22ms
compilation (LCNF mono) 6.55ms
congr simp thm 35.1ms
dsimp 4.1ms
elaboration 551ms
fix level params 17.6ms
import 1.55s
initialization 26.6ms
instantiate metavars 23.5ms
interpretation 904ms
let-to-have transformation 0.851ms
linting 76.6ms
parsing 39.8ms
process pre-definitions 67.4ms
share common exprs 39.1ms
simp 1.22s
tactic execution 3.82s
type checking 1.13s
typeclass inference 7.09s
real 8.51
user 16.15
sys 1.09
LeanPool/BrauerGroupNew/Centralizer.lean
import took 1.28s
type checking took 287ms
cumulative profiling times:
aesop 39.2ms
attribute application 0.061ms
congr simp thm 15.4ms
elaboration 70.4ms
fix level params 3.48ms
import 1.28s
initialization 30.2ms
instantiate metavars 3.9ms
interpretation 334ms
let-to-have transformation 0.181ms
linting 7.92ms
parsing 9.35ms
process pre-definitions 6.81ms
share common exprs 7.45ms
simp 525ms
tactic execution 509ms
type checking 407ms
typeclass inference 1.13s
real 3.33
user 4.04
sys 0.87
LeanPool/BrauerGroupNew/ExtendScalar.lean
import took 1.23s
typeclass inference of MulZeroClass took 245ms
typeclass inference of MulZeroClass took 241ms
typeclass inference of HMul took 201ms
typeclass inference of NonUnitalNonAssocSemiring took 253ms
typeclass inference of NonUnitalSemiring took 214ms
typeclass inference of AddHomClass took 298ms
typeclass inference of AddHomClass took 170ms
typeclass inference of Distrib took 234ms
typeclass inference of LeftDistribClass took 182ms
typeclass inference of HMul took 198ms
typeclass inference of HMul took 192ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 141ms
typeclass inference of NonUnitalNonAssocSemiring took 238ms
typeclass inference of NonUnitalSemiring took 213ms
typeclass inference of AddHomClass took 299ms
typeclass inference of AddHomClass took 171ms
typeclass inference of Distrib took 236ms
typeclass inference of RightDistribClass took 185ms
typeclass inference of MulZeroClass took 233ms
typeclass inference of ZeroHomClass took 111ms
typeclass inference of ZeroHomClass took 107ms
typeclass inference of Distrib took 235ms
typeclass inference of RightDistribClass took 174ms
typeclass inference of AddHomClass took 166ms
typeclass inference of MulZeroClass took 234ms
typeclass inference of ZeroHomClass took 112ms
typeclass inference of ZeroHomClass took 108ms
typeclass inference of Distrib took 234ms
typeclass inference of LeftDistribClass took 175ms
typeclass inference of AddHomClass took 167ms
typeclass inference of ZeroHomClass took 111ms
typeclass inference of ZeroHomClass took 106ms
typeclass inference of AddHomClass took 170ms
typeclass inference of AddHomClass took 166ms
typeclass inference of ZeroHomClass took 110ms
typeclass inference of ZeroHomClass took 109ms
typeclass inference of AddHomClass took 170ms
typeclass inference of AddHomClass took 164ms
typeclass inference of Mul took 195ms
typeclass inference of MulHomClass took 122ms
typeclass inference of AddHomClass took 444ms
typeclass inference of ZeroHomClass took 189ms
typeclass inference of ZeroHomClass took 180ms
typeclass inference of AddHomClass took 461ms
typeclass inference of AddHomClass took 452ms
typeclass inference of ZeroHomClass took 174ms
typeclass inference of ZeroHomClass took 168ms
typeclass inference of ZeroHomClass took 173ms
typeclass inference of ZeroHomClass took 167ms
typeclass inference of AddHomClass took 442ms
typeclass inference of AddHomClass took 433ms
typeclass inference of AddHomClass took 441ms
typeclass inference of AddHomClass took 430ms
elaboration took 104ms
cumulative profiling times:
attribute application 3.68ms
compilation (IR) 0.523ms
compilation (LCNF base) 15.4ms
compilation (LCNF impure) 3.01ms
compilation (LCNF mono) 14.5ms
congr simp thm 14.7ms
elaboration 248ms
fix level params 6.4ms
import 1.23s
initialization 26.4ms
instantiate metavars 6.86ms
interpretation 294ms
let-to-have transformation 124ms
linting 10.5ms
parsing 9.45ms
process pre-definitions 91.5ms
share common exprs 12.7ms
simp 566ms
tactic execution 795ms
type checking 1.06s
typeclass inference 18.1s
real 22.20
user 22.54
sys 0.82
LeanPool/BrauerGroupNew/FieldCat.lean
import took 1.04s
cumulative profiling times:
aesop 43.3ms
attribute application 16.8ms
blocked (unaccounted) 26.7ms
compilation (IR) 0.478ms
compilation (LCNF base) 12.1ms
compilation (LCNF impure) 2.58ms
compilation (LCNF mono) 11ms
congr simp thm 3.23ms
elaboration 165ms
fix level params 0.911ms
import 1.04s
initialization 26.4ms
instantiate metavars 1.03ms
interpretation 274ms
let-to-have transformation 0.534ms
linting 11.6ms
parsing 9.14ms
process pre-definitions 15.8ms
share common exprs 2.27ms
simp 68.6ms
tactic execution 101ms
type checking 123ms
typeclass inference 327ms
real 2.46
user 2.08
sys 0.73
LeanPool/BrauerGroupNew/LemmasAboutSimpleRing.lean
import took 1.51s
cumulative profiling times:
aesop 53.5ms
attribute application 0.0226ms
congr simp thm 4.77ms
elaboration 13.3ms
fix level params 1.62ms
import 1.51s
initialization 26.4ms
instantiate metavars 2.3ms
interpretation 209ms
let-to-have transformation 0.0343ms
linting 10.2ms
parsing 5.41ms
process pre-definitions 3.35ms
share common exprs 4.26ms
simp 176ms
tactic execution 269ms
type checking 108ms
typeclass inference 1.44s
real 4.18
user 3.48
sys 0.95
LeanPool/BrauerGroupNew/Mathlib.lean
import took 1.21s
cumulative profiling times:
elaboration 0.153ms
import 1.21s
initialization 26.3ms
interpretation 118ms
linting 0.222ms
parsing 0.0266ms
real 1.89
user 1.12
sys 0.78
LeanPool/BrauerGroupNew/Mathlib/Algebra.lean
import took 1.21s
cumulative profiling times:
elaboration 0.145ms
import 1.21s
initialization 26.5ms
interpretation 118ms
linting 0.222ms
parsing 0.026ms
real 1.88
user 1.09
sys 0.81
LeanPool/BrauerGroupNew/Mathlib/Algebra/Algebra.lean
import took 1.23s
cumulative profiling times:
elaboration 0.165ms
import 1.23s
initialization 27.1ms
interpretation 125ms
linting 0.286ms
parsing 0.025ms
real 1.91
user 1.12
sys 0.81
LeanPool/BrauerGroupNew/Mathlib/Algebra/Algebra/Subalgebra.lean
import took 1.21s
cumulative profiling times:
elaboration 0.142ms
import 1.21s
initialization 26.5ms
interpretation 122ms
linting 0.237ms
parsing 0.0274ms
real 1.89
user 1.11
sys 0.80
LeanPool/BrauerGroupNew/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
import took 1.17s
cumulative profiling times:
attribute application 3.08ms
elaboration 22.9ms
fix level params 0.125ms
import 1.17s
initialization 26.6ms
instantiate metavars 0.0292ms
interpretation 125ms
let-to-have transformation 0.173ms
linting 1.88ms
parsing 0.945ms
process pre-definitions 0.287ms
share common exprs 0.29ms
type checking 6.36ms
typeclass inference 18.3ms
real 1.88
user 1.13
sys 0.79
LeanPool/BrauerGroupNew/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
import took 1.21s
cumulative profiling times:
attribute application 0.00915ms
elaboration 6.84ms
fix level params 0.218ms
import 1.21s
initialization 26.7ms
instantiate metavars 0.15ms
interpretation 130ms
let-to-have transformation 0.0176ms
linting 1.29ms
parsing 0.53ms
process pre-definitions 0.319ms
share common exprs 0.288ms
tactic execution 7ms
type checking 2.22ms
typeclass inference 9.85ms
real 1.91
user 1.15
sys 0.79
LeanPool/BrauerGroupNew/Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
import took 1.22s
cumulative profiling times:
attribute application 0.011ms
dsimp 1.64ms
elaboration 5.6ms
fix level params 0.206ms
import 1.22s
initialization 26.5ms
instantiate metavars 0.234ms
interpretation 119ms
let-to-have transformation 0.013ms
linting 0.741ms
parsing 0.467ms
process pre-definitions 0.441ms
share common exprs 0.464ms
tactic execution 6.68ms
type checking 2.94ms
typeclass inference 16.4ms
real 1.92
user 1.14
sys 0.80
LeanPool/BrauerGroupNew/Mathlib/RingTheory.lean
import took 1.09s
cumulative profiling times:
elaboration 0.171ms
import 1.09s
initialization 26.7ms
interpretation 113ms
linting 0.23ms
parsing 0.0255ms
real 1.75
user 1.02
sys 0.74
LeanPool/BrauerGroupNew/Mathlib/RingTheory/TwoSidedIdeal.lean
import took 1.1s
cumulative profiling times:
elaboration 0.14ms
import 1.1s
initialization 26.3ms
interpretation 112ms
linting 0.305ms
parsing 0.0256ms
real 1.75
user 1.04
sys 0.74
LeanPool/BrauerGroupNew/Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
import took 1.04s
cumulative profiling times:
attribute application 0.0106ms
congr simp thm 0.693ms
elaboration 4.95ms
fix level params 0.152ms
import 1.04s
initialization 26.1ms
instantiate metavars 0.123ms
interpretation 123ms
let-to-have transformation 0.0133ms
linting 0.948ms
parsing 0.719ms
process pre-definitions 0.474ms
share common exprs 0.452ms
simp 10ms
tactic execution 18ms
type checking 5.86ms
typeclass inference 38.4ms
real 1.78
user 1.09
sys 0.72
LeanPool/BrauerGroupNew/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
import took 1.1s
cumulative profiling times:
attribute application 3.13ms
compilation (IR) 0.0682ms
compilation (LCNF base) 2.91ms
compilation (LCNF impure) 0.375ms
compilation (LCNF mono) 1.77ms
congr simp thm 4.25ms
elaboration 18.4ms
fix level params 0.812ms
import 1.1s
initialization 26.5ms
instantiate metavars 0.837ms
interpretation 143ms
let-to-have transformation 0.0344ms
linting 3.5ms
parsing 2.2ms
process pre-definitions 7.01ms
share common exprs 1.49ms
simp 65.5ms
tactic execution 67.8ms
type checking 41.9ms
typeclass inference 160ms
real 2.08
user 1.44
sys 0.76
LeanPool/BrauerGroupNew/MatrixCenterEquiv.lean
import took 1.3s
cumulative profiling times:
aesop 46ms
attribute application 0.141ms
blocked (unaccounted) 15.8ms
compilation (IR) 0.332ms
compilation (LCNF base) 11.1ms
compilation (LCNF impure) 1.9ms
compilation (LCNF mono) 7.43ms
congr simp thm 3.04ms
elaboration 48.2ms
fix level params 2.42ms
import 1.3s
initialization 26.4ms
instantiate metavars 4.12ms
interpretation 280ms
let-to-have transformation 13.2ms
linting 16.8ms
parsing 11.9ms
process pre-definitions 31.1ms
share common exprs 6.14ms
simp 480ms
tactic execution 241ms
type checking 212ms
typeclass inference 2.15s
real 4.73
user 4.62
sys 0.85
LeanPool/BrauerGroupNew/MatrixEquivTensor.lean
import took 1.24s
simp took 107ms
simp took 177ms
simp took 114ms
cumulative profiling times:
attribute application 21.1ms
compilation (IR) 1.12ms
compilation (LCNF base) 23.8ms
compilation (LCNF impure) 6.09ms
compilation (LCNF mono) 21.5ms
congr simp thm 13.7ms
elaboration 219ms
fix level params 6.19ms
import 1.24s
initialization 26.5ms
instantiate metavars 3.66ms
interpretation 239ms
let-to-have transformation 39.2ms
linting 12.2ms
parsing 9.21ms
process pre-definitions 74ms
share common exprs 12.7ms
simp 1.59s
tactic execution 105ms
type checking 675ms
typeclass inference 4.53s
real 7.81
user 8.62
sys 0.86
LeanPool/BrauerGroupNew/Subfield.lean
import took 1.35s
cumulative profiling times:
elaboration 0.18ms
import 1.35s
initialization 26.6ms
interpretation 128ms
linting 0.192ms
parsing 0.0277ms
real 2.04
user 1.21
sys 0.85
LeanPool/BrauerGroupNew/Subfield/Defs.lean
import took 1.24s
simp took 278ms
simp took 198ms
cumulative profiling times:
aesop 17.1ms
attribute application 7.73ms
blocked (unaccounted) 93.9ms
compilation (IR) 0.185ms
compilation (LCNF base) 5.07ms
compilation (LCNF impure) 0.874ms
compilation (LCNF mono) 3.6ms
congr simp thm 9.41ms
elaboration 189ms
fix level params 4.03ms
import 1.24s
initialization 26.5ms
instantiate metavars 1.5ms
interpretation 455ms
let-to-have transformation 48.1ms
linting 12.1ms
parsing 8.82ms
process pre-definitions 32.4ms
share common exprs 8.39ms
simp 684ms
tactic execution 59.5ms
type checking 144ms
typeclass inference 488ms
real 3.19
user 3.21
sys 0.83
LeanPool/BrauerGroupNew/Subfield/FiniteDimensional.lean
import took 1.36s
cumulative profiling times:
attribute application 0.483ms
elaboration 24.7ms
fix level params 0.048ms
import 1.36s
initialization 26.3ms
instantiate metavars 0.0109ms
interpretation 130ms
let-to-have transformation 0.267ms
linting 0.704ms
parsing 0.339ms
process pre-definitions 0.196ms
share common exprs 0.0895ms
type checking 18.7ms
typeclass inference 114ms
real 2.21
user 1.37
sys 0.87
LeanPool/BrauerGroupNew/TwoSidedIdeal.lean
import took 1.18s
cumulative profiling times:
attribute application 0.233ms
compilation (IR) 0.0769ms
compilation (LCNF base) 1.49ms
compilation (LCNF impure) 0.346ms
compilation (LCNF mono) 1.29ms
congr simp thm 6.24ms
elaboration 56.9ms
fix level params 3.06ms
import 1.18s
initialization 26.6ms
instantiate metavars 5.19ms
interpretation 277ms
let-to-have transformation 0.11ms
linting 11.8ms
parsing 7.09ms
process pre-definitions 14.8ms
share common exprs 8.84ms
simp 185ms
tactic execution 236ms
type checking 57.6ms
typeclass inference 542ms
real 2.71
user 2.39
sys 0.81
LeanPool/BrauerGroupNew/Wedderburn.lean
import took 1.51s
simp took 150ms
cumulative profiling times:
aesop 229ms
attribute application 2.54ms
blocked (unaccounted) 15.9ms
compilation (IR) 0.707ms
compilation (LCNF base) 21.9ms
compilation (LCNF impure) 3.61ms
compilation (LCNF mono) 12ms
congr simp thm 38.2ms
dsimp 3.88ms
elaboration 390ms
fix level params 13.7ms
import 1.51s
initialization 26.5ms
instantiate metavars 19.7ms
interpretation 862ms
let-to-have transformation 3.22ms
linting 71.2ms
parsing 41.1ms
process pre-definitions 121ms
share common exprs 37.8ms
simp 2.22s
tactic execution 1.37s
type checking 813ms
typeclass inference 4.94s
real 7.75
user 12.29
sys 1.05
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | ring theory and central simple algebras |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a substantial formalization of the Brauer group of a field and its standard structure theory, including Wedderburn-Artin, splitting fields, base change, and relative Brauer group/cohomology machinery.
Tokens: 250,638 in / 767 out · Tier: flex · Cost: $0.6381
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
/profile |
1 similar comment
|
/profile |
|
Deterministic partial-port audit flags this PR as incomplete against the registered upstream source. Compared with That means the current PR imports useful central-simple-algebra/Wedderburn infrastructure, but not the larger upstream Brauer group development advertised by the repository source. Treating this as request-changes until the missing Brauer group files are ported, or the project title/card/source scope is narrowed to the imported CSA core. This is the failure mode automated in #110. |
|
/profile |
|
Follow-up on the partial-port audit: this PR is not the same failure mode as the imports where the agent stopped before the registered headline result. The current branch already contains the registered core Brauer group declarations |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
Updated this branch against current Verification on the pushed head:
The earlier partial-port flag is no longer active for the current project scope: this PR now imports the Brauer-group core it advertises, and the project metadata is scoped to that textbook/source rather than claiming the full upstream repository tree. |
|
Follow-up on the earlier #88 audit flag: I added the clean upstream Local verification before push:
I will rerun |
|
/review |
|
Follow-up partial-port repair pushed in Restored additional upstream-compatible files from
Verification before push:
The deterministic partial-port audit still rejects the PR: now So this is progress, not a ready-to-merge state. The next substantial blocker is the Morita/DoubleCentralizer/ToSecond downstream chain; several later upstream files also contain forbidden |
|
Pushed another #88 partial-port repair checkpoint: This restores upstream Local verification passed before push:
This PR is still not merge-ready. The deterministic partial-port audit still rejects it at |
|
Pushed another #88 partial-port checkpoint in 23158bc: added LeanPool.BrauerGroupNew.RelativeBrauer and wired it into LeanPool.lean and LeanPool/BrauerGroupNew.lean. This restores the upstream relative Brauer group layer, including Local checks passed before push:
This PR is still not merge-ready. The dependency-chain recovery is continuing; notably |
|
Pushed another #88 partial-port checkpoint in 06f9aab: added LeanPool.BrauerGroupNew.Subfield.Splitting and wired it into the Subfield index and LeanPool.lean. This restores the upstream splitting-field/maximal-subfield layer, including Local checks passed before push:
This is still a partial recovery, not merge-ready. I am continuing with the remaining upstream files now unlocked by the splitting layer. |
|
Pushed another #88 partial-port checkpoint in This restores the upstream cross-product algebra layer, including the Local checks passed before push:
Manual upstream comparison now still shows 15 missing upstream paths: |
|
Pushed another #88 partial-port checkpoint in This restores the upstream Morita change-of-rings layer, including the matrix Morita equivalences, the opposite-division-ring endomorphism equivalence, transport of endomorphism algebras across a Morita equivalence, and the resulting algebra equivalence for Morita-equivalent division algebras. The port adapts a few categorical/additive proof steps to current Mathlib APIs and adds required public docstrings. No active Local checks passed before push:
Manual upstream comparison now still shows 14 missing upstream paths: |
|
Checkpoint update: ported and registered Notes:
Local verification passed:
|
|
Checkpoint update: ported and registered Notes:
Local verification passed:
|
|
Source-coverage audit update: The earlier partial-port concern about
A direct file-set comparison against
Those three upstream files contain active Local checks performed for the audit:
|
|
Partial-port audit follow-up: The old import notes are stale: this PR now includes I compared the PR against
Those files contain live upstream So I do not think #88 is exhibiting the failure mode where the porting agent gave up on completed upstream theorems. The remaining omissions are incomplete upstream files, not dropped verified source. |
|
/review |
Review — promising, but holding (no current LLM verdict + round limit reached)Significance — good. A substantial Brauer-group development ( CI — green (warning-free build, runLinter, lint-style, mk_all, quality + axiom audit). LLM review — missing. The automated review was skipped ("Lean Action CI conclusion was Compile speed — moderate (~116 s import-excluded serial; worth confirming the parallel wall-clock). Decision: hold for now. Not because of a red flag, but because (a) there is no current LLM verdict yet, and (b) I've reached the 10-merge cap for this round. Recommend merging once the fresh |
# Conflicts: # LeanPool/projects.yml
Imported from https://github.com/Whysoserioushah/BrauerGroup_new.
Slug:
brauergroup_newToolchain target:
leanprover/lean4:v4.30.0-rc2Branch:
import/brauergroup_new(auto-generated byscripts/import-formalization.sh)Agent:
codexusinggpt-5.5at effortxhigh, exited with code0.Commits on this branch:
Import notes (from agent)
Import notes for
brauergroup_newSource: https://github.com/Whysoserioushah/BrauerGroup_new
The source repository is Apache-2.0 licensed, compatible with Lean Pool.
Imported the core files needed for central simple algebra infrastructure,
tensor-product centralizer results, matrix/tensor equivalences, and the
Wedderburn-Artin statements.
Excluded examples, tests, and scratch material. Also excluded downstream source
files whose proofs were incomplete or depended on substantially unfinished
sections in the source, including the original
BrauerGroup.leanandFiniteField.lean. I first tried porting the Brauer-group files, but thecurrent source depends on unfinished base-change and commutativity
constructions that generated unresolved declarations and
sorrydiagnosticsunder Lean 4.30.0-rc2.
FiniteField.leandepends on that excluded API.No excluded file is required by the imported verified entry module.
Opened automatically by
scripts/import-formalization.sh. Review the diff carefully before merging — the agent ran unattended.