Exact derivative coordinates of genuine Sobolev word blocks.

theorem EulerSobolevWordBlocks.wordBlock_word (period : ℝ) [Fact (0 < period)] (q n : ℕ) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + n))) {m : ℕ} (hm : m ≤ q) (v : Fin m → Fin 4) : EulerCylinderSobolevSpace.word period ((wordBlock period q n w) u) hm v = EulerCylinderSobolevSpace.word period u ⋯ (Fin.append v w)

Every derivative coordinate of a true word block is the corresponding concatenated original word.