Flat lossless guarantees for the decoded runtime condenser

Within the coefficient capacity, equal-length bitstrings give distinct source polynomials. The runtime correctness theorem therefore transfers polynomial neighbor expansion without collapsing any source points. The seedwise injection theorem turns this expansion into a bound on every retained-seed test, and exact subset averaging extends it to larger flat supports.

theorem Algebraic.Cutwidth.Extractor.Internal.decodedCondenser_flat_lossless (s v n : ℕ) [Fintype (AdjoinRoot (binaryModulus s))] (halfDegree extensionCount stride count : List Bool) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) (degree : 0 < v) (fieldSize : stride.length ≤ 2 * 3 ^ s) (capacity : n ≤ 2 * 3 ^ s * 3 ^ v) (P : Finset (List Bool)) (nonempty : P.Nonempty) (source : ∀ bits ∈ P, bits.length = n) (size : P.card ≤ (2 ^ stride.length) ^ count.length) : ∃ (g : AdjoinRoot (binaryModulus s) → ↥P ↪ Fin count.length → AdjoinRoot (binaryModulus s)), ∀ (T : Finset (AdjoinRoot (binaryModulus s) × (Fin count.length → AdjoinRoot (binaryModulus s)))), |seededTestProb (fun (bits : ↥P) => decodedCondenser s halfDegree extensionCount stride count ↑bits) T - seededTestProb (fun (bits : ↥P) (y : AdjoinRoot (binaryModulus s)) => (g y) bits) T| ≤ ↑((3 ^ v - 1) * (2 ^ stride.length - 1) * count.length) / 2 ^ (2 * 3 ^ s)

theorem Algebraic.Cutwidth.Extractor.Internal.decodedCondenser_flat_mixture (s v n : ℕ) [Fintype (AdjoinRoot (binaryModulus s))] (halfDegree extensionCount stride count : List Bool) (half : halfDegree.length = 3 ^ s) (extension : extensionCount.length = 3 ^ v) (degree : 0 < v) (fieldSize : stride.length ≤ 2 * 3 ^ s) (capacity : n ≤ 2 * 3 ^ s * 3 ^ v) (P : Finset (List Bool)) (source : ∀ bits ∈ P, bits.length = n) {K : ℕ} (positive : 0 < K) (threshold : K ≤ P.card) (size : K ≤ (2 ^ stride.length) ^ count.length) : ∃ (g : (S : ↥(Finset.powersetCard K P)) → AdjoinRoot (binaryModulus s) → ↥↑S ↪ Fin count.length → AdjoinRoot (binaryModulus s)), ∀ (T : Finset (AdjoinRoot (binaryModulus s) × (Fin count.length → AdjoinRoot (binaryModulus s)))), |seededTestProb (fun (bits : ↥P) => decodedCondenser s halfDegree extensionCount stride count ↑bits) T - seededMixtureTestProb (fun (x : ↥(Finset.powersetCard K P)) => (↑(Finset.powersetCard K P).card)⁻¹) (fun (S : ↥(Finset.powersetCard K P)) (bits : ↥↑S) (y : AdjoinRoot (binaryModulus s)) => (g S y) bits) T| ≤ ↑((3 ^ v - 1) * (2 ^ stride.length - 1) * count.length) / 2 ^ (2 * 3 ^ s)