The actual finite sumset-extractor construction

The amplified matched sampler produces the seed of one fixed affine correlation breaker. Its advice encodes the outer and candidate indices. XOR over candidates gives each outer bit, and strict majority gives the final bit. None of these choices depends on the source sets or on a tested parity. All maps are total, including outside the finite sampling guards.

This is the construction strategy of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.4 and the proof of Theorem 2: https://arxiv.org/abs/2110.12652. Its parameters use the library's conservative matched and Gamma extractors. Eventual entropy bounds and uniform evaluation of the complete family are proved in Construction.Asymptotics and Construction.Uniform.

def Algebraic.Cutwidth.Extractor.sourceReductionSeedBits (n L : ℕ) : ℕ

The seed width of the single affine breaker used by the entire reduction.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionEntropy (n L : ℕ) : ℕ

Source entropy sufficient for both affine leakage and the amplified sampler.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionSampler (n L : ℕ) (x : Fin n → Bool) (i : Fin (sourceReductionOuterCount (matchedBlockSeedBits L))) (z : Fin (sourceReductionCandidateCount (matchedBlockSeedBits L))) : Fin (sourceReductionSeedBits n L) → Bool

The actual sampler with explicit binary enumeration of both seed indices.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionOutput (n L : ℕ) (x : Fin n → Bool) : Fin (sourceReductionOuterCount (matchedBlockSeedBits L)) → Bool

XOR the actual candidate calls, using injective fixed-length binary advice.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionExtractor (n L : ℕ) (x : Fin n → Bool) : Bool

The final finite construction: majority of the actual XOR-reduction outputs.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionExtractor n L x = Complexity.majority (Algebraic.Cutwidth.Extractor.sourceReductionOutput n L x)