I was not a fan of the writing style of the proof. There seem to be some irrelevant details: Is the mention of 8-flow at all relevant? I, at least, found the definition of L on the first line of the proof of Lemma 2.2 to be needlessly inscrutable, and my thesis advisor would have likely stopped reading there and told me to fix it.
Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)
I was confused at first when you asked if the 8-flow is relevant, when like, the 8-flow is a key input that the cycle double cover is built out of. Then I realized, oh, I guess technically they're not using the 8-flow, they're using the Z_2^3-flow. But like. The existence of an 8-flow and the existence of a Z_2^3-flow are equivalent, and I gather most graph theorists are going to talk about it in terms of the existence of an 8-flow, so noting that having a Z_2^3-flow is equivalent to having an 8-flow helps the reader to put this information in context.
I'm not sure why you find this proof so hard to read. I found it mostly quite readable (and the definition of L is straightforward? I wouldn't have written it quite that way but it's hardly inscrutable), although I feel like some parts are maybe lacking some exposition to explain the reason for certain things -- it doesn't feel written "in order". I also don't like that it's not cleanly separated into theorems and proofs -- some of the proof occurs in parts that aren't set off, for instance, and there isn't even a proper main theorem statement! But overall I was able to get through it without a lot of trouble and I'm not even a graph theorist...
My issues with the definition of L are mostly about the order in which things are written.
L(t, epsilon)_e breaks down the range of L onto its component values indexed by edge, but this only really makes sense when you know that t and epsilon are. They are sort of defined in the middle of a sentence in the proof of 2.1, which IMO is asking a lot of the reader, and this sort of sloppiness is a way that errors can hide in a proof. (Not that I see an error here. But a formalization in Lean or whatever would not get away with this.)
And, in the same definition of L, for some reason the e=uv part comes at the end only after u and v are used.
What would be wrong with stating, in the definition, what sorts of objects t and epsilon are and with omitting e entirely in favor of just calling the edge uv everywhere?
Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)