Certified Constructive Box Embeddings for DAG Taxonomies

Embeddings of a taxonomy are usually trained. However, containment holds only up to a residual error, and the geometry reflects the frequencies in the training data. A geometry compiled from the order structure alone can guarantee two properties that no trained embedding offers: certified zero violations on a declared pair family, and retrieval rankings that no corpus frequency has shaped. We build on GRAIL, a classic reachability index that labels each node of a DAG with one interval per random linear extension, and we lift this labelling into the representation space. Instead of drawing extensions at random, we select each embedding dimension as a witness that separates specific pairs from a declared disjointness family. The resulting box embedding has certified zero containment and separation violations on that family, attested by a machine-checkable certificate that any third party can re-verify. Randomised GRAIL labels remain nonzero even at four times the dimension budget, and gradient-trained box baselines leave residual violations even when trained to fit the full graph. Because the geometry never sees a corpus, ranking by box volume never buries rare, specific concepts on GO, MeSH, or WordNet, while every similarity-based ranker prefers popular ones, at retrieval utility matching an oracle prefilter. Construction takes seconds, and full Gene Ontology under $P_2$, with $3.6\times 10^8$ separation pairs, builds in $28$s. The containment slack between two boxes also predicts held-out edges. Compared with fairly tuned baselines on three datasets, its AUC is higher on the densely multi-parent MeSH, on par on GO, and lower on the nearly tree-shaped WordNet. Symbolic graph features remain above every embedding method. With no task-specific training, the same slack tracks graded lexical entailment on HyperLex at $\rho =0.761$.