Octonions

Stream: mathlib4

[Mr Proof]

Anyone yet tried formalising octonions in Lean? I might like to try doing that as an exercise.

Why are they interesting you may ask?

• They are related to the exceptional lie groups. e.g. G2 is the automorphism group of the algebra
• They can be used to construct the exceptional Jordan Algebra
• Is related to the 7 dimensional cross product
• Can be used to construct the Freudenthal magic square

Are there any pitfalls you can see? For example they are non-associative (ab)c != a(bc) in general.

I wonder if it is best to use the Cayley–Dickson construction. I think probably not.

---

On a different note. Looking at the Quaternion functions in Lean there seems to be a separate function for each imaginary part e.g.

QuaternionAlgebra.sub_imI
QuaternionAlgebra.sub_imJ
QuaternionAlgebra.sub_imK

So when doing the octonions this will be 7 functions. Is this really the most efficient API? :thinking:

[Mario Carneiro]

cayley-dickson seems like a much more efficient route here

[Mr Proof]

Yes, although it does kind of artificially split the octonion into two sets of 4 so breaks a bit of the symmetry. But it's maybe that doesn't matter.

[Mario Carneiro]

I'm not sure I would call that breaking the symmetry. S^2 is a subgroup of the symmetries...

[Utensil Song]

Judging by Baez, J. (2002). The octonions, Cayley-Dickson construction is quite natural, and such a inductive construction should help the proofs in principle.

As for the quaternion algebra construction approach in Lean, I've experiment it a while ago, and I seem to have difficulty generalize it to, say, octonion, or Dirac algebra. The approach seems to be very specific to quaternions.

[Mr Proof]

I think one way would be to store the octonion as a struct with 8 separate numbers. But then have a function that converts that into two quaternions to do the multiplications etc. And vice versa.

I wonder how much work it would be to do a proof that G2 is automorphism group for octonions. It looks like you can define exceptional lie groups already. The proofs I've seen seem to rely on the fact that G2 is the only simple lie algebra of dimension 14. Would be quite a challenge :thinking:(well I suppose unless you actually defined G2 that way) But I'm thinking too far ahead...

[Kim Morrison]

I did Cayley-Dickson long ago in Lean 3. It is easy, fun, and the right way to do the octonions. :-)

[Kevin Buzzard]

Just to throw a spanner into the works, the group scheme G2 has a model over Z and in particular it works in characteristic 2. Lean's definition of quaternions isn't good in characteristic 2, there are quaternion algebras in characteristic 2 which we can't express in lean with the current constructor because we demand $i^2=r$ rather than the more general $i^2+si=r$.

[Kevin Buzzard]

This comment also applies to the theory of quadratic algebras which we have, which has notation $\Z[\sqrt{d}]$ so you can guess the definition. Bourbaki's constructor for quadratic algebras allows $i^2+si=r$ and were it to do octonions I'm sure it would also allow this level of generality. Which will make the algebra much worse.

[Scott Carnahan]

Marty Weissman has a very brief treatment in pages 1 and 3 of this 2009 talk. Naturally, many details need to be filled in.

[Oliver Nash]

@Filippo A. E. Nuccio supervised a project during the Machine Checked Mathematics conference at the Lorentz Center last July in which the Octonions were constructed as a star algebra via Cayley-Dickson. I’m afraid I don’t know what happened to the code (which was Lean 4) but it must be somewhere!

[Mr Proof]

Talking of exceptional objects, just thought I'd share this mind map of how some of these things fit together. Not sure all the arrows are correct but, it gives a nice overview:
https://upload.wikimedia.org/wikipedia/commons/thumb/7/7c/Exceptionalmindmap2.png/900px-Exceptionalmindmap2.png

Which reminds me that do we have Hurwitz quaternions in Lean yet?

[Scott Carnahan]

In that chart, the "monster vertex algebra" (top left) is more or less the same thing as "monster CFT" (bottom right).

[Mr Proof]

Interesting. Yeah I wouldn't trust the chart completely. But more as an aid to see what kind of things are missing. Mind you some of the things at the top would be related to the ones at the bottom via compactification. e.g. Monstrous Moonshine and all that.

Another thing that might be missing in Lean is Eiseinstein integers. Z[ω:ω^3=1]. Wonder if that should be it's own type as we already have GaussianInt. Not sure the best way to formalise that is though :thinking:

