Exact serialization of statistical condenser outputs

The coordinate vector and its concatenated fixed-width bit representation are equivalent, including the empty vector. Serialization is injective independently of any source distribution, and decoding preserves each coordinate's position and every padding bit at the canonical total width. Coordinate addition corresponds exactly to padded bitwise XOR.

Re-encoding the decoded runtime output returns its exact original bits. This links statistical statements about field-coordinate vectors to the existing bit output, using only the correct base-field width. The codec operations are semantic maps; the runtime algorithm and its cost are already supplied by Encoding.

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

Serialization writes one canonical-width block for every coordinate.

theorem Algebraic.Cutwidth.Extractor.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)

Each consecutive output block is exactly the corresponding field encoding.

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

Decoding after serialization recovers every coordinate vector.

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

A bitstring of the exact total width is recovered, including all zero padding.

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

Distinct coordinate vectors always have distinct serialized words.

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

Decoding preserves padded XOR, including words of unequal lengths.

theorem Algebraic.Cutwidth.Extractor.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)

Serialization sends coordinate addition to XOR of the two fixed-width words.

noncomputable def Algebraic.Cutwidth.Extractor.condenserOutputEquiv (s m : ℕ) : (Fin m → AdjoinRoot (binaryModulus s)) ≃ { bits : List Bool // bits.length = m * (2 * 3 ^ s) }

Coordinate vectors correspond exactly to bitstrings of the prescribed total width.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Extractor.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

The serialized statistical output is the actual runtime bit output. Only the base-field width is required; extension and iteration words remain arbitrary.