Surreal inverse formula in mathlib4 is incorrect

Stream: mathlib4

[Ted Hwa]

The surreal inverse formula defined here as inv' is incorrect. The code for inv':

def inv' : PGame → PGame
  | ⟨_, r, L, R⟩ =>
    let l' := { i // 0 < L i }
    let L' : l' → PGame := fun i => L i.1
    let IHl' : l' → PGame := fun i => inv' (L i.1)
    let IHr i := inv' (R i)
    ⟨InvTy l' r false, InvTy l' r true, invVal L' R IHl' IHr, invVal L' R IHl' IHr⟩

and the typical line for invVal is

def invVal {l r} (L : l → PGame) (R : r → PGame) (IHl : l → PGame) (IHr : r → PGame) :
    ∀ {b}, InvTy l r b → PGame
  -- [...]
  | _, InvTy.left₁ i j => (1 + (R i - mk l r L R) * invVal L R IHl IHr j) * IHr i
  -- [...]

The correct formula as given in ONAG (p. 21 in the second edition) has this typical form:

$$\frac{1 + (x^R - x) y^L}{x^R}$$

The Lean translation is not correct because the parameters passed into invValfrom inv' are not the original l, r, L, R but the modified l', r, L', R where in l', we retain only the positive Left options. This means that the mk l r L R in the formula for invVal is not the original x, but a modified version of x with only the positive Left options.

Thus, for example, if $x = \frac{1}{2} = \{0|1\}$ then the value of mk l r L R in invVal will be $\{ | 1 \} = 0$ not $\frac{1}{2}$.

I will submit a PR to fix this.

cc original authors: @Violeta Hernández @Junyan Xu

[Kevin Buzzard]

I will submit a PR to fix this.

Thanks a lot! That's the best possible last line for a message like this :-)

[Ted Hwa]

Sorry I just noticed the authors I tagged weren't the original authors of this file - I had copied the authors from the Surreal.Multiplication file but inverses are actually defined in the Game.Basic file.

[Mario Carneiro]

is inv proved to be a multiplicative inverse?

[Ted Hwa]

It is not yet proved to be a multiplicative inverse. I was working on that when I discovered this error.

[Ted Hwa]

Fixed in PR #14463

[Mario Carneiro]

Probably better to roll this into the pr for proving it's an inverse then

[Ted Hwa]

The PR for proving it's an inverse might take some time though, since it is going to be a long proof. The PR above is a quick fix. I would prefer to work on my "proving inverse" PR with this correction already in place.

[Junyan Xu]

I'd be inclined to merge the change of the definition and the proof that it works in the same PR. There might be additional bugs in the definition that would only be uncovered by carrying out the proof (even though unlikely), or you might want to change the definition to make the proof smoother. Once you've proven what you defined is an inverse, I think no one would object merging the new definition whatever it ends up to be.

[Ted Hwa]

I have a PR out #14498 for proving it's an inverse. Started a new thread on it here

[Ted Hwa]

Now that we have another PR with a proof that this inverse formula is correct (even though it isn't merged yet), are people more comfortable with this PR #14463 ? Trying to break up the other huge PR with the complete proof, and this seems like a natural splitting point.