Redux: (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent)

Once upon a time, John Wentworth and I thought we had a proof of a very useful looking theorem . We did not have that proof. An important intermediate step was shown [1] to be invalid and the whole thing crumbled and disappeared, never to see the light of day again... [2] Until now! I'd love to say that we came up with an ingenious fix to the old erroneous proof, but unfortunately it turned out to be a really infuriatingly hard nut to crack. Instead I spent the last ~month experimenting with various ways of incorporating frontier LLMs into the proof-making process, specifically with autoformalization and proving in Lean4. (This is, I recently learned, roughly what Resolution is doing.) The result is stated below, and linked at the bottom is a Lean statement+proof of the same. I will not be providing the proof in prose in this post, as it is not suitable for even impolite human company, but it sure does compile and comes out the other side with a machine-certified proof of what sure looks to be an even stronger correctly-expressed statement than the one I was originally aiming for. Take a look at the first section of the old post, (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent) , for exposition on what all is going on here and why. The Statement Let: be any measurable latent variable on finite observables and (with arbitrary cardinalities and ) be any distribution over the observables be an exact deterministic function of the observables which minimizes…