Nice! I just happened to write a post expressing similar ideas, with a more concrete construction, at the same time: A model for stage 4 "tightly coupled" sharding plus full Casper
I’m actually not too worried about data availability proofs, at least in the short term, because we can just use an honest majority substitute in the short term. In my model, the fork choice rule for the main chain is driven largely by collations, and collations are implicitly endorsements of the chain, so if you are considering building on some chain, you could simply verify the availability of the last, say, 100 collations that have been built on the chain, and trust everything before then. In the long term, I agree better data availability checking constructions would massively improve the scheme and possibly let it scale super-quadratically.