[Ruben Van de Velde]

We've got Hurwitz quaternions in flt

[Kevin Buzzard]

Feel free to upstream them if you need them!

[Mr Proof]

Here's my script for doing evaluations with octonions [Updated 17 June] Excuse my code, I am just learning.

I just did it the hard way instead of using quaternions. I used the multiplication ordering e[n]*e[n+1]=e[n+3] since this is a way to have a cyclic ordering. (Possibly there is a way to shorten the script making use of cyclic ordering?)

I'm not sure how to define addition and multiplication so it works with both Rat and Int types. Is there a way to do union types? Also I can't do the O notation for octonions :smiling_face_with_tear:

Maybe I'll try and do a proof that this is equivalent to the Cayley-Dickson construction :check:....

import Mathlib

/-

An definition of the Octonion Algebra over field F denoted by 𝕆[F]
Includes proof of Cayley Dickson construction

-/

open Quaternion


structure Octonion (α : Type u) where
  re: α
  e1: α
  e2: α
  e3: α
  e4: α
  e5: α
  e6: α
  e7: α

/- Alternertive names: e1=i, e2=j, e3=Ii, e4=k, e5=Ik, e6=Ij, e7=I  -/


/- Notation and output -/

notation "𝕆" => Octonion ℝ

notation "𝕆[" F "]" => Octonion F

instance [Repr α] : Repr (Octonion α) :=
  { reprPrec := fun q _ => s!"({repr q.re} + {repr q.e1}*e1 + {repr q.e2}*e2 + {repr q.e3}*e3 + {repr q.e4}*e4 + {repr q.e5}*e5 + {repr q.e6}*e6 + {repr q.e7}*e7)" }

/- Construct from a pair of Quaternions-/
/- Many equivalent permuations are possible (which form a group)-/

def octFromQuat [Field α]: (ℍ[α] × ℍ[α])-> 𝕆[α] := fun (q,p) =>
   ⟨q.re, q.imI, q.imJ, -p.imI, q.imK, -p.imK, -p.imJ, p.re⟩

def quatFromOct [Field α]: 𝕆[α]-> (ℍ[α] × ℍ[α]) := fun q =>
  ( ⟨q.re,q.e1,q.e2,q.e4⟩, ⟨q.e7, -q.e3, -q.e6,-q.e5⟩ )

/- Prove these are inverses -/

def quatFromOctInverseOctFromQuat [Field α]: forall (A B:ℍ[α]), (A,B) = quatFromOct (octFromQuat (A,B)) := by
intro a b
simp[octFromQuat,quatFromOct]


def octFromQuatInverseQuatFromOct [Field α]: forall (A:𝕆[α]), A = octFromQuat (quatFromOct A) := by
intro a
simp[quatFromOct,octFromQuat]

/- boolean equality -/


def Octonion.bequal {α : Type} [DecidableEq α]: (p q: 𝕆[α]) -> Bool := fun p q =>
    p.e1 == q.e1 &&
    p.e2 == q.e2 &&
    p.e3 == q.e3 &&
    p.e4 == q.e4 &&
    p.e5 == q.e5 &&
    p.e6 == q.e6 &&
    p.e7 == q.e7



/- conjugation-/

protected /- should it be protected? -/
def Octonion.star {α : Type} [Field α] (p : 𝕆[α]) : 𝕆[α] :={
    re := p.re
    e1 := -p.e1
    e2 := -p.e2
    e3 := -p.e3
    e4 := -p.e4
    e5 := -p.e5
    e6 := -p.e6
    e7 := -p.e7
}


def Octonion.add {α : Type} [Field α] (p q : 𝕆[α]) : 𝕆[α] :={
    re := p.re + q.re
    e1 := p.e1 + q.e1
    e2 := p.e2 + q.e2
    e3 := p.e3 + q.e3
    e4 := p.e4 + q.e4
    e5 := p.e5 + q.e5
    e6 := p.e6 + q.e6
    e7 := p.e7 + q.e7
}

def Octonion.sub {α : Type} [Field α] (p q : 𝕆[α]) : 𝕆[α] :={
    re := p.re - q.re
    e1 := p.e1 - q.e1
    e2 := p.e2 - q.e2
    e3 := p.e3 - q.e3
    e4 := p.e4 - q.e4
    e5 := p.e5 - q.e5
    e6 := p.e6 - q.e6
    e7 := p.e7 - q.e7
}



