It does use a sum of KL divergence errors, but embarrassingly I’m noticing just now that originally the proof implied a bound for weak natural latents (all-but-one redundancy) instead of strong natural latents (any-one-redundancy) which is what I intended. Bound for strong natural latents is underway, I think the proof is pretty quick but lean formalization will take a minute.
The repo is updated with the full redundancy deletion spectrum, so we’ve got formalized proofs of bounds for weak natural latents and strong natural latents and everything in between.
Thanks primarily to GPT 5.6 I’ve got a Lean proof of a bound which works for any number of observables (the bound is in terms of the number of variables): https://github.com/satchlj/general_stoch_to_det
I’ve looked at the formalization of the statements and definitions and am happy with them.
Does it use the sum of KL divergence errors or something else?
It does use a sum of KL divergence errors, but embarrassingly I’m noticing just now that originally the proof implied a bound for weak natural latents (all-but-one redundancy) instead of strong natural latents (any-one-redundancy) which is what I intended. Bound for strong natural latents is underway, I think the proof is pretty quick but lean formalization will take a minute.
The repo is updated with the full redundancy deletion spectrum, so we’ve got formalized proofs of bounds for weak natural latents and strong natural latents and everything in between.