Categorical Completeness and Type-Level Invariants of Bitmapped Vector Tries in Idris 2

Persistent random-access sequences are typically implemented using either balanced trees, incurring logarithmic overhead per operation, or bitmapped vector tries (BVTs), which achieve near-constant amortised performance through wide branching but traditionally rely on runtime bounds checks to guarantee structural safety. This paper presents a formally verified implementation of the 32-way Bitmapped Vector Trie in Idris 2, in which five core structural invariants -- depth-uniformity, fixed branching factor, bounded bitwise indexing, exhaustive pattern matching, and length-indexed buffering -- are encoded directly in dependent types and checked at compile time. We further establish a lawful Monad instance via an induced structure over the canonical list isomorphism, without expanding the implementation to a fully balanced concatenation scheme such as Relaxed Radix Balanced trees. Benchmarks on a Haskell prototype against Data.Sequence and Data.IntMap confirm that the underlying algorithmic behaviour matches theoretical expectations, despite the prototype's raw performance lagging behind mature, optimised libraries.