Thank you for the writeup!
What is the benefit if any to reasoning about DAGs as opposed to just reasoning about the {0,1} consensus game as @nrryuya’s writeup does? The latter is much simpler and it definitely seems intuitively that a result on the latter would translate to the LMD GHOST context anyway; there’s even an explicit construction that slightly modifies LMD GHOST to turn it into a series of {0,1} decisions from genesis up until the head.