Inverse laws for serialized condenser coordinates

Equal-width list blocks can be extracted and reassembled without losing leading or trailing zeros. Applying the field codec's inverse laws to each block gives exact serialization, including the empty-coordinate case. The fixed runtime output length then identifies serialization of decoded coordinates with the original output word.

theorem Algebraic.Cutwidth.Extractor.Internal.encodeCondenserOutput_length (s m : ℕ) (coords : Fin m → AdjoinRoot (binaryModulus s)) : (encodeCondenserOutput s m coords).length = m * (2 * 3 ^ s)

theorem Algebraic.Cutwidth.Extractor.Internal.coefficientBlock_encodeCondenserOutput (s m : ℕ) (coords : Fin m → AdjoinRoot (binaryModulus s)) (i : Fin m) : Complexity.BitPolynomial.coefficientBlock (encodeCondenserOutput s m coords) (2 * 3 ^ s) ↑i = BinaryFieldCodec.encode s (coords i)

theorem Algebraic.Cutwidth.Extractor.Internal.decode_encodeCondenserOutput (s m : ℕ) (coords : Fin m → AdjoinRoot (binaryModulus s)) : decodeCondenserOutput s m (encodeCondenserOutput s m coords) = coords

theorem Algebraic.Cutwidth.Extractor.Internal.encode_decodeCondenserOutput (s m : ℕ) (bits : List Bool) (length : bits.length = m * (2 * 3 ^ s)) : encodeCondenserOutput s m (decodeCondenserOutput s m bits) = bits

theorem Algebraic.Cutwidth.Extractor.Internal.encodeCondenserOutput_injective (s m : ℕ) : Function.Injective (encodeCondenserOutput s m)

theorem Algebraic.Cutwidth.Extractor.Internal.decodeCondenserOutput_addBits (s m : ℕ) (a b : List Bool) : decodeCondenserOutput s m (Complexity.BitPolynomial.addBits a b) = decodeCondenserOutput s m a + decodeCondenserOutput s m b

theorem Algebraic.Cutwidth.Extractor.Internal.encodeCondenserOutput_add (s m : ℕ) (a b : Fin m → AdjoinRoot (binaryModulus s)) : encodeCondenserOutput s m (a + b) = Complexity.BitPolynomial.addBits (encodeCondenserOutput s m a) (encodeCondenserOutput s m b)

theorem Algebraic.Cutwidth.Extractor.Internal.encodeCondenserOutput_decodedCondenser (s : ℕ) (halfDegree extensionCount stride count bits : List Bool) (seed : AdjoinRoot (binaryModulus s)) (half : halfDegree.length = 3 ^ s) : encodeCondenserOutput s count.length (decodedCondenser s halfDegree extensionCount stride count bits seed) = condenserBits bits halfDegree extensionCount (BinaryFieldCodec.encode s seed) stride count