Hehe, since you're still on watching, so here the calibration according to ChatGPT, which I like to track: Let T = IZF + AC_{N, 2} (ZF without LEM and but with the capacity of making infinitely many binary choices.) ChatGPT will quickly tell you LPO proves a lot here. Now the principle LLPO lets you stare down an countably infinite abyss and tell you if something happens here or not. T+LLPO still allows you to postulate functions in ℝ→ℝ always to be continuous. (Because reals p can be too complicatedly defined for a computer to decide p>0 in finite time, so "discontinuous functions" can't be evaluated on the actual reals in this framework. They are not functions in the first place.) Hence this theory can't prove a counter-example. If one exists, what does it look like? IZF + "dichotomy for the reals, (p>0 ∨ p=0 ∨ p<0)" lets you show that an open ℝ→ℝ never has an isolated discontinuity. This makes all possible counter-examples disgustingly dense with if-then-else checks about what the return values is. The principle LPO lets you stare down an countably infinite abyss and if something happens, it tells you how deeply it happens, and else it tells you the fact that nothing ever happens. T+LPO proves you can decide membership in the Cantor function, and with it you can prove that relation with the Cantorian cast distinction is a function - and an open one and with those dense discontinuities. en.wikipedia.org/wiki/Limite…