I had Fable 5.2 cross-check the bounds GPT-6-Astra came up with for the Strang splitting local order

12 Nov, 2026

In an old post, we explored bounds on how high we can make the Strang splitting go if we pick the right decomposition $A=B+C$ given some appropriate matrix $A$. GPT-6 Astra proved upper and lower bounds on the best local order we can get as we increase the dimensionality of $A\in {ℝ}^{n\times n}$.

As Fable 5.2 is available (and discounted), I thought I would have it take a second look at Astra's proof (both for correctness and for simplifications).

The statement was:

Let $M_n$ be the largest finite local order attained by a nonexact Strang splitting of two $n\times n$ Markov generators. One can show that

$$\boxed{2\lfloor \frac{n}{2}\rfloor +1\le M_n\le n(n-1)+1.}$$

Fable 5.2 agrees with the statement and proof and was able to cut out a few things that were superfluous.

The proof is on Github.

Is this useful?

The intermediate results, like the local order criterion, can be useful -- in fact, local orders are how people compare the performance of different splittings in the literature.

The splittings that attain those orders can be unnatural though and are probably not useful.

Is the proof verified?

Only parts of it are lean-verified. The whole proof was checked by two different LLMs (GPT-6-Astra and Fable 5.2). I also checked some of the lemmas, but not the whole argument yet.