What's interesting with the Scholze-Stix rebuttal is that (staring from mathematically a long way away) there is a reasonable proof strategy which would fit the Scholze-Stix rebuttal and Mochizuki rejoinder well. The obvious objection to it being right is: well, Scholze-Stix would have seen it, and even if somehow not Mochizuki would have explained it, right? But maybe it is worth posting here, in order that someone explains why it is not what is going on and not correct. So here goes...

Very caricatured, the proof of Mochizuki's Corollary 3.12 is supposed to give two different (complicated) transforms from a set $S$ to a set $T$, along with inequalities regarding an associated parameter $f(t)$, and what comes out for a given $s\in S$ is the inequality $c(x)f(t)\ge d(x)f(t')$. Here $x$ is the arithmetic information which Mochizuki wants to get some control of, and $c$ and $d$ are (`simple') functions which depend on the transforms chosen but not on the $s\in S$.

The obvious way to get something useful out of this is to ask that $t=t'$; this is insisting that the Scholze-Stix diagram is commutative. Then you can cancel the $f(t)$ factor and get an inequality involving $x$. This looks like it's what Mochizuki wants to do (he says the images are the same). One way to get $t=t'$ is to choose a couple of spaces equal (this choice fixes the transforms).

Scholze and Stix find that in this case you get a trivial inequality, and claim that anything else which gets $t=t'$ is likely to give the same result. Mochizuki agrees, and says that the reason is that in this case his transforms don't do anything interesting (he also says the Scholze-Stix choice is essentially the only way to get $t=t'$). This is consistent with Scholze-Stix saying that Mochizuki's use of anabelian geometry doesn't seem to be doing anything.

The other two things Scholze and Stix simplify are `polymorphism' to morphism, which in this caricature means they consider one $s\in S$ as above, where Mochizuki wants to consider all $s\in S$ (polymorphism). And averaging over the result, which is meaningless if you have only one morphism.

But one can also work as follows. Consider all $s\in S$, and you get a collection of inequalities $c(x)f(t)\ge d(x)f(t')$, where $t$ and $t'$ are images of $s$ under Mochizuki's two transforms. If as $s$ ranges over $S$, you get the same collection of elements appearing as $t$ and as $t'$, just permuted, then this is exactly what Mochizuki means by saying the polymorphism images are the same (as sets, even though the individual morphism images aren't the same). In this case, when you average the collection of inequalities, as Mochizuki wants to do, you get an inequality which is useful: the average of the $f(t)$ equals the average of the $f(t')$, because they're the same sum permuted, so you can cancel it and get $c(x)\ge d(x)$, this time (Mochizuki claims) with meaningful content.

This is entirely consistent with Scholze-Stix saying that polymorphisms and averages don't appear to play a role - in this caricature, they would be playing no role in 400+ pages, except exactly at this point.