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.
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.