Skip to content

Import Conway refinement for omnific integers #509

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 35 commits into
base: main
Choose a base branch
from
Open

Import Conway refinement for omnific integers #509

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
37cab20
Import Conway refinement for omnific integers with source attribution…
Vilin97 Sep 21, 2026
330d921
Port complete upstream content to current Mathlib and improve lint co…
Vilin97 Sep 21, 2026
8f3738e
Port Conway tensor recursors and algebraic structure interfaces
Vilin97 Sep 21, 2026
935fefd
Port Conway tensor, Hahn-series and game APIs to Lean 4.34
Vilin97 Sep 21, 2026
701bd50
Repair Conway graded coefficients and principal tensor representations
Vilin97 Sep 21, 2026
cf0cffc
Update Conway germ coefficients and graded tensor assumptions
Vilin97 Sep 21, 2026
b2ff9c1
Port Conway normal forms and downstream divisor interfaces
Vilin97 Sep 22, 2026
2e8019a
Restore transfinite normal-form recursion and boundary orders
Vilin97 Sep 22, 2026
8f42274
Port Conway coefficient APIs and preserve signature fixtures
Vilin97 Sep 22, 2026
dd6732a
Clean Conway import warnings and document the complete API
Vilin97 Sep 22, 2026
63bd538
Finish Conway proof refactors and strict quality audits
Vilin97 Sep 22, 2026
c1d5bd8
Isolate Conway quotient games from existing pool games
Vilin97 Sep 22, 2026
a0ecb11
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 22, 2026
85b7729
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 23, 2026
bbe32e0
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 24, 2026
d5d9790
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 24, 2026
7a56eb0
Restore project registration lost during automatic main merge
Vilin97 Sep 24, 2026
eae96d0
Isolate Conway OfSets tactic syntax within the pool
Vilin97 Sep 25, 2026
a4932bf
Migrate Conway import aggregators to Lean modules
Vilin97 Sep 25, 2026
5d2e114
Sync current main and preserve complete Conway project card
Vilin97 Sep 25, 2026
67f8a56
Correct ordinal-value multiplication citation
Vilin97 Sep 25, 2026
03255d3
Merge current main while preserving the complete project registry
Vilin97 Sep 25, 2026
7b105e6
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
70b06df
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
dcb4735
refactor(ConwayRefinement): focus the public umbrella
Vilin97 Sep 26, 2026
dd81bfe
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 26, 2026
6877ffa
Merge current main without changing project claims or gates
Vilin97 Sep 26, 2026
3010605
Merge current main without changing project claims or gates
Vilin97 Sep 26, 2026
bed4d89
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 26, 2026
6660b83
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 26, 2026
981996b
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 26, 2026
9bc8b95
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot] Sep 26, 2026
b7a2a4e
refactor(ConwayRefinement): bridge directly to shared surreal foundat…
Vilin97 Sep 26, 2026
f044cde
Merge remote-tracking branch 'origin/main' into HEAD
Vilin97 Sep 26, 2026
c59d7d3
Merge commit 'refs/review-reconcile-20260926/final509' into HEAD
Vilin97 Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
774 changes: 774 additions & 0 deletions LeanPool.lean
View file
Open in desktop

Large diffs are not rendered by default.

20 changes: 20 additions & 0 deletions LeanPool/ConwayRefinement.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
/-
Copyright (c) 2026 Dan Abramov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dan Abramov
-/

module

public import LeanPool.ConwayRefinement.Solution

/-!
# Conway refinement for omnific integers

Source: url:https://github.com/gaearon/conway-refinement
Authors: Dan Abramov
Status: verified
Main declarations: `ConwayRefinement.Palomar.conwayRefinement`
Tags: surreal-numbers, ordered-algebra, factorization
MSC: 06A05, 13F25
-/
15 changes: 15 additions & 0 deletions LeanPool/ConwayRefinement/CombinatorialGames.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
/-
Copyright (c) 2026 Dan Abramov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dan Abramov
-/

module

public import LeanPool.ConwayRefinement.CombinatorialGames.Game
public import LeanPool.ConwayRefinement.CombinatorialGames.Mathlib
public import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal
public import LeanPool.ConwayRefinement.CombinatorialGames.Surreal
public import LeanPool.ConwayRefinement.CombinatorialGames.Tactic

/-! Supporting modules for Conway refinement for omnific integers. -/
18 changes: 18 additions & 0 deletions LeanPool/ConwayRefinement/CombinatorialGames/Game.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
/-
Copyright (c) 2026 Dan Abramov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dan Abramov
-/

module

public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Basic
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Birthday
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Classes
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Functor
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.IGame
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Ordinal
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Player
public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Special

/-! Supporting modules for Conway refinement for omnific integers. -/
Loading
Loading