Few bad seeds for the actual affine correlation breaker #
For the complete selected construction, most honest seeds remain good
after deterministic source-dependent seed leakage, simultaneously for
every shift and every tuple of tampered seeds. The original source pays
for all t + 1 leakage words. No caller-supplied security or conditional
entropy statement is required.
This proves the finite form of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.3, with the library's actual conservative affine parameters: https://arxiv.org/abs/2110.12652.
theorem
Algebraic.Cutwidth.Extractor.affineLeakageBadSeeds_parameters_card_le
(n t a target : ℕ)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool)
(advice : Option (Fin t) → List Bool)
{γ : ℝ}
(positive : 0 < t)
(error : 0 < γ)
(probability : IsProbabilityWeight p)
(cap : ∀ (x : Fin n → Bool), p x ≤ (2 ^ affineLeakageSourceEntropy n t a target)⁻¹)
(honest_length : (advice none).length = a)
(tampered_length : ∀ (i : Fin t), (advice (some i)).length = a)
(different : ∀ (i : Fin t), advice none ≠ advice (some i))
:
let σ := affineIterationTarget t target;
let d := affinePhaseOneRightBits n t a σ;
have h := growingMatchedBlockDepth t;
have L₀ := affinePhaseOneInitialScale n t a σ;
have L := affinePhaseOneScale n t a σ;
have e := affinePhaseOneLocalError σ;
have cb := affineCorrelationBreaker n d h L₀ e L (adviceErrorExponent a e) e (affineIterationRounds t);
↑(affineLeakageBadSeeds cb p leak advice γ).card ≤ (2 ^ target)⁻¹ / γ * ↑(Fintype.card (Fin d → Bool))
The actual selected affine construction has at most a 2^-target / γ fraction of bad seeds.