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.
But the paper doesn’t just restate Shannon.
It extends this very formalism to semantic spaces where the symbol set itself becomes unstable. These situations arise when (a) entropy is calculated across interpretive layers (as in LLMs), and (b) the probability distribution follows a heavy-tailed regime (α ≤ 1). Under these conditions, entropy divergence becomes mathematically provable.
This is far from being metaphorical: it’s backed by formal Coq-style proofs (see Appendix C in he paper).
AND: it is exactly the mechanism that can explain the Apple-Papers' results