/- This is using a cyclic order of multiplication such that e[n]*e[n+1]=e[n+3]    -/
/- Therefore a subgroup of quaternions could be using a+b*e1+c*e2+d*e4 for example  -/

def Octonion.mul {α : Type} [Field α] (p q : 𝕆[α]) : 𝕆[α] := {
    re := p.re*q.re - p.e1*q.e1 - p.e2*q.e2 - p.e3*q.e3 - p.e4*q.e4 - p.e5*q.e5 - p.e6*q.e6 - p.e7*q.e7

    e1 := p.re*q.e1 + p.e5*q.e6 + p.e2*q.e4 + p.e3*q.e7    +    p.e1*q.re - p.e6*q.e5 - p.e4*q.e2 - p.e7*q.e3
    e2 := p.re*q.e2 + p.e6*q.e7 + p.e3*q.e5 + p.e4*q.e1    +    p.e2*q.re - p.e7*q.e6 - p.e5*q.e3 - p.e1*q.e4
    e3 := p.re*q.e3 + p.e7*q.e1 + p.e4*q.e6 + p.e5*q.e2    +    p.e3*q.re - p.e1*q.e7 - p.e6*q.e4 - p.e2*q.e5
    e4 := p.re*q.e4 + p.e1*q.e2 + p.e5*q.e7 + p.e6*q.e3    +    p.e4*q.re - p.e2*q.e1 - p.e7*q.e5 - p.e3*q.e6
    e5 := p.re*q.e5 + p.e2*q.e3 + p.e6*q.e1 + p.e7*q.e4    +    p.e5*q.re - p.e3*q.e2 - p.e1*q.e6 - p.e4*q.e7
    e6 := p.re*q.e6 + p.e3*q.e4 + p.e7*q.e2 + p.e1*q.e5    +    p.e6*q.re - p.e4*q.e3 - p.e2*q.e7 - p.e5*q.e1
    e7 := p.re*q.e7 + p.e4*q.e5 + p.e1*q.e3 + p.e2*q.e6    +    p.e7*q.re - p.e5*q.e4 - p.e3*q.e1 - p.e6*q.e2
}


def Octonion.scale {α : Type} [Field α] (r:α) (p: 𝕆[α]):𝕆[α] := {
    re := r * p.re
    e1 := r * p.e1
    e2 := r * p.e2
    e3 := r * p.e3
    e4 := r * p.e4
    e5 := r * p.e5
    e6 := r * p.e6
    e7 := r * p.e7
}


/- overload the operators -/

instance [Field α]: Add 𝕆[α] where
  add := Octonion.add

instance [Field α]: Sub 𝕆[α] where
  sub := Octonion.sub

instance [Field α]: Mul 𝕆[α] where
  mul := Octonion.mul

instance [Field α]: SMul α 𝕆[α] where
  smul := Octonion.scale

instance [DecidableEq α]: BEq 𝕆[α] where
  beq := Octonion.bequal

instance [Field α]: Star 𝕆[α] where
  star := Octonion.star


def Octonion.norm {α : Type} [Field α] [StarRing α] (p: 𝕆[α])  : α :=
  p.re * (star p.re) + p.e1* (star p.e1) + p.e2* (star p.e2) + p.e3* (star p.e3) + p.e4* (star p.e4) + p.e5*(star p.e5) + p.e6*(star p.e6) + p.e7*(star p.e7)

def Octonion.reciprocal {α : Type} [Field α] [StarRing α] ( P : 𝕆[α]) : 𝕆[α] := Octonion.scale (1/(Octonion.norm P)) (star P)


/- Proofs -/

/-- do I really have to do this? --/
@[simp] theorem Octonion.mul_eq {α : Type} [Field α] (p q : 𝕆[α])  : p * q = ⟨
    p.re*q.re - p.e1*q.e1 - p.e2*q.e2 - p.e3*q.e3 - p.e4*q.e4 - p.e5*q.e5 - p.e6*q.e6 - p.e7*q.e7,
    p.re*q.e1 + p.e5*q.e6 + p.e2*q.e4 + p.e3*q.e7    +    p.e1*q.re - p.e6*q.e5 - p.e4*q.e2 - p.e7*q.e3,
    p.re*q.e2 + p.e6*q.e7 + p.e3*q.e5 + p.e4*q.e1    +    p.e2*q.re - p.e7*q.e6 - p.e5*q.e3 - p.e1*q.e4,
    p.re*q.e3 + p.e7*q.e1 + p.e4*q.e6 + p.e5*q.e2    +    p.e3*q.re - p.e1*q.e7 - p.e6*q.e4 - p.e2*q.e5,
    p.re*q.e4 + p.e1*q.e2 + p.e5*q.e7 + p.e6*q.e3    +    p.e4*q.re - p.e2*q.e1 - p.e7*q.e5 - p.e3*q.e6,
    p.re*q.e5 + p.e2*q.e3 + p.e6*q.e1 + p.e7*q.e4    +    p.e5*q.re - p.e3*q.e2 - p.e1*q.e6 - p.e4*q.e7,
    p.re*q.e6 + p.e3*q.e4 + p.e7*q.e2 + p.e1*q.e5    +    p.e6*q.re - p.e4*q.e3 - p.e2*q.e7 - p.e5*q.e1,
    p.re*q.e7 + p.e4*q.e5 + p.e1*q.e3 + p.e2*q.e6    +    p.e7*q.re - p.e5*q.e4 - p.e3*q.e1 - p.e6*q.e2
⟩:=by rfl

/- Proof of Cayley Dickson -/
def cayleyDickson [Field α]: forall A B C D:ℍ[α],
  octFromQuat (A,B) * octFromQuat (C,D)  = octFromQuat (A * C - (star D) * B , D * A + B * (star C)) := by
  intro p q r s
  simp[octFromQuat]
  ring_nf
  simp
/- Q.E.D -/


/-  tests -/

def e1: 𝕆[ℚ] := ⟨0,1,0,0,0,0,0,0⟩
def e2: 𝕆[ℚ] := ⟨0,0,1,0,0,0,0,0⟩
def e3: 𝕆[ℚ] := ⟨0,0,0,1,0,0,0,0⟩
def e4: 𝕆[ℚ] := ⟨0,0,0,0,1,0,0,0⟩
def e5: 𝕆[ℚ] := ⟨0,0,0,0,0,1,0,0⟩
def e6: 𝕆[ℚ] := ⟨0,0,0,0,0,0,1,0⟩
def e7: 𝕆[ℚ] := ⟨0,0,0,0,0,0,0,1⟩


def q:𝕆[ℚ] := Octonion.mk 1 2 3 4 5 6 7 8
def r:𝕆[ℚ] := Octonion.mk 1 2 3 4 3 2 1 2


#eval q + r
#eval q * r
#eval (2:Rat) • q == q + q
#eval star q
#eval Octonion.reciprocal q


#eval e1*e2 /-  e4   -/
#eval e2*e1 /-  -e4  -/
#eval (e1*e2)*e3 /- -e6 -/
#eval e1*(e2*e3) /- +e6  -/

/- more tests -/


instance [Repr α] [One α] [Neg α] : Repr ℍ[α] :=
  { reprPrec := fun q _ => s!"({repr q.re} + {repr q.imI}*I + {repr q.imJ}*J + {repr q.imK}*K)" }


def h:ℍ[ℚ] := ⟨1,2,3,4⟩
def Q:𝕆[ℍ[ℚ]] := ⟨h,h,h,h,h,h,h,h⟩
#eval Q

def Z:𝕆[𝕆[ℚ]]:=⟨e1,e1,e1,e1,e1,e1,e1,e1⟩

[Eric Wieser]

Note you don't need to link to the web editor like that, Zulip inserts the link automatically if you make a code block

[Mr Proof]

OK, now I want to do my first proof on octonions. To prove that the quaternions are a sub-algbera. Here's my starting point (not including the previous definition of octonions):

open Quaternion

def toOctonion: ℍ[ℚ] -> Oct ℚ := fun q=>⟨q.re, q.imI, q.imJ, 0, q.imK, 0, 0, 0⟩

/- some checks-/
def C:ℍ[ℚ] := ⟨1,2,3,4⟩
def D:ℍ[ℚ] := ⟨5,4,2,6⟩
#eval toOctonion (C * D) - (toOctonion C) * (toOctonion D)

/- The proof-/
def qSubAlgebra: forall A B:ℍ[ℚ], (toOctonion A) * (toOctonion B) = toOctonion (A * B) := by
intro p q
simp[toOctonion]
sorry

I'm stuck here because simp[Octonion.mul] doesn't work

[Junyan Xu]

Are octonions an example of a skew monoid algebra #10541? I guess the quaternions must be.

A docstring there says "The associativity of the skewed multiplication depends on the [MulSemiringAction G k] instance" so I think the construction can produce non-associative algebras. For quaternions we'd use G = ℤˣ × ℤˣ and for octonions ℤˣ × ℤˣ × ℤˣ (replace ℤˣ by ZMod 2 if we are to introduce SkewAddMonoidAlgebra ...)

By the way FLT3 has the Eisenstein integers, but they don't fix a particular model. (And I think you mean ℤ[ω] not ℝ[ω].)

[Mr Proof]

OK. With the help of ChatGPT giving some tips, I solved it. But I'm not too happy with the proof. Since I had to write a big lemma which basically is a copy-and-paste of the original definition:

/-- do I really have to do this? --/
@[simp] theorem Octonion.mul_eq (p q : Octonion ℚ)  : p * q = ⟨
    p.re*q.re - p.e1*q.e1 - p.e2*q.e2 - p.e3*q.e3 - p.e4*q.e4 - p.e5*q.e5 - p.e6*q.e6 - p.e7*q.e7,
    p.re*q.e1 + p.e5*q.e6 + p.e2*q.e4 + p.e3*q.e7    +    q.re*p.e1 - q.e5*p.e6 - q.e2*p.e4 - q.e3*p.e7,
    p.re*q.e2 + p.e6*q.e7 + p.e3*q.e5 + p.e4*q.e1    +    q.re*p.e2 - q.e6*p.e7 - q.e3*p.e5 - q.e4*p.e1,
    p.re*q.e3 + p.e7*q.e1 + p.e4*q.e6 + p.e5*q.e2    +    q.re*p.e3 - q.e7*p.e1 - q.e4*p.e6 - q.e5*p.e2,
    p.re*q.e4 + p.e1*q.e2 + p.e5*q.e7 + p.e6*q.e3    +    q.re*p.e4 - q.e1*p.e2 - q.e5*p.e7 - q.e6*p.e3,
    p.re*q.e5 + p.e2*q.e3 + p.e6*q.e1 + p.e7*q.e4    +    q.re*p.e5 - q.e2*p.e3 - q.e6*p.e1 - q.e7*p.e4,
    p.re*q.e6 + p.e3*q.e4 + p.e7*q.e2 + p.e1*q.e5    +    q.re*p.e6 - q.e3*p.e4 - q.e7*p.e2 - q.e1*p.e5,
    p.re*q.e7 + p.e4*q.e5 + p.e1*q.e3 + p.e2*q.e6    +    q.re*p.e7 - q.e4*p.e5 - q.e1*p.e3 - q.e2*p.e6
⟩:=by rfl

/- The proof-/
def qSubAlgebra: forall A B:ℍ[ℚ], (toOctonion A) * (toOctonion B) = toOctonion (A * B) := by
  intro p q
  simp[toOctonion]
  ring_nf
  simp
/- Q.E.D -/

[Mr Proof]

Here is my proof of Cayley-Dickson for my construction:

def pairToOct: ℍ[ℚ]-> ℍ[ℚ] -> Oct ℚ := fun q p =>⟨q.re, q.imI, q.imJ,p.re, q.imK, p.imJ,-p.imK,p.imI⟩

/- The proof-/
def cayleyDickson: forall A B C D:ℍ[ℚ], (pairToOct A B) * (pairToOct C D) = pairToOct (A * C- (star D) * B ) ( D * A + B * (star C)) := by
  intro p q r s
  simp[pairToOct]
  ring_nf
  simp
/- Q.E.D -/

Does this count as a proof? I haven't really shown that pairToOct keeps the same degrees of freedom.

Any feedback and tips on how to improve these proofs welcome :hug: I'm still learning.

[Junyan Xu]

I'd guess those linarith could be replaced by ring which is presumably faster

[Mr Proof]

Yep. Much nicer.

Is that big Octonion.mul_eq really necessary? Seems a bit unnecessary as it's proving a tautology.

[Mr Proof]

My strategy to prove G2 is the automorphism group is as follows using a brute force approach:

• Create a vector E=(e1,e2,e3,e4,e5,e6,e7) of the imaginary components.
• For any small automorphism G (a+b.E + δb.G.E)*(c+d.E + δd.G.E) = (e+f.E + δf.E) + O(δ^2)
• Equating terms should give a restriction on the matrix G of the formG[a,m]f[m,b,c] + G[b,m]f[m,c,a] + G[c,m]f[m,a,b] = 0
• Then using some linear solver it may be possible to show that G has 14 independent components
• Then (somehow) prove it is irreducible
• Then something else
• QED

Since G2 is not already in Lean (?) all we can do at the moment probably the best we can do is prove the automorphism group must have 14 generators.

[Filippo A. E. Nuccio]

This repo contains what had been done during the Leiden workshop. It follows Cayley-Dickson, and I agree this is the right way to go. In particular, I think that we do not need octonions over $\mathbb{Q}$ but over more general algebras over arbitrary fields.

[Filippo A. E. Nuccio]

@Mr Proof I would be very happy to see Octonions in Mathlib, so please do not hesitate to ping me if you have some code to share before/during a mathlib PR.

[Mr Proof]

Thanks @Filippo A. E. Nuccio I'm still learning so my code is not the best.
Talking of arbitrary fields. How could I change this line so it accepts any algebraic field not just the rationals:

def Octonion.add (p q : Octonion ℚ) : Octonion ℚ :={

I need to change it to a general ring.

[Filippo A. E. Nuccio]

Can you provide a #mwe?

[Mr Proof]

Filippo A. E. Nuccio said:

Can you provide a #mwe?

Yes, there is a full example 16th post down from the top.

[Filippo A. E. Nuccio]

So, what you can do is

noncomputable
def Octonion.equal {α : Type} [Field α]: (p q: Octonion α) -> Bool := fun p q =>

to specify that you're working with octonions over a type α that you require to be a field. That being said, this definition is a bit bizarre and the way we'd do this is mathlib is somewhat different, but at least for your question of ℚ vs an arbitrary field, this is the way to go.

[Edward van de Meent]

don't you rather just want to use @[ext] at the definition of your structure? i misunderstood what Octonion.equal means, but still do use @[ext] at the start of your structure.

[Edward van de Meent]

the way we'd do that in mathlib would probably be something like this:

def Octonion.equal {α : Type} [Field α] (p q : Octonion α) : Prop := p.e1 = q.e1 ∧ p.e2 = q.e2 ∧ p.e3 = q.e3 ∧ p.e4 = q.e4 ∧ p.e5 = q.e5 ∧ p.e6 = q.e6 ∧ p.e7 = q.e7

[Edward van de Meent]

note the use of Prop rather than Bool

[Eric Wieser]

Surely we wouldn't have that at all, and would instead write

instance : DecidableEq (Octonion α) := sorry

[Edward van de Meent]

i was confused too, but note the absence of p.re = q.re

[Edward van de Meent]

equal is indeed pretty much a misnomer in this case

[Filippo A. E. Nuccio]

I agree with @Eric Wieser and @Edward van de Meent 's comments, but I had the feeling that the OP requested help on more "fundamental" issues.

[Mr Proof]

Yes, perhaps I have my names wrong. I was using the boolean version of equals. I probably need a propositional version as well (?) I am just doing this as an exercise to practice with Lean.

instance [DecidableEq α]: BEq 𝕆[α] where
  beq := Octonion.equal

I've updated the script recently. (16th post from the top if the link doesn't work). Do you think this is something useful for Lean or would it have to be totally rewritten?

[Eric Wieser]

You get the propositional version for free

[Filippo A. E. Nuccio]

Mr Proof said:

Yes, perhaps I have my names wrong. I was using the boolean version of equals. I probably need a propositional version as well (?) I am just doing this as an exercise to practice with Lean.

instance [DecidableEq α]: BEq 𝕆[α] where
  beq := Octonion.equal

I've updated the script recently. (16th post from the top if the link doesn't work). Do you think this is something useful for Lean or would it have to be totally rewritten?

We will certainly be happy to help you, and in particular consider that using Beq is normally not very encouraged (see the doc at docs#BEq). That being said, can I gently remind you that we encourage users to use their real names rather than nicknames?

[Mr Proof]

Perhaps I just have an apposite aptronym. :thinking:I'll consider that of course... but then what is a real name anyway. :thinking: