Lossless condensation with explicitly selected runtime parameters

The schedule chooses the field, extension degree, powering stride, and coordinate count from source length n, entropy budget k, inverse-error exponent e, and positive rate parameter u. The resulting runtime map has retained-seed test error at most 2^(-e) on every qualifying flat source. All algebraic and numerical capacity conditions follow from this schedule.

At support sizes at most 2^k, each ideal seed fiber is uniform on as many outputs as there are source points. Larger supports admit an explicit mixture of conditional 2^k-flat witnesses with the same error. These finite statistical consequences combine the checked GUV expansion proof with the explicit sparse parameter choice and runtime correctness. Asymptotic bounds and the higher extractor composition are separate results.

theorem Algebraic.Cutwidth.Extractor.explicitCondenser_loss (n k e : ℕ) {u : ℕ} (rate : 0 < u) : ↑((explicitCondenserExtensionDegree n k e u - 1) * (2 ^ sparsePowerBits u (explicitCondenserBudget n k e) - 1) * condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e))) / 2 ^ sparseFieldBits u (explicitCondenserBudget n k e) ≤ (2 ^ e)⁻¹

The selected extension and slack budget pay for inverse-power-of-two error.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_flat_lossless (n k e u : ℕ) [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) (P : Finset (List Bool)) (nonempty : P.Nonempty) (source : ∀ bits ∈ P, bits.length = n) (size : P.card ≤ 2 ^ k) : let T := explicitCondenserBudget n k e; let s := sparseFieldExponent u T; let m := condenserCoordinates k (sparsePowerBits u T); ∃ (g : AdjoinRoot (binaryModulus s) → ↥P ↪ Fin m → AdjoinRoot (binaryModulus s)), ∀ (test : Finset (AdjoinRoot (binaryModulus s) × (Fin m → AdjoinRoot (binaryModulus s)))), |seededTestProb (fun (bits : ↥P) => decodedExplicitCondenser n k e u ↑bits) test - seededTestProb (fun (bits : ↥P) (y : AdjoinRoot (binaryModulus s)) => (g y) bits) test| ≤ (2 ^ e)⁻¹

Every nonempty flat n-bit source of size at most 2^k has a seedwise flat witness within the requested error. All parameters are selected before P.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_flat_mixture (n k e u : ℕ) [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) (P : Finset (List Bool)) (source : ∀ bits ∈ P, bits.length = n) (threshold : 2 ^ k ≤ P.card) : let T := explicitCondenserBudget n k e; let s := sparseFieldExponent u T; let m := condenserCoordinates k (sparsePowerBits u T); ∃ (g : (S : ↥(Finset.powersetCard (2 ^ k) P)) → AdjoinRoot (binaryModulus s) → ↥↑S ↪ Fin m → AdjoinRoot (binaryModulus s)), ∀ (test : Finset (AdjoinRoot (binaryModulus s) × (Fin m → AdjoinRoot (binaryModulus s)))), |seededTestProb (fun (bits : ↥P) => decodedExplicitCondenser n k e u ↑bits) test - seededMixtureTestProb (fun (x : ↥(Finset.powersetCard (2 ^ k) P)) => (↑(Finset.powersetCard (2 ^ k) P).card)⁻¹) (fun (S : ↥(Finset.powersetCard (2 ^ k) P)) (bits : ↥↑S) (y : AdjoinRoot (binaryModulus s)) => (g S y) bits) test| ≤ (2 ^ e)⁻¹

Every flat n-bit support of size at least 2^k is close to an explicit mixture of conditional 2^k-flat outputs, retaining the uniform seed.