Your paper only claims that those Coq snippets constitute a "constructive proof sketch". Have those formalizations actually been verified, and if so, why not include the results in the paper?

Separately from that, your entire argument wrt Shannon hinges on this notion that it is applicable to "semantic spaces", but it is not clear on what basis this jump is made.