The scheduled condenser on blocks with one shared seed #
Apply the actual decoded scheduled map to every input block, using the
same seed for all blocks. The joint output is within t * 2^(-e) of a
normalized threshold-2^k block source conditional on each seed. The
source may have arbitrary dependence consistent with its block-source caps.
This is a finite statistical specialization of shared-seed condensation. It does not construct an encoded runtime loop over a varying block count.
theorem
Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_block
(n k e u : ℕ)
{α : Type u_1}
[Fintype α]
[Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))]
(rate : 0 < u)
(input : α ↪ List Bool)
(sourceLength : ∀ (x : α), (input x).length = n)
{t : ℕ}
{p : (Fin t → α) → ℝ}
(source : IsBlockSource p (2 ^ k))
:
let F := AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)));
let m := condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e));
∃ (q : F → (Fin t → Fin m → F) → ℝ),
(∀ (y : F), IsBlockSource (q y) (2 ^ k)) ∧ weightDist
(weightedSeededOutput p
fun (x : Fin t → α) (y : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))
(i : Fin t) =>
decodedExplicitCondenser n k e u (input (x i)) y)
(seedFamilyWeight q) ≤ ↑t * (2 ^ e)⁻¹
The scheduled map condenses any block source represented by fixed-length words, with the same seed in every block and additive total variation error.
theorem
Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_block_ofFn
(n k e u : ℕ)
[Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))]
(rate : 0 < u)
{t : ℕ}
{p : (Fin t → Fin n → Bool) → ℝ}
(source : IsBlockSource p (2 ^ k))
:
let F := AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)));
let m := condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e));
∃ (q : F → (Fin t → Fin m → F) → ℝ),
(∀ (y : F), IsBlockSource (q y) (2 ^ k)) ∧ weightDist
(weightedSeededOutput p
fun (x : Fin t → Fin n → Bool)
(y : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) (i : Fin t) =>
decodedExplicitCondenser n k e u (List.ofFn (x i)) y)
(seedFamilyWeight q) ≤ ↑t * (2 ^ e)⁻¹
In particular, arbitrary dependent blocks of n Boolean coordinates
use the scheduled condenser with one retained shared seed.