Fixed-width signed measurement values

measurementValues c D j decodes c little-endian digits in radix 2 * D + 1, shifted by -D. The result is runtime list data, including at D = 0 (radix one) and c = 0. This is the measurement-VALUE box, not a tuple of formal monomial exponents.

def Cslib.Radix.measurementValues (c D j : ℕ) : List ℤ

Decode a runtime number of signed measurement coordinates using the existing radix digits.

@[simp]

theorem Cslib.Radix.length_measurementValues (c D j : ℕ) : (measurementValues c D j).length = c

The tuple keeps its full declared dimension, including zero entries.

theorem Cslib.Radix.measurementValues_bounds (c D j : ℕ) (z : ℤ) : z ∈ measurementValues c D j → -↑D ≤ z ∧ z ≤ ↑D

Every coordinate is in the required signed interval, even at out-of-range indices.

theorem Cslib.Radix.measurementValues_injective (c D : ℕ) : Function.Injective fun (j : Fin ((2 * D + 1) ^ c)) => measurementValues c D ↑j

No two fitting indices encode the same signed measurement tuple, including radix one.

theorem Cslib.Radix.measurementValues_coverage (c D : ℕ) (word : List ℤ) (hlen : word.length = c) (hword : ∀ z ∈ word, -↑D ≤ z ∧ z ≤ ↑D) : ∃! j : Fin ((2 * D + 1) ^ c), measurementValues c D ↑j = word

Every list of the declared length with coordinates in the signed interval has exactly one fitting index. This proves actual decoder coverage without materializing the box.