Computation of a simplified version of the Brunerie Number

[aljungstrom]

In #741 , I constructed a bunch of elements η₁,η₂,η₃,η₄ all corresponding to the Brunerie number. I've played around with them a bit now and managed to get at least η₃ to compute to -2. This definition of the Brunerie number is of course a lot simpler than the original one in Experiments.Brunerie, but it's the only one I've been able to get working. I also had to give another definition of f7. It's a lot less direct but for some reason I can't get it to compute otherwise...

[kangrongji]

Intereseting! Do you think you can simplify it further so that it can be computed?

[mortberg]

Intereseting! Do you think you can simplify it further so that it can be computed?

I'm confused, it does compute very fast? (1 second)

[kangrongji]

Intereseting! Do you think you can simplify it further so that it can be computed?

I'm confused, it does compute very fast? (1 second)

Sorry, I mean the other ones... and even the Brunerie one.

[mortberg]

Intereseting! Do you think you can simplify it further so that it can be computed?

I'm confused, it does compute very fast? (1 second)

Sorry, I mean the other ones... and even the Brunerie one.

Right, maybe this will shed some light on how to get some of the other ones to compute. But I don't think that's super interesting, what matters to me is that we have one version which computes fast and then establish that pi_4(S^3) = Z / brunerie' Z (this second step is still missing, but hopefully doable). All of the other Brunerie numbers should then be provably equal to brunerie', but Cubical Agda can't check this using refl using reasonable amount of time and memory

[kangrongji]

Intereseting! Do you think you can simplify it further so that it can be computed?

I'm confused, it does compute very fast? (1 second)

Sorry, I mean the other ones... and even the Brunerie one.

Right, maybe this will shed some light on how to get some of the other ones to compute. But I don't think that's super interesting, what matters to me is that we have one version which computes fast and then establish that pi_4(S^3) = Z / abs(brunerie') (this second step is still missing, but hopefully doable). All of the other Brunerie numbers should then be provably equal to brunerie', but Cubical Agda can't check this using refl using reasonable amount of time and memory

Oh... My fault! I just take a glimpse on it and I thought η₁,η₂,η₃,η₄ are a series of numbers that leads to the Brunerie number. Now I realize they're all Brunerie numbers. That's very exciting!