PR #35857: Bijective Base-2 Numeration

Stream: PR reviews

[Alexey Milovanov]

This PR introduces a formalization of the bijective base-2 numeration system. Unlike standard binary representation, bijective base-2 avoids the "leading zeros" problem, providing a strict mathematical bijection between natural numbers (ℕ) and lists of booleans (List Bool). All CI checks are passing. Since I am a new contributor, I would greatly appreciate it if a maintainer could take a look or add the appropriate labels to put it in the review queue.

Thanks!

[Weiyi Wang]

Out of curiosity, is there interesting math theorem related to this?

[Alexey Milovanov]

Weiyi Wang

The main motivation is to provide a canonical, strictly bijective encoding between ℕ and finite boolean strings.

This strict bijection is highly useful for example in
Algorithmic Information Theory (Kolmogorov Complexity):
To formally define the complexity of a natural number K(n),
you need to map it uniquely to a bitstring.