# W-Digit Convention

## Abstract

W digits use shifted Fibonacci weights and the canonical Zeckendorf representation.

**Definition 1.1 (Every natural has exactly one canonical W-digit representation).**

Lean statement: `D5/S0/Conventions/WDigits.wEncoding`

*Formalization.* `D5/S0/Conventions/WDigits.wEncoding` (`✓ std3`).

*Source.* Repository-derived.

*Commentary.*

Natural numbers are equivalent to canonical Zeckendorf index lists. IsZeckendorfRep requires every occupied Fibonacci index to be at least two and consecutive occupied indices to differ by at least two; its inverse sums the selected Fibonacci numbers. Thus the equivalence states existence and uniqueness of the binary, nonadjacent W-digit representation, including the empty representation of zero.

`D5/S0/Conventions/WDigits` fixes the zero-based weights `W(k)=F(k+2)`, hence `1,2,3,5,...`. A digit string is represented by its occupied Fibonacci indices.

The module delegates the canonical algorithm and proof to mathlib's Zeckendorf development. It exposes the three repository-facing facts: indices are nonadjacent, decoding returns the original natural number, and no other canonical list decodes to the same value.

## References

- Truth anchor: `D5/S0/Conventions/WDigits.wEncoding`