Import Nash-Williams fronts and 2-BQO - #380
Open
Vilin97 wants to merge 11 commits into
Open
Conversation
Greptile SummaryThe PR imports the Nash-Williams fronts and finite-rank 2-BQO formalization, exposes it through project and root umbrella modules, and registers its principal declarations in the project catalog.
|
| Filename | Overview |
|---|---|
| LeanPool/projects.yml | Registers the project and now describes TwoBQO.embedForAll_wqo consistently with its exact hypotheses and sequence-embedding relation. |
| LeanPool/NashWilliams/Order/TwoBQO.lean | Defines 2-BQO and sequence embedding and proves the registered well-quasi-order headline under the documented preorder hypothesis. |
| LeanPool/NashWilliams/Combinatorics/Front/NashWilliams.lean | Adds the Nash-Williams theorem, its finite-color form, and the resulting finite-arity infinite Ramsey theorem. |
| LeanPool/NashWilliams.lean | Provides the stable project umbrella for the imported combinatorics, data, and order modules. |
| LeanPool.lean | Makes the new project and its constituent modules reachable through the aggregate library entry point. |
Reviews (11): 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: 535 maxHeartbeats units across 20 files (2,651 added LOC). Sum of Count-heartbeats wall-clock total: 49.78 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.NashWilliams.Order.TwoBQO |
4.70 s |
LeanPool.NashWilliams.Order.WellQuasiOrder.Regular |
3.90 s |
LeanPool.NashWilliams.Combinatorics.Front.Rank |
3.90 s |
LeanPool.NashWilliams.Data.Nat.Nth |
3.30 s |
LeanPool.NashWilliams.Data.Fintype.Pigeonhole |
3.30 s |
LeanPool.NashWilliams.Combinatorics.Front.Defs |
2.60 s |
LeanPool.NashWilliams.Order.WellQuasiOrder |
2.30 s |
LeanPool.NashWilliams.Combinatorics.Front.Ray |
2.10 s |
LeanPool.NashWilliams.Combinatorics.Front.Shrink |
2.10 s |
LeanPool.NashWilliams.Combinatorics.Ramsey.Infinite |
2.00 s |
LeanPool.NashWilliams.Combinatorics.Front.NashWilliams |
1.90 s |
LeanPool.NashWilliams.Data.Fintype |
1.80 s |
Per-file `lean --profile` output
LeanPool/NashWilliams.lean
import took 984ms
cumulative profiling times:
elaboration 0.353ms
import 984ms
initialization 29ms
interpretation 119ms
linting 0.299ms
module linting 0.00147ms
overlappingInstancesLinter 0.3ms
parsing 0.029ms
tacticAnalysis 0.892ms
real 1.74
user 0.95
sys 0.81
LeanPool/NashWilliams/Combinatorics.lean
import took 956ms
cumulative profiling times:
elaboration 0.132ms
import 956ms
initialization 40.3ms
interpretation 113ms
linting 0.241ms
module linting 0.00149ms
overlappingInstancesLinter 0.447ms
parsing 0.0267ms
tacticAnalysis 0.732ms
real 1.73
user 0.97
sys 0.77
LeanPool/NashWilliams/Combinatorics/Front.lean
import took 912ms
cumulative profiling times:
elaboration 0.182ms
import 912ms
initialization 29.7ms
interpretation 114ms
linting 0.289ms
module linting 0.00114ms
overlappingInstancesLinter 0.27ms
parsing 0.0262ms
tacticAnalysis 2.31ms
real 1.67
user 0.94
sys 0.74
LeanPool/NashWilliams/Combinatorics/Front/Defs.lean
import took 859ms
cumulative profiling times:
attribute application 0.447ms
blocked (unaccounted) 14.8ms
congr simp thm 2.86ms
elaboration 58.4ms
fix level params 0.45ms
import 859ms
initialization 28.7ms
instantiate metavars 1.14ms
interpretation 259ms
let-to-have transformation 0.104ms
linting 19.7ms
module linting 0.00132ms
overlappingInstancesLinter 4.86ms
parsing 13.6ms
process pre-definitions 5.47ms
share common exprs 2.61ms
simp 68ms
tactic execution 101ms
tacticAnalysis 37ms
type checking 33.1ms
typeclass inference 46.8ms
real 1.79
user 1.37
sys 0.76
LeanPool/NashWilliams/Combinatorics/Front/NashWilliams.lean
import took 877ms
cumulative profiling times:
attribute application 0.0799ms
congr simp thm 0.517ms
elaboration 49.2ms
fix level params 0.659ms
import 877ms
initialization 35.4ms
instantiate metavars 3.09ms
interpretation 288ms
let-to-have transformation 0.128ms
linting 23.8ms
module linting 0.00141ms
overlappingInstancesLinter 5.13ms
parsing 20.2ms
process pre-definitions 6.37ms
share common exprs 4.13ms
simp 4.28ms
tactic execution 256ms
tacticAnalysis 51.2ms
type checking 47.5ms
typeclass inference 116ms
real 1.93
user 1.65
sys 0.76
LeanPool/NashWilliams/Combinatorics/Front/Rank.lean
import took 890ms
cumulative profiling times:
attribute application 0.211ms
congr simp thm 4.7ms
elaboration 84.5ms
fix level params 1.12ms
import 890ms
initialization 28.4ms
instantiate metavars 4.74ms
interpretation 407ms
let-to-have transformation 0.194ms
linting 40.2ms
module linting 0.00151ms
overlappingInstancesLinter 7.67ms
parsing 35.3ms
process pre-definitions 13.3ms
share common exprs 8.49ms
simp 214ms
tactic execution 482ms
tacticAnalysis 84.6ms
type checking 242ms
typeclass inference 263ms
real 2.18
user 2.65
sys 0.76
LeanPool/NashWilliams/Combinatorics/Front/Ray.lean
import took 896ms
cumulative profiling times:
attribute application 0.188ms
congr simp thm 1.92ms
elaboration 67.6ms
fix level params 0.559ms
import 896ms
initialization 33.5ms
instantiate metavars 1.68ms
interpretation 298ms
let-to-have transformation 0.153ms
linting 26.1ms
module linting 0.00147ms
overlappingInstancesLinter 5.21ms
parsing 21.3ms
process pre-definitions 7.29ms
share common exprs 3.24ms
simp 61.9ms
tactic execution 205ms
tacticAnalysis 56.4ms
type checking 92.4ms
typeclass inference 65.9ms
real 1.86
user 1.68
sys 0.75
LeanPool/NashWilliams/Combinatorics/Front/Shrink.lean
import took 901ms
cumulative profiling times:
attribute application 0.183ms
blocked (unaccounted) 0.795ms
congr simp thm 1.31ms
elaboration 24.9ms
fix level params 0.22ms
import 901ms
initialization 35.5ms
instantiate metavars 0.749ms
interpretation 205ms
let-to-have transformation 0.0583ms
linting 10.3ms
module linting 0.0016ms
overlappingInstancesLinter 2.31ms
parsing 7.71ms
process pre-definitions 2.66ms
share common exprs 1.24ms
simp 36.5ms
tactic execution 56.4ms
tacticAnalysis 21.1ms
type checking 8.15ms
typeclass inference 13.1ms
real 1.77
user 1.15
sys 0.76
LeanPool/NashWilliams/Combinatorics/Ramsey.lean
import took 871ms
cumulative profiling times:
elaboration 0.25ms
import 871ms
initialization 29.4ms
interpretation 106ms
linting 0.302ms
module linting 0.00137ms
overlappingInstancesLinter 0.193ms
parsing 0.0259ms
tacticAnalysis 0.88ms
real 1.59
user 0.88
sys 0.73
LeanPool/NashWilliams/Combinatorics/Ramsey/Infinite.lean
import took 863ms
cumulative profiling times:
attribute application 0.0529ms
blocked (unaccounted) 0.796ms
congr simp thm 5.98ms
elaboration 35.3ms
fix level params 0.921ms
import 863ms
initialization 36.7ms
instantiate metavars 3.26ms
interpretation 292ms
let-to-have transformation 0.0547ms
linting 36.8ms
module linting 0.00139ms
overlappingInstancesLinter 5.72ms
parsing 18ms
process pre-definitions 8.62ms
share common exprs 3.67ms
simp 34.8ms
tactic execution 309ms
tacticAnalysis 72ms
type checking 36.4ms
typeclass inference 54.8ms
real 1.92
user 1.68
sys 0.73
LeanPool/NashWilliams/Data.lean
import took 858ms
cumulative profiling times:
elaboration 0.188ms
import 858ms
initialization 29.3ms
interpretation 110ms
linting 0.296ms
module linting 0.00138ms
overlappingInstancesLinter 0.275ms
parsing 0.0252ms
tacticAnalysis 2.69ms
real 1.57
user 0.86
sys 0.73
LeanPool/NashWilliams/Data/Fintype.lean
import took 800ms
cumulative profiling times:
elaboration 0.12ms
import 800ms
initialization 34.2ms
interpretation 103ms
linting 0.459ms
module linting 0.00149ms
overlappingInstancesLinter 0.381ms
parsing 0.0259ms
tacticAnalysis 0.795ms
real 1.53
user 0.83
sys 0.71
LeanPool/NashWilliams/Data/Fintype/Pigeonhole.lean
import took 807ms
cumulative profiling times:
attribute application 0.0115ms
elaboration 1.84ms
fix level params 0.022ms
import 807ms
initialization 40.6ms
instantiate metavars 0.0362ms
interpretation 106ms
let-to-have transformation 0.0103ms
linting 0.561ms
module linting 0.00157ms
overlappingInstancesLinter 1.03ms
parsing 0.633ms
process pre-definitions 0.221ms
share common exprs 0.0497ms
tactic execution 2.44ms
tacticAnalysis 1.19ms
type checking 0.345ms
typeclass inference 0.2ms
real 1.54
user 0.85
sys 0.71
LeanPool/NashWilliams/Data/Nat.lean
import took 869ms
cumulative profiling times:
elaboration 0.313ms
import 869ms
initialization 33.1ms
interpretation 106ms
linting 0.312ms
module linting 0.00143ms
overlappingInstancesLinter 0.414ms
parsing 0.0274ms
tacticAnalysis 0.887ms
real 1.61
user 0.92
sys 0.70
LeanPool/NashWilliams/Data/Nat/Nth.lean
import took 870ms
cumulative profiling times:
attribute application 0.0189ms
congr simp thm 0.356ms
elaboration 4.74ms
fix level params 0.0297ms
import 870ms
initialization 29.4ms
instantiate metavars 0.0982ms
interpretation 111ms
let-to-have transformation 0.0203ms
linting 1.37ms
module linting 0.00148ms
overlappingInstancesLinter 0.784ms
parsing 1.22ms
process pre-definitions 0.407ms
share common exprs 0.139ms
simp 1.91ms
tactic execution 7.23ms
tacticAnalysis 2.37ms
type checking 0.585ms
typeclass inference 1.12ms
real 1.60
user 0.91
sys 0.72
LeanPool/NashWilliams/Order.lean
import took 928ms
cumulative profiling times:
elaboration 0.159ms
import 928ms
initialization 28.7ms
interpretation 123ms
linting 0.292ms
module linting 0.00113ms
overlappingInstancesLinter 0.266ms
parsing 0.0269ms
tacticAnalysis 1.29ms
real 1.66
user 0.92
sys 0.76
LeanPool/NashWilliams/Order/TwoBQO.lean
import took 938ms
cumulative profiling times:
aesop 29.8ms
attribute application 0.669ms
compilation (IR) 0.0862ms
compilation (LCNF base) 0.691ms
compilation (LCNF impure) 0.483ms
compilation (LCNF mono) 0.82ms
congr simp thm 14.6ms
elaboration 132ms
fix level params 3.35ms
grind 61.4ms
grind ac 0.0254ms
grind cutsat 2.21ms
grind ematch 24ms
grind linarith 0.0169ms
grind mark subsingleton 7.69ms
grind ring 0.139ms
grind simp 55.4ms
import 938ms
initialization 36.1ms
instantiate metavars 5.97ms
interpretation 736ms
let-to-have transformation 0.271ms
linting 63.5ms
module linting 0.00174ms
norm_num 12.2ms
overlappingInstancesLinter 13.9ms
parsing 48.1ms
process pre-definitions 22.5ms
ring 22ms
share common exprs 12ms
simp 308ms
sym canon 5.71ms
sym typeclass inference 6.15ms
tactic execution 462ms
tacticAnalysis 131ms
type checking 117ms
typeclass inference 499ms
real 2.54
user 3.54
sys 0.79
LeanPool/NashWilliams/Order/WellQuasiOrder.lean
import took 859ms
cumulative profiling times:
elaboration 0.135ms
import 859ms
initialization 32.6ms
interpretation 107ms
linting 0.325ms
module linting 0.00155ms
overlappingInstancesLinter 0.446ms
parsing 0.0307ms
tacticAnalysis 1.15ms
real 1.57
user 0.87
sys 0.71
LeanPool/NashWilliams/Order/WellQuasiOrder/Basic.lean
import took 851ms
cumulative profiling times:
attribute application 0.0377ms
congr simp thm 0.0775ms
elaboration 10.5ms
fix level params 0.111ms
import 851ms
initialization 29.3ms
instantiate metavars 0.219ms
interpretation 161ms
let-to-have transformation 0.0345ms
linting 3.75ms
module linting 0.00142ms
overlappingInstancesLinter 2.58ms
parsing 4.19ms
process pre-definitions 1.03ms
share common exprs 0.338ms
simp 0.613ms
tactic execution 13.1ms
tacticAnalysis 12.3ms
type checking 1.55ms
typeclass inference 2.61ms
real 1.60
user 0.96
sys 0.72
LeanPool/NashWilliams/Order/WellQuasiOrder/Regular.lean
import took 858ms
cumulative profiling times:
attribute application 0.329ms
congr simp thm 1.58ms
elaboration 24.7ms
fix level params 0.413ms
import 858ms
initialization 36ms
instantiate metavars 1.24ms
interpretation 250ms
let-to-have transformation 0.0738ms
linting 15.5ms
module linting 0.00127ms
overlappingInstancesLinter 6.25ms
parsing 14.3ms
process pre-definitions 4.06ms
share common exprs 2.38ms
simp 24.8ms
tactic execution 131ms
tacticAnalysis 32.2ms
type checking 67.3ms
typeclass inference 75.6ms
real 1.78
user 1.37
sys 0.74
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All six headline declarations match their informal statements, with the relevant front, infinitude, finiteness, 2-BQO, and preorder assumptions disclosed. |
| Novelty | ✅ pass |
No Mathlib search hit or existing pooled project proves any of the six headline results. |
| Significance | ✅ pass |
This is a research-level theory-building project centered on named results in infinitary combinatorics and better-quasi-order theory. |
| Sources | ✅ pass |
The survey and upstream-repository citations are internally consistent, but the diff does not include enough source text to verify the theorem-number and closure-property attributions directly. |
| Code quality (advisory) | 🤔 discuss |
The central lexicographic-sum theorem duplicates the long argument already packaged by the immediately preceding reflector. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The front theorems assume IsFront F M; infinite_ramsey assumes M.Infinite and a finite color type; TwoBQO.wellQuasiOrdered assumes TwoBQO r; TwoBQO.lexSigmaQO assumes the index and every fiber relation are 2-BQO; and TwoBQO.embedForAll_wqo additionally assumes [IsPreorder α r]. The card discloses these conditions. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | infinitary combinatorics and order theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The Lean proves monochromatic restrictions for two- and finite-colorings of fronts, infinite Ramsey for every finite arity, 2-BQO implies WQO, 2-BQO closure for LexSumRelQO, and WQO of infinite sequences under EmbedForAll.
The contribution develops Nash-Williams fronts and ordinal ranks, proves finite-color front homogeneity, and establishes substantial 2-BQO consequences including lexicographic-sum closure and well-quasi-ordering of infinite sequences under embedding.
Code quality findings (1)
- duplicate-proof —
LeanPool/NashWilliams/Order/TwoBQO.lean:360
TwoBQO.lexSigmaQO_reflectprovides exactly the bad-sequence dichotomy needed forTwoBQO.lexSigmaQO, but the latter repeats the perfect/bad split, constant-index test, and dependent constant-fibre construction. This leaves the cast-heavy argument maintained twice. ProveTwoBQO.lexSigmaQOthroughTwoBQO.iff_noBad, invokeTwoBQO.lexSigmaQO_reflect, and usehrorht ito contradict the resulting bad sequence.
Evidence: The reflector starts with
let f₁ : PairSeq ι := fun m n h => (f m n h).1
obtain ⟨e, he, hperf | hbad₁⟩ := PairSeq.perfect_or_bad r f₁
· by_cases hconst : ∀ m n l : ℕ, (hmn : m < n) → (hnl : n < l) →
(f (e m) (e n) (he hmn)).1 = (f (e n) (e l) (he hnl)).1
The following theorem repeats the same setup:
theorem TwoBQO.lexSigmaQO {ι : Type*} (r : ι → ι → Prop) (hr : TwoBQO r) (s : ι → Type*)
(t : ∀ i, s i → s i → Prop) (ht : ∀ i, TwoBQO (t i)) : TwoBQO (TwoBQO.LexSumRelQO r s t) := by
intro f
let f₁ : PairSeq ι := fun m n h => (f m n h).1
obtain ⟨e, he, hperf | hbad⟩ := PairSeq.perfect_or_bad r f₁
· by_cases hconst : ∀ m n l : ℕ, (hmn : m < n) → (hnl : n < l) →
(f (e m) (e n) (he hmn)).1 = (f (e n) (e l) (he hnl)).1
Tokens: 283,199 in / 19,215 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $0.9962
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.
# Conflicts: # LeanPool/projects.yml
Owner
Author
Changes requested by automated reviewReviewed exact head The card says Acceptance condition: either describe this headline precisely as preservation of the pair-sequence Independent rubric evidence: #380 (comment) |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
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
Source and significance
The front definition, rank construction, and Nash-Williams theorem were checked against Definitions 3.11 and 3.16 and Theorem 3.22 of Yann Pequignot, Towards better: A motivated introduction to better-quasi-orders, DOI 10.4171/EMSS/4-2-2. The formalization deliberately proves the finite-rank 2-BQO fragment and does not overclaim full BQO.
Headline results include Front.IsFront.nash_williams, Front.IsFront.nash_williams_fin, infinite_ramsey, TwoBQO.wellQuasiOrdered, TwoBQO.lexSigmaQO, and TwoBQO.embedForAll_wqo.
Integration and optimization
A clean project-only build improved from 9.98 s / 1,995,828 KiB peak RSS to 9.60 s / 1,982,832 KiB after import pruning. The slowest sampled proof was 0.308 s; no proof approached pool limits.
Validation
The upstream verification blocks were removed only after reproducing their axiom results: standard propext/Classical.choice/Quot.sound where used, and no axioms for TwoBQO.wellQuasiOrdered.