Conway's Refinement Conjecture for Omnific Integers

The repository gives a Lean proof of Conway's 1976 refinement conjecture for omnific integers: whenever $$ab=cd$$ with $a,b,c,d\in\mathbf{Oz}$, there exist $e,f,g,h\in\mathbf{Oz}$ satisfying $$a=ef,\quad b=gh,\quad c=eg,\quad d=fh.$$ The proof is formalized twice: once using CombinatorialGames' surreal-number implementation and once with the required surreal definitions inlined over Mathlib. The development also proves stronger structural results about factorization in Hahn-series integer parts and related generalized power-series rings.

The repository gives a Lean proof of Conway's 1976 refinement conjecture for omnific integers: whenever $$ab=cd$$ with $a,b,c,d\in\mathbf{Oz}$, there exist $e,f,g,h\in\mathbf{Oz}$ satisfying $$a=ef,\quad b=gh,\quad c=eg,\quad d=fh.$$ The proof is formalized twice: once using CombinatorialGames' surreal-number implementation and once with the required surreal definitions inlined over Mathlib. The development also proves stronger structural results about factorization in Hahn-series integer parts and related generalized power-series rings.