Correctness of Cowlishaw's ten-bit declet table

Encoding a value below 1000 produces a ten-bit declet whose decoding recovers all three decimal digits. Re-encoding a ten-bit pattern clears the ignored high bits precisely in the redundant cases.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeDeclet_lt (n : ℕ) : encodeDeclet n < 1024

The canonical encoding uses at most ten bits.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeDeclet_lt (n : ℕ) : decodeDeclet n < 1000

Every ten-bit pattern denotes three decimal digits.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeDeclet_encodeDeclet (n : ℕ) (h : n < 1000) : decodeDeclet (encodeDeclet n) = n

The DPD table preserves all three input digits.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeDeclet_decodeDeclet (n : ℕ) (h : n < 1024) : encodeDeclet (decodeDeclet n) = if n / 2 % 8 = 7 ∧ n / 32 % 4 = 3 then n % 256 else n

The only redundant declets have all three digits in {8, 9}. The canonical representative clears the two ignored high bits, as required by IEEE 754-2019 Tables 3.3–3.4; every other ten-bit pattern is already canonical.