Let D̂ₙʳaw be the full-reflection Coxeter cover of W (Dₙ) with only thepairwise Coxeter-order relations, and let Kₙʳaw = ker (D̂ₙʳaw → W (Dₙ) ). We determine the integral first homology of Kₙʳaw for every n ≥ 5: H₁ (Kₙʳaw; Z) ≅ Z^ ( (n−2) (3n² − 2n + 1) /2) ⊕ (Z/2) ^ (n (n−2) ). The proof separates an integral localization theorem from a modular countingtheorem. First, one label orbit of the standard R₁ fork relation saturates the full forkdefect in first homology; the resulting target is torsion-free, so the rawtorsion is elementary 2-torsion and is generated by five-coordinate D₅subsystems. Second, the torsion is presented by a permutation module on formal R₁ classesmodulo three local relation orbits T, M₀, M₁. A finite exact D₅ rewritecertificate gives an all-rank normal-form induction, while a signed-reflectiondetector leaves one universal formal class κₙ unresolved. An explicit all-ncrossed cocycle evaluates nontrivially on κₙ, proving that no hidden relationremains. The only computer-assisted proof inputs are finite exact D₅ certificates; everypassage from D₅ to arbitrary Dₙ is symbolic. The rational multiplicities are quoted from the companion paper (doi: 10. 5281/zenodo. 21966004) and are not reproved here.
Sana Kamiki (2026) studied this question.