Import Conway refinement for omnific integers - #509

Open

Vilin97 wants to merge 35 commits into

mainfrom

codex/import42-conway-refinement

Commits on Sep 21, 2026

Import Conway refinement for omnific integers with source attribution and complete production scope
Vilin97
committed
37cab20
Port complete upstream content to current Mathlib and improve lint compliance
Vilin97
committed
330d921
Port Conway tensor recursors and algebraic structure interfaces
Vilin97
committed
8f3738e
Port Conway tensor, Hahn-series and game APIs to Lean 4.34
Vilin97
committed
935fefd
Repair Conway graded coefficients and principal tensor representations
Vilin97
committed
701bd50
Update Conway germ coefficients and graded tensor assumptions
Vilin97
committed
cf0cffc

Commits on Sep 22, 2026

Port Conway normal forms and downstream divisor interfaces
Vilin97
committed
b2ff9c1
Restore transfinite normal-form recursion and boundary orders
Vilin97
committed
2e8019a
Port Conway coefficient APIs and preserve signature fixtures
Vilin97
committed
8f42274
Clean Conway import warnings and document the complete API
Vilin97
committed
dd6732a
Finish Conway proof refactors and strict quality audits
Vilin97
committed
63bd538
Isolate Conway quotient games from existing pool games
Vilin97
committed
c1d5bd8
Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot]
committed
a0ecb11

Commits on Sep 23, 2026

Merge remote-tracking branch 'origin/main' into pr-509
github-actions[bot]
committed
85b7729

Commits on Sep 24, 2026

Commits on Sep 25, 2026

Commits on Sep 26, 2026