Import Wallace problem formalization - #397
Open
Vilin97 wants to merge 9 commits into
Open
Conversation
Greptile SummaryThe PR imports and registers the Wallace-problem formalization, exposing its three principal results. The targeted follow-up refactor:
|
| Filename | Overview |
|---|---|
| LeanPool/Wallace/CoefficientTransfiniteExtension.lean | Provides the shared coefficient-parametric transfinite-extension pipeline that resolves the previously reported duplication. |
| LeanPool/Wallace/TransfiniteExtension.lean | Reduces the integer implementation to a coordinate-extension definition and thin wrappers over the shared core. |
| LeanPool/Wallace/RationalTransfiniteExtension.lean | Keeps the Baer-based rational coordinate construction while delegating the common recursion and admissibility machinery to the shared core. |
| LeanPool/Wallace.lean | Defines the project entry module and imports the modules exposing the three principal Wallace results. |
| LeanPool/projects.yml | Registers the pinned upstream source, license, project metadata, and three paper-level results. |
| LeanPool.lean | Adds all Wallace modules to the generated repository umbrella. |
Reviews (5): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Contributor
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: 3,634 maxHeartbeats units across 39 files (7,391 added LOC). Sum of Count-heartbeats wall-clock total: 145.90 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.Wallace.UniformKronecker |
12.00 s |
LeanPool.Wallace.FiniteCombinatorics |
9.30 s |
LeanPool.Wallace.FusionStage |
4.80 s |
LeanPool.Wallace.TriangularPreprocess |
4.60 s |
LeanPool.Wallace.FusionSchedule |
4.50 s |
LeanPool.Wallace.BoundedIndependentMap |
4.40 s |
LeanPool.Wallace.NontrivialSequences |
4.20 s |
LeanPool.Wallace.TransfiniteExtension |
4.20 s |
LeanPool.Wallace.MathlibFoundations |
4.10 s |
LeanPool.Wallace.BlockFilters |
4.10 s |
LeanPool.Wallace.RationalTransfiniteExtension |
4.10 s |
LeanPool.Wallace.LocalFusion |
4.10 s |
Per-file `lean --profile` output
LeanPool/Wallace.lean
import took 1.9s
cumulative profiling times:
elaboration 0.21ms
import 1.9s
initialization 39.9ms
interpretation 209ms
linting 0.407ms
module linting 0.00146ms
overlappingInstancesLinter 0.849ms
parsing 0.05ms
tacticAnalysis 2.96ms
real 2.86
user 1.55
sys 1.32
LeanPool/Wallace/BlockFilters.lean
import took 1.52s
cumulative profiling times:
attribute application 1.3ms
blocked (unaccounted) 0.459ms
compilation (IR) 0.0684ms
compilation (LCNF base) 0.552ms
compilation (LCNF impure) 0.311ms
compilation (LCNF mono) 0.408ms
congr simp thm 6.17ms
dsimp 8.88ms
elaboration 80.9ms
fix level params 0.836ms
import 1.52s
initialization 40.2ms
instantiate metavars 1.33ms
interpretation 487ms
let-to-have transformation 0.221ms
linting 29.3ms
module linting 0.00166ms
norm_num 2.17ms
overlappingInstancesLinter 9.14ms
parsing 22.6ms
process pre-definitions 11.2ms
share common exprs 4.26ms
simp 89.8ms
tactic execution 240ms
tacticAnalysis 57ms
type checking 41.4ms
typeclass inference 255ms
real 2.74
user 2.46
sys 1.13
LeanPool/Wallace/BlockLimit.lean
import took 1.9s
cumulative profiling times:
attribute application 0.0297ms
congr simp thm 1.19ms
dsimp 1.11ms
elaboration 15.6ms
fix level params 0.115ms
import 1.9s
initialization 29.5ms
instantiate metavars 0.298ms
interpretation 255ms
let-to-have transformation 0.0538ms
linting 5.58ms
module linting 0.00138ms
overlappingInstancesLinter 1.79ms
parsing 4.4ms
process pre-definitions 1.28ms
share common exprs 0.686ms
simp 14.6ms
tactic execution 32.6ms
tacticAnalysis 11ms
type checking 8.54ms
typeclass inference 51.3ms
real 2.94
user 1.76
sys 1.29
LeanPool/Wallace/BoundedIndependentMap.lean
import took 1.52s
cumulative profiling times:
attribute application 0.0145ms
congr simp thm 0.813ms
elaboration 5.03ms
fix level params 0.313ms
import 1.52s
initialization 30.2ms
instantiate metavars 0.233ms
interpretation 197ms
let-to-have transformation 0.0234ms
linting 3.35ms
module linting 0.00142ms
overlappingInstancesLinter 2.33ms
parsing 2.28ms
process pre-definitions 0.916ms
share common exprs 0.525ms
simp 14.2ms
tactic execution 18.7ms
tacticAnalysis 8.9ms
type checking 3.14ms
typeclass inference 80.7ms
real 2.52
user 1.47
sys 1.09
LeanPool/Wallace/ConcreteClosure.lean
import took 1.52s
cumulative profiling times:
attribute application 0.0835ms
elaboration 26.8ms
fix level params 0.108ms
import 1.52s
initialization 29.8ms
instantiate metavars 0.125ms
interpretation 220ms
let-to-have transformation 0.0813ms
linting 7.56ms
module linting 0.00151ms
overlappingInstancesLinter 2.44ms
parsing 4.3ms
process pre-definitions 2.17ms
share common exprs 0.572ms
tactic execution 17ms
tacticAnalysis 15ms
type checking 3.46ms
typeclass inference 30ms
real 2.44
user 1.40
sys 1.15
LeanPool/Wallace/ConcreteData.lean
import took 1.53s
cumulative profiling times:
attribute application 0.201ms
compilation (IR) 0.0438ms
compilation (LCNF base) 0.419ms
compilation (LCNF impure) 0.224ms
compilation (LCNF mono) 0.355ms
congr simp thm 0.186ms
elaboration 47.3ms
fix level params 0.256ms
import 1.53s
initialization 29.3ms
instantiate metavars 0.141ms
interpretation 234ms
let-to-have transformation 0.121ms
linting 10.1ms
module linting 0.00167ms
overlappingInstancesLinter 3.73ms
parsing 6.06ms
process pre-definitions 4.02ms
share common exprs 1.14ms
simp 1.36ms
tactic execution 13.1ms
tacticAnalysis 19.3ms
type checking 9ms
typeclass inference 45ms
real 2.50
user 1.52
sys 1.13
LeanPool/Wallace/ConcreteFusionRun.lean
import took 1.9s
cumulative profiling times:
attribute application 0.355ms
compilation (IR) 0.0287ms
compilation (LCNF base) 0.201ms
compilation (LCNF impure) 0.153ms
compilation (LCNF mono) 0.113ms
congr simp thm 1.15ms
elaboration 58.8ms
fix level params 0.383ms
import 1.9s
initialization 30.4ms
instantiate metavars 0.64ms
interpretation 327ms
let-to-have transformation 0.178ms
linting 12.7ms
module linting 0.00164ms
overlappingInstancesLinter 5.2ms
parsing 11.4ms
process pre-definitions 12.2ms
share common exprs 2.03ms
simp 7.37ms
tactic execution 66.5ms
tacticAnalysis 27.6ms
type checking 24.1ms
typeclass inference 89ms
real 3.01
user 1.98
sys 1.32
LeanPool/Wallace/ConcreteLocalSetup.lean
import took 1.94s
cumulative profiling times:
attribute application 0.274ms
compilation (IR) 0.0998ms
compilation (LCNF base) 0.663ms
compilation (LCNF impure) 0.437ms
compilation (LCNF mono) 0.61ms
congr simp thm 3.16ms
elaboration 89.5ms
fix level params 0.645ms
import 1.94s
initialization 36.2ms
instantiate metavars 0.996ms
interpretation 356ms
let-to-have transformation 0.329ms
linting 18.8ms
module linting 0.00177ms
overlappingInstancesLinter 6.27ms
parsing 13.9ms
process pre-definitions 8.77ms
share common exprs 3.77ms
simp 75.6ms
tactic execution 135ms
tacticAnalysis 44.1ms
type checking 28.7ms
typeclass inference 343ms
real 3.27
user 2.54
sys 1.31
LeanPool/Wallace/CountableClosure.lean
import took 887ms
cumulative profiling times:
attribute application 0.0764ms
elaboration 16.7ms
fix level params 0.269ms
import 887ms
initialization 37.7ms
instantiate metavars 0.192ms
interpretation 167ms
let-to-have transformation 0.0591ms
linting 5.68ms
module linting 0.00148ms
overlappingInstancesLinter 2.5ms
parsing 4.3ms
process pre-definitions 3.47ms
share common exprs 0.689ms
tactic execution 17.5ms
tacticAnalysis 13.9ms
type checking 4.14ms
typeclass inference 6.91ms
real 1.71
user 1.00
sys 0.81
LeanPool/Wallace/CountableDisjointization.lean
import took 1.53s
cumulative profiling times:
attribute application 0.0175ms
elaboration 5.94ms
fix level params 0.077ms
import 1.53s
initialization 29.9ms
instantiate metavars 0.0723ms
interpretation 187ms
let-to-have transformation 0.0196ms
linting 2.2ms
module linting 0.00153ms
overlappingInstancesLinter 1.79ms
parsing 2.11ms
process pre-definitions 0.502ms
share common exprs 0.181ms
tactic execution 9.74ms
tacticAnalysis 8.49ms
type checking 1.64ms
typeclass inference 14.2ms
real 2.44
user 1.38
sys 1.10
LeanPool/Wallace/FiniteCombinatorics.lean
import took 1.52s
cumulative profiling times:
attribute application 1.42ms
blocked (unaccounted) 309ms
compilation (IR) 0.0758ms
compilation (LCNF base) 0.574ms
compilation (LCNF impure) 0.393ms
compilation (LCNF mono) 0.554ms
congr simp thm 7.18ms
dsimp 0.891ms
elaboration 98.8ms
fix level params 3.37ms
import 1.52s
initialization 30.1ms
instantiate metavars 5.17ms
interpretation 487ms
let-to-have transformation 0.288ms
linting 44.3ms
module linting 0.00144ms
overlappingInstancesLinter 15.6ms
parsing 30ms
process pre-definitions 20ms
share common exprs 8.35ms
simp 555ms
tactic execution 379ms
tacticAnalysis 76.8ms
type checking 74.9ms
typeclass inference 663ms
real 3.60
user 3.52
sys 1.19
LeanPool/Wallace/FullTopology.lean
import took 1.36s
cumulative profiling times:
attribute application 4.17ms
blocked (unaccounted) 2.25ms
compilation (IR) 0.0871ms
compilation (LCNF base) 2.23ms
compilation (LCNF impure) 0.338ms
compilation (LCNF mono) 1.05ms
congr simp thm 10.3ms
elaboration 135ms
fix level params 1.34ms
import 1.36s
initialization 30ms
instantiate metavars 0.99ms
interpretation 309ms
let-to-have transformation 0.24ms
linting 18.3ms
module linting 0.0016ms
overlappingInstancesLinter 10.2ms
parsing 14.8ms
process pre-definitions 13ms
share common exprs 3.2ms
simp 29.5ms
tactic execution 106ms
tacticAnalysis 39.2ms
type checking 90.3ms
typeclass inference 272ms
real 2.52
user 2.08
sys 1.06
LeanPool/Wallace/FullTopologyMain.lean
import took 1.9s
cumulative profiling times:
attribute application 0.0135ms
elaboration 1.92ms
fix level params 0.00517ms
import 1.9s
initialization 30ms
instantiate metavars 0.00429ms
interpretation 235ms
let-to-have transformation 0.00814ms
linting 1.11ms
module linting 0.00147ms
overlappingInstancesLinter 1.38ms
parsing 0.526ms
process pre-definitions 0.156ms
share common exprs 0.0112ms
tacticAnalysis 6.47ms
type checking 0.0577ms
real 2.85
user 1.57
sys 1.31
LeanPool/Wallace/FusionLimit.lean
import took 1.36s
cumulative profiling times:
attribute application 0.0195ms
congr simp thm 0.493ms
elaboration 15.2ms
fix level params 0.177ms
import 1.36s
initialization 30.8ms
instantiate metavars 0.0885ms
interpretation 188ms
let-to-have transformation 0.0525ms
linting 3.06ms
module linting 0.00166ms
overlappingInstancesLinter 2.83ms
parsing 2.02ms
process pre-definitions 4.13ms
share common exprs 0.645ms
simp 6.03ms
tactic execution 14.2ms
tacticAnalysis 7.56ms
type checking 29.3ms
typeclass inference 127ms
real 2.39
user 1.45
sys 1.03
LeanPool/Wallace/FusionSchedule.lean
import took 1.88s
cumulative profiling times:
attribute application 0.472ms
blocked (unaccounted) 7.9ms
compilation (IR) 0.14ms
compilation (LCNF base) 1.97ms
compilation (LCNF impure) 0.688ms
compilation (LCNF mono) 0.813ms
congr simp thm 1.62ms
elaboration 65.8ms
fix level params 0.71ms
import 1.88s
initialization 30.3ms
instantiate metavars 0.641ms
interpretation 416ms
let-to-have transformation 0.235ms
linting 13.7ms
module linting 0.00148ms
norm_num 4.24ms
overlappingInstancesLinter 8.09ms
parsing 13.9ms
process pre-definitions 9.87ms
ring 20.5ms
share common exprs 5.9ms
simp 21.1ms
tactic execution 62.2ms
tacticAnalysis 27.1ms
type checking 65.1ms
typeclass inference 222ms
real 3.05
user 2.23
sys 1.33
LeanPool/Wallace/FusionStage.lean
import took 1.89s
cumulative profiling times:
attribute application 0.141ms
congr simp thm 4.39ms
elaboration 49.7ms
fix level params 1.69ms
import 1.89s
initialization 35.5ms
instantiate metavars 1.16ms
interpretation 366ms
let-to-have transformation 0.221ms
linting 23.2ms
module linting 0.00152ms
overlappingInstancesLinter 9.12ms
parsing 13.4ms
process pre-definitions 7.69ms
share common exprs 4.14ms
simp 258ms
tactic execution 165ms
tacticAnalysis 40.7ms
type checking 35.9ms
typeclass inference 449ms
real 3.31
user 2.80
sys 1.29
LeanPool/Wallace/GeneralMain.lean
import took 1.89s
cumulative profiling times:
attribute application 0.0383ms
congr simp thm 1.6ms
elaboration 18.5ms
fix level params 0.0846ms
import 1.89s
initialization 30.4ms
instantiate metavars 0.194ms
interpretation 243ms
let-to-have transformation 0.0363ms
linting 3.32ms
module linting 0.00177ms
overlappingInstancesLinter 5.2ms
parsing 3.01ms
process pre-definitions 1.56ms
share common exprs 0.371ms
simp 9.62ms
tactic execution 10.1ms
tacticAnalysis 9.18ms
type checking 4.55ms
typeclass inference 15.9ms
real 2.90
user 1.65
sys 1.32
LeanPool/Wallace/GlobalAssembly.lean
import took 1.54s
cumulative profiling times:
attribute application 0.0721ms
elaboration 51.2ms
fix level params 0.167ms
import 1.54s
initialization 29.7ms
instantiate metavars 0.0967ms
interpretation 222ms
let-to-have transformation 0.137ms
linting 5.75ms
module linting 0.00158ms
overlappingInstancesLinter 2.57ms
parsing 5.2ms
process pre-definitions 3.95ms
share common exprs 1.08ms
tactic execution 18.5ms
tacticAnalysis 15.9ms
type checking 11.7ms
typeclass inference 119ms
real 2.61
user 1.60
sys 1.14
LeanPool/Wallace/InitialCharacter.lean
import took 1.87s
cumulative profiling times:
attribute application 0.0141ms
congr simp thm 0.799ms
elaboration 5.04ms
fix level params 0.14ms
import 1.87s
initialization 34.3ms
instantiate metavars 0.108ms
interpretation 224ms
let-to-have transformation 0.0303ms
linting 2.28ms
module linting 0.00162ms
overlappingInstancesLinter 2.7ms
parsing 1.81ms
process pre-definitions 0.728ms
share common exprs 0.482ms
simp 75.7ms
tactic execution 11ms
tacticAnalysis 6.22ms
type checking 3.78ms
typeclass inference 45.2ms
real 2.96
user 1.72
sys 1.28
LeanPool/Wallace/LocalEnumeration.lean
import took 1.52s
cumulative profiling times:
attribute application 0.0227ms
elaboration 6.88ms
fix level params 0.0246ms
import 1.52s
initialization 30.2ms
instantiate metavars 0.0319ms
interpretation 196ms
let-to-have transformation 0.0246ms
linting 2.2ms
module linting 0.00162ms
overlappingInstancesLinter 1.6ms
parsing 1.73ms
process pre-definitions 0.716ms
share common exprs 0.13ms
tactic execution 4.95ms
tacticAnalysis 8.85ms
type checking 0.768ms
typeclass inference 17.6ms
real 2.43
user 1.37
sys 1.11
LeanPool/Wallace/LocalFusion.lean
import took 1.87s
elaboration took 196ms
cumulative profiling times:
attribute application 0.994ms
blocked (unaccounted) 417ms
compilation (IR) 0.0992ms
compilation (LCNF base) 0.739ms
compilation (LCNF impure) 0.51ms
compilation (LCNF mono) 0.788ms
congr simp thm 35.3ms
elaboration 556ms
fix level params 1.57ms
import 1.87s
initialization 29.9ms
instantiate metavars 1.98ms
interpretation 525ms
let-to-have transformation 0.548ms
linting 43.5ms
module linting 0.00175ms
norm_num 6.16ms
overlappingInstancesLinter 17.4ms
parsing 36.8ms
process pre-definitions 19.8ms
ring 6.29ms
share common exprs 8.27ms
simp 187ms
tactic execution 285ms
tacticAnalysis 83.4ms
type checking 265ms
typeclass inference 640ms
real 4.28
user 4.05
sys 1.32
LeanPool/Wallace/MathlibFoundations.lean
import took 1.03s
cumulative profiling times:
attribute application 0.656ms
compilation (IR) 0.883ms
compilation (LCNF base) 17.4ms
compilation (LCNF impure) 4.83ms
compilation (LCNF mono) 9.21ms
congr simp thm 1.24ms
elaboration 29.2ms
fix level params 0.291ms
import 1.03s
initialization 39ms
instantiate metavars 0.367ms
interpretation 208ms
let-to-have transformation 0.102ms
linting 9ms
module linting 0.00151ms
overlappingInstancesLinter 5.03ms
parsing 8ms
process pre-definitions 3.35ms
share common exprs 1.03ms
simp 34.1ms
tactic execution 32.5ms
tacticAnalysis 19.3ms
type checking 7.8ms
typeclass inference 44ms
real 1.95
user 1.31
sys 0.85
LeanPool/Wallace/NontrivialSequences.lean
import took 1.35s
cumulative profiling times:
attribute application 0.054ms
congr simp thm 1.47ms
dsimp 1.13ms
elaboration 18.5ms
fix level params 0.655ms
import 1.35s
initialization 30.6ms
instantiate metavars 0.714ms
interpretation 226ms
let-to-have transformation 0.0493ms
linting 10.2ms
module linting 0.00146ms
overlappingInstancesLinter 4.66ms
parsing 7.62ms
process pre-definitions 3.56ms
share common exprs 1.44ms
simp 62.5ms
tactic execution 74ms
tacticAnalysis 23ms
type checking 8.39ms
typeclass inference 105ms
real 2.34
user 1.59
sys 1.00
LeanPool/Wallace/PackageTransport.lean
import took 1.33s
cumulative profiling times:
attribute application 0.0241ms
compilation (IR) 0.228ms
compilation (LCNF base) 4.03ms
compilation (LCNF impure) 1.2ms
compilation (LCNF mono) 4.4ms
congr simp thm 0.286ms
elaboration 25.1ms
fix level params 0.34ms
import 1.33s
initialization 37.4ms
instantiate metavars 0.319ms
interpretation 198ms
let-to-have transformation 0.0591ms
linting 4.46ms
module linting 0.00197ms
overlappingInstancesLinter 3.79ms
parsing 3.48ms
process pre-definitions 7.27ms
share common exprs 0.89ms
simp 7.39ms
tactic execution 25.8ms
tacticAnalysis 13.5ms
type checking 17.2ms
typeclass inference 73.3ms
real 2.34
user 1.44
sys 1.00
LeanPool/Wallace/RationalAssembly.lean
import took 1.89s
cumulative profiling times:
attribute application 0.162ms
compilation (IR) 0.0351ms
compilation (LCNF base) 0.303ms
compilation (LCNF impure) 0.158ms
compilation (LCNF mono) 0.151ms
elaboration 43.5ms
fix level params 0.13ms
import 1.89s
initialization 30.3ms
instantiate metavars 0.105ms
interpretation 270ms
let-to-have transformation 0.11ms
linting 5.86ms
module linting 0.00145ms
overlappingInstancesLinter 4.28ms
parsing 4.73ms
process pre-definitions 4.07ms
share common exprs 0.846ms
tactic execution 15.9ms
tacticAnalysis 14.8ms
type checking 12.5ms
typeclass inference 90.4ms
real 2.97
user 1.81
sys 1.30
LeanPool/Wallace/RationalClosure.lean
import took 1.59s
cumulative profiling times:
attribute application 0.0651ms
elaboration 21.4ms
fix level params 0.0747ms
import 1.59s
initialization 33.2ms
instantiate metavars 0.0782ms
interpretation 207ms
let-to-have transformation 0.0622ms
linting 6.3ms
module linting 0.00172ms
overlappingInstancesLinter 2.08ms
parsing 2.45ms
process pre-definitions 1.21ms
share common exprs 0.444ms
tactic execution 9.89ms
tacticAnalysis 11.3ms
type checking 2.51ms
typeclass inference 17.2ms
real 2.51
user 1.45
sys 1.15
LeanPool/Wallace/RationalData.lean
import took 1.61s
cumulative profiling times:
attribute application 0.182ms
compilation (IR) 0.0335ms
compilation (LCNF base) 0.347ms
compilation (LCNF impure) 0.173ms
compilation (LCNF mono) 0.235ms
congr simp thm 0.163ms
elaboration 46.3ms
fix level params 0.232ms
import 1.61s
initialization 30.2ms
instantiate metavars 0.144ms
interpretation 238ms
let-to-have transformation 0.124ms
linting 10.3ms
module linting 0.0015ms
overlappingInstancesLinter 3.55ms
parsing 6.33ms
process pre-definitions 4.12ms
share common exprs 1.22ms
simp 1.33ms
tactic execution 12.3ms
tacticAnalysis 19.6ms
type checking 8.57ms
typeclass inference 39.4ms
real 2.57
user 1.59
sys 1.13
LeanPool/Wallace/RationalFusionRun.lean
import took 1.89s
cumulative profiling times:
attribute application 0.362ms
blocked (unaccounted) 108ms
compilation (IR) 0.0352ms
compilation (LCNF base) 0.249ms
compilation (LCNF impure) 0.181ms
compilation (LCNF mono) 0.15ms
congr simp thm 5.12ms
elaboration 109ms
fix level params 0.451ms
import 1.89s
initialization 29.8ms
instantiate metavars 0.882ms
interpretation 343ms
let-to-have transformation 0.217ms
linting 17ms
module linting 0.00147ms
overlappingInstancesLinter 5.67ms
parsing 14ms
process pre-definitions 11.4ms
share common exprs 2.71ms
simp 28ms
tactic execution 110ms
tacticAnalysis 31.5ms
type checking 66.7ms
typeclass inference 153ms
real 3.20
user 2.22
sys 1.34
LeanPool/Wallace/RationalLocalSetup.lean
import took 1.9s
cumulative profiling times:
attribute application 0.267ms
compilation (IR) 0.0724ms
compilation (LCNF base) 0.843ms
compilation (LCNF impure) 0.429ms
compilation (LCNF mono) 0.554ms
congr simp thm 2.6ms
elaboration 86.5ms
fix level params 0.643ms
import 1.9s
initialization 35.8ms
instantiate metavars 0.971ms
interpretation 337ms
let-to-have transformation 0.317ms
linting 19.2ms
module linting 0.00154ms
overlappingInstancesLinter 5.54ms
parsing 12.3ms
process pre-definitions 8.39ms
share common exprs 3.49ms
simp 76.4ms
tactic execution 123ms
tacticAnalysis 42.6ms
type checking 27.3ms
typeclass inference 320ms
real 3.18
user 2.40
sys 1.33
LeanPool/Wallace/RationalTransfiniteExtension.lean
import took 1.6s
cumulative profiling times:
attribute application 1.74ms
blocked (unaccounted) 0.916ms
compilation (IR) 0.269ms
compilation (LCNF base) 5.9ms
compilation (LCNF impure) 1.2ms
compilation (LCNF mono) 2.57ms
congr simp thm 9.98ms
elaboration 131ms
fix level params 1.77ms
import 1.6s
initialization 30.3ms
instantiate metavars 1.25ms
interpretation 315ms
let-to-have transformation 0.488ms
linting 22.1ms
module linting 0.00167ms
overlappingInstancesLinter 9.54ms
parsing 18.6ms
process pre-definitions 13.3ms
share common exprs 5.88ms
simp 86.9ms
tactic execution 171ms
tacticAnalysis 40.9ms
type checking 71.2ms
typeclass inference 485ms
real 3.01
user 2.57
sys 1.17
LeanPool/Wallace/RationalTriangularPreprocess.lean
import took 1.52s
cumulative profiling times:
attribute application 0.311ms
blocked (unaccounted) 11.6ms
congr simp thm 2.69ms
elaboration 36.2ms
fix level params 0.257ms
import 1.52s
initialization 29.6ms
instantiate metavars 0.447ms
interpretation 274ms
let-to-have transformation 0.146ms
linting 13.6ms
module linting 0.00151ms
overlappingInstancesLinter 5.36ms
parsing 10.1ms
process pre-definitions 5.32ms
share common exprs 1.49ms
simp 88.2ms
tactic execution 52.2ms
tacticAnalysis 25.2ms
type checking 13.2ms
typeclass inference 116ms
real 2.57
user 1.75
sys 1.12
LeanPool/Wallace/RealMain.lean
import took 1.91s
cumulative profiling times:
attribute application 0.0545ms
elaboration 16ms
fix level params 0.0582ms
import 1.91s
initialization 35.7ms
instantiate metavars 0.0568ms
interpretation 236ms
let-to-have transformation 0.046ms
linting 2.24ms
module linting 0.0014ms
overlappingInstancesLinter 1.72ms
parsing 2.16ms
process pre-definitions 1.97ms
share common exprs 0.287ms
tactic execution 7.69ms
tacticAnalysis 6.43ms
type checking 18ms
typeclass inference 68.2ms
real 2.95
user 1.67
sys 1.35
LeanPool/Wallace/Result.lean
import took 1.1s
cumulative profiling times:
attribute application 0.137ms
compilation (IR) 0.027ms
compilation (LCNF base) 0.675ms
compilation (LCNF impure) 0.117ms
compilation (LCNF mono) 0.214ms
congr simp thm 0.942ms
elaboration 62.2ms
fix level params 0.996ms
import 1.1s
initialization 31.2ms
instantiate metavars 0.723ms
interpretation 230ms
let-to-have transformation 0.18ms
linting 14.5ms
module linting 0.00186ms
overlappingInstancesLinter 8.82ms
parsing 11.3ms
process pre-definitions 5.75ms
share common exprs 2.24ms
simp 18.4ms
tactic execution 65.1ms
tacticAnalysis 26.7ms
type checking 19.1ms
typeclass inference 155ms
real 2.09
user 1.50
sys 0.94
LeanPool/Wallace/SeparationInterface.lean
import took 1.33s
cumulative profiling times:
attribute application 0.107ms
blocked (unaccounted) 2.42ms
congr simp thm 9.18ms
elaboration 52.2ms
fix level params 0.56ms
import 1.33s
initialization 36.4ms
instantiate metavars 0.414ms
interpretation 231ms
let-to-have transformation 0.0904ms
linting 7.16ms
module linting 0.0015ms
overlappingInstancesLinter 3.68ms
parsing 7.72ms
process pre-definitions 5.24ms
share common exprs 1.51ms
simp 17.7ms
tactic execution 62.1ms
tacticAnalysis 18.5ms
type checking 53.3ms
typeclass inference 155ms
real 2.40
user 1.65
sys 1.02
LeanPool/Wallace/TorsionFreeCoordinate.lean
import took 1.54s
cumulative profiling times:
attribute application 0.16ms
blocked (unaccounted) 1.75ms
congr simp thm 7.02ms
elaboration 79.9ms
fix level params 0.347ms
import 1.54s
initialization 29.8ms
instantiate metavars 0.301ms
interpretation 246ms
let-to-have transformation 0.626ms
linting 10.7ms
module linting 0.00174ms
overlappingInstancesLinter 7.1ms
parsing 7.27ms
process pre-definitions 7.94ms
share common exprs 2.08ms
simp 87.9ms
tactic execution 60ms
tacticAnalysis 21.6ms
type checking 64.4ms
typeclass inference 593ms
real 2.80
user 2.34
sys 1.11
LeanPool/Wallace/TransfiniteExtension.lean
import took 1.52s
cumulative profiling times:
attribute application 0.766ms
blocked (unaccounted) 0.873ms
compilation (IR) 0.05ms
compilation (LCNF base) 1.1ms
compilation (LCNF impure) 0.249ms
compilation (LCNF mono) 0.36ms
congr simp thm 7.83ms
elaboration 96.3ms
fix level params 1.85ms
import 1.52s
initialization 30.4ms
instantiate metavars 1.12ms
interpretation 328ms
let-to-have transformation 0.355ms
linting 19.6ms
module linting 0.00149ms
overlappingInstancesLinter 10.5ms
parsing 16.2ms
process pre-definitions 10.2ms
share common exprs 4.45ms
simp 31.5ms
tactic execution 150ms
tacticAnalysis 36.9ms
type checking 48.2ms
typeclass inference 361ms
real 2.85
user 2.28
sys 1.11
LeanPool/Wallace/TriangularPreprocess.lean
import took 1.54s
cumulative profiling times:
attribute application 0.833ms
blocked (unaccounted) 166ms
compilation (IR) 0.393ms
compilation (LCNF base) 8.19ms
compilation (LCNF impure) 4.78ms
compilation (LCNF mono) 3.41ms
congr simp thm 14.9ms
elaboration 139ms
fix level params 1.59ms
import 1.54s
initialization 30ms
instantiate metavars 2.16ms
interpretation 516ms
let-to-have transformation 0.626ms
linting 59.3ms
module linting 0.00149ms
overlappingInstancesLinter 17.9ms
parsing 36.4ms
process pre-definitions 21.8ms
share common exprs 6.45ms
simp 273ms
tactic execution 305ms
tacticAnalysis 87.6ms
type checking 81.1ms
typeclass inference 424ms
real 2.96
user 3.03
sys 1.19
LeanPool/Wallace/TychonoffWallace.lean
import took 1.89s
cumulative profiling times:
attribute application 0.0493ms
elaboration 13.9ms
fix level params 0.094ms
import 1.89s
initialization 33.8ms
instantiate metavars 0.113ms
interpretation 254ms
let-to-have transformation 0.0424ms
linting 3.51ms
module linting 0.00165ms
overlappingInstancesLinter 3.95ms
parsing 3.05ms
process pre-definitions 1.64ms
share common exprs 0.387ms
tactic execution 19.2ms
tacticAnalysis 10.4ms
type checking 6.63ms
typeclass inference 46.8ms
real 2.90
user 1.69
sys 1.31
LeanPool/Wallace/UniformKronecker.lean
import took 1.85s
simp took 201ms
simp took 130ms
simp took 137ms
cumulative profiling times:
attribute application 5.39ms
compilation (IR) 0.507ms
compilation (LCNF base) 14.5ms
compilation (LCNF impure) 2.67ms
compilation (LCNF mono) 5.12ms
congr simp thm 13ms
dsimp 4.05ms
elaboration 206ms
fix level params 4.07ms
import 1.85s
initialization 34.3ms
instantiate metavars 7.48ms
interpretation 751ms
let-to-have transformation 4.24ms
linting 70.6ms
module linting 0.00145ms
norm_num 16.6ms
overlappingInstancesLinter 14.6ms
parsing 50.2ms
process pre-definitions 57.8ms
ring 13.4ms
share common exprs 28.2ms
simp 1.13s
tactic execution 945ms
tacticAnalysis 104ms
type checking 385ms
typeclass inference 3.05s
real 5.41
user 8.13
sys 1.39
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All three headline declarations match the card’s informal statements, with no undisclosed mathematical assumptions. |
| Novelty | ✅ pass |
None of the three headline results is already formalized in the searched Mathlib declarations or the listed pool projects. |
| Significance | ✅ pass |
This is a substantial research-level formalization of a named problem, with unconditional group-topology theorems and the Wallace counterexample as completed endpoints. |
| Sources | ✅ pass |
The citation metadata is internally consistent, but the diff does not reproduce enough of the cited paper to verify the three claimed paper-level correspondences. |
| Code quality (advisory) | ✅ pass |
The construction is maintainably decomposed: shared closure, coefficient-parametric transfinite extension, scheduling, and limit arguments are factored once, while endpoint modules remain concise assembly layers. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Wallace.torsionFreeAbelianGroup_mainTheorem_exact assumes an additive commutative group structure, torsion-freeness, and #G = 𝔠; all are disclosed in the card. The rational/real and Wallace-counterexample endpoints are unconditional. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | set-theoretic topology and topological algebra |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The Lean constructs the claimed Hausdorff countably compact group topologies with every convergent sequence eventually constant, and an explicit commutative Tychonoff countably compact cancellative topological monoid containing a non-additive-unit.
The project constructs Hausdorff countably compact group topologies without nontrivial convergent sequences on continuum-sized torsion-free Abelian groups and derives a commutative Tychonoff countably compact cancellative semigroup that is not a group.
Tokens: 534,917 in / 10,247 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $1.4910
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.
Owner
Author
|
Addressed all three code-quality findings in
I also audited the residual Z/Q adapters declaration-by-declaration and prototyped a wider dependent extraction. The two branches use distinct Measured result: 8,464 -> 7,206 Lean lines (-1,258, -14.9%), 731 -> 582 declarations (all 582 source-live), and 697 constants in the three-endpoint kernel closure. A clean focused build is 29.50s / 3.53 GB versus the canonical 48.97s / 6.90 GB. Full project build, aggregate collision compile, all project lint/style checks, static quality, exact endpoint signatures, and allowed-axiom audits are green. |
Owner
Author
Automation disposition: mergeReviewed exact head |
Owner
Author
Automation disposition: mergeReviewed exact head |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
vo-rodrigues/wallace-problem-zfc-paper@23756864de1f14e272dafb070b97fcdc7cbc75c5Wallace.torsionFreeAbelianGroup_mainTheorem_exactWallace.continuumRationalGroup_and_real_mainTheoremWallace.commutativeTychonoffWallaceCounterexampleExistsregister the project, and regenerate the umbrella
Optimization audit
through extracted kernel/source dependencies plus one genuinely source-used
simp lemma); the compiled kernel closure contains 697 constants
module
a coefficient-parametric core; the two 555-line pipelines are now a 268-line
shared implementation plus 76/103-line coefficient adapters (447 lines,
-19.5%), without casts or transports
relevant-code scheduling, countable local-group enumeration, and retained-block
convergence into shared implementations; the integer/rational modules now
contain only their coefficient-specific prepared-vector adapters
removed the two linter-proven unused hypotheses and their now-dead callers
(-39.8% wall time, -48.8% peak RSS)
local implementation scaffolding
ultrafilter, integer-annihilator, and uniform-Kronecker abstractions; none was
an exact reusable match, so this adds no cross-project dependency
(
Hversus a concrete fusion certificate) and result records(
SeparationPackageversusFullCharacterPackage) differ, so forcing themthrough a dependent configuration record would add more machinery than the
three thin wrappers it could share
the shared scheduling spine is now generic, while the remaining proofs depend
on distinct code embeddings and on
↑Dversus predicate-subtype Finsuppdomains that are not definitionally equal; a prototype required explicit
transports and a nine-field dependent configuration, increasing rather than
reducing the two 209/214-line adapters
Validation
mk_all --checkLeanPool.leancollision compilepropext,Classical.choice, andQuot.soundsorry,admit,unsafe,partial,opaque,set_option, lint waiver,or diagnostic command