Source addition and zero preservation for the actual encoded condenser

Padded coefficientwise XOR represents addition of source polynomials for arbitrary lists. For every semantic field seed, the decoded runtime program therefore preserves source addition and sends every all-false input to zero. The program is the existing condenserBits implementation behind decodedCondenser, connected to the polynomial map by the checked correctness theorem; no alternative implementation is introduced.

Only the two runtime dimension words must match their chosen powers of three. No source-length, capacity, positive-count, or positive-stride premise is needed. The characteristic-two structure is derived locally from the explicit binary field, and no global instances are introduced. Polynomial-map linearity and its source credits are documented in Condenser.Polynomial.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_addBits (s d : ℕ) (a b : List Bool) : sourcePolynomial s d (Complexity.BitPolynomial.addBits a b) = sourcePolynomial s d a + sourcePolynomial s d b

Padded XOR preserves source-polynomial addition, including unequal input lengths.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_replicate_false (s d n : ℕ) : sourcePolynomial s d (List.replicate n false) = 0

Every all-false source represents the zero polynomial, at every padding length.

theorem Algebraic.Cutwidth.Extractor.sourcePolynomial_nil (s d : ℕ) : sourcePolynomial s d [] = 0

An empty source represents the zero polynomial.

theorem Algebraic.Cutwidth.Extractor.decodedCondenser_addBits (s v : ℕ) (halfDegree extensionCount stride count a b : List Bool) (seed : AdjoinRoot (binaryModulus s)) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : decodedCondenser s halfDegree extensionCount stride count (Complexity.BitPolynomial.addBits a b) seed = decodedCondenser s halfDegree extensionCount stride count a seed + decodedCondenser s halfDegree extensionCount stride count b seed

For each field seed, the actual decoded program preserves padded source XOR.

theorem Algebraic.Cutwidth.Extractor.decodedCondenser_replicate_false (s v n : ℕ) (halfDegree extensionCount stride count : List Bool) (seed : AdjoinRoot (binaryModulus s)) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : decodedCondenser s halfDegree extensionCount stride count (List.replicate n false) seed = 0

Every padded zero source gives the zero vector of decoded output coordinates.

theorem Algebraic.Cutwidth.Extractor.decodedCondenser_nil (s v : ℕ) (halfDegree extensionCount stride count : List Bool) (seed : AdjoinRoot (binaryModulus s)) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) : decodedCondenser s halfDegree extensionCount stride count [] seed = 0

The empty source gives the zero decoded output for every field seed.