The next transcendental is at most SVO

Stream: combinatorial-games

[Violeta Hernández]

I felt like it'd be appropriate to put this in a separate thread to the #combinatorial-games > Nimbers thread. An acquaintance (Rachel L. A. Hunter) recently communicated a proof that every nimber of the form φ(1@ω, x@0) is transcendental (where the notation is Veblen's multivariate function). In particular, the next transcendental is at most the Small Veblen Ordinal, giving a partial answer to a conjecture by Lenstra. I've gone over the proof and though I can't say I completely grasp it, it does seem correct.

[Violeta Hernández]

Here's the document, shared with permission: nimtrans.pdf

[Violeta Hernández]

For reference, here's a Lean definition of the multivariate Veblen function. The description on Wikipedia is kind of confusing, though admittedly so is this.

import Mathlib.Data.Finset.Max
import Mathlib.Data.Finsupp.Single
import Mathlib.SetTheory.Ordinal.Veblen

namespace Ordinal

noncomputable def veblen₀ (f : Ordinal →₀ Ordinal) : Ordinal :=
  let g := f.erase 0
  if hg : g = 0 then ω ^ f 0 else
    let e := g.support.min' (Finsupp.support_nonempty_iff.2 hg)
    derivFamily
      (fun (x : Set.Iio (f e) × Set.Iio e) o ↦ veblen₀ ((g.update e x.1).update x.2 o)) (f 0)
termination_by f -- with colex order
decreasing_by sorry

end Ordinal

The notation (a₁@b₁, ..., aₙ@bₙ) is simply the finitely supported function with f(aᵢ) = bᵢ and f(x) = 0 otherwise.

[Violeta Hernández]

The secret sauce here is the definition $C(\alpha, p)$. For $p$ a nimber polynomial whose coefficients are less than $\alpha$, this is the smallest nimber $F\ge\alpha$ such that every non-constant polynomial $q : F[X]$ with $q < p$ contains a root/splits in $F$.

She proves by induction on $p$ that if $p_0=0$, then $\alpha < \varphi(p_n,\ldots,p_1,\beta)$ implies $C(\alpha,p)\le \varphi(p_n,\ldots,p_1,\beta)$. Which then straightforwardly implies the claimed result.

[Violeta Hernández]

If I'm not mistaken, her proof in fact proves the stronger statement that $\alpha<\varphi(p_n,\ldots,p_1,\beta)$ implies $C(\alpha,p)\le\varphi(p_n,\ldots,p_1,\beta+p_0)$, where of course $p_0$ can now be anything else.

[Aaron Liu]

I guess I can try porting it to Lean

[Violeta Hernández]

Well, I would like to be methodic about this.

[Aaron Liu]

what does that mean

[Violeta Hernández]

I would like to first distill the argument into its bare components

[Violeta Hernández]

I think there's a lemma about $C(\alpha,p)$ which goes implicit in the document but which we probably want to show explicitly. Again, assume that I'm not mistaken.

Let $p$ be a nimber polynomial and let $\alpha$ be larger than all its coefficients. Let $d$ be the "co-degree" of $p$, i.e. the index of the least non-zero coefficient. Define $\alpha_0=\alpha$ and $\alpha_{n+1}=\bigsqcup_q C(\alpha_n,q)$ where $q:\alpha_n[X]$ goes over all polynomials with $q<p$ and where $p_k=q_k$ for every $k>d$. Define $\alpha_\omega$ as the supremum of $\alpha_n$ for $n : \mathbb N$. Then $C(\alpha,p)\le \alpha_\omega$.

[Violeta Hernández]

I think that this lemma allows us to unify the $m=0$ and $m>0$ successor cases in the document.

[Violeta Hernández]

Oh and of course. Before we do any of this we'd have to formalize Veblen's multivariate function itself. I think I can take care of that.

[Aaron Liu]

Violeta Hernández said:

For reference, here's a Lean definition of the multivariate Veblen function. The description on Wikipedia is kind of confusing, though admittedly so is this.

this is the first definition I've seen that I can remember and not have to go back and look it up

[Violeta Hernández]

Veblen's multivariate function is just inherently confusing I think

[Violeta Hernández]

φ(1, 0, 0) is a fixed point of φ(-, 0) though not necessarily of φ(x, -)

[Aaron Liu]

unfortunately it doesn't seem to define the correct function

[Violeta Hernández]

my definition or Wikipedia's?

[Aaron Liu]

your definition

[Aaron Liu]

No maybe I just misread it

[Aaron Liu]

no this is probably fine

[Aaron Liu]

no yeah this is fine

[Aaron Liu]

it's so confusing

[Aaron Liu]

I'm confirming everything up to $\Gamma_0$ and then I will assume it's correct

[Violeta Hernández]

wouldn't $\Gamma_0$ be the case where $p$ is a linear polynomial which is trivial anyways?

[Aaron Liu]

confirming the output of your definition of Veblen

[Violeta Hernández]

ah

[Aaron Liu]

It seems to be doing fine

[Aaron Liu]

I'm guess the first thing to do is to prove the Veblen function terminates then?

[Violeta Hernández]

Well

[Violeta Hernández]

What we really need to do is define the order instance for docs#Colex of a docs#Finsupp

[Violeta Hernández]

the API should be pretty much copy and paste from the docs#Lex API

[Violeta Hernández]

I think it's not particularly controversial to say the multivariate Veblen function belongs in our repo rather than Mathlib

[Violeta Hernández]

I'm currently working on PR-ing the Preorder (Colex (α →₀ β)) instance to Mathlib

[Violeta Hernández]

Once we have that it shouldn't be very difficult to prove termination

[Violeta Hernández]

This might take a while
image.png

[Violeta Hernández]

Turns out there's way more dependent PRs for this colex stuff than I was anticipating. What do you think about just putting it in our repo for the time being?