Actual affine calls supply the linear-sampler parity estimate #
The complete selected affine construction supplies both the small bad set and the parity estimate outside that set. The source has only its original point-mass bound; no extractor, security, or parity-bias witness is assumed. The caller supplies a linear map for the sampler values at the selected call positions. Choosing and amplifying the global sampler is a separate step of Chattopadhyay--Liao, Lemma 5.4.
theorem
Algebraic.Cutwidth.Extractor.affineLeakage_linear_parameters
(n t a target : ℕ)
(p : (Fin n → Bool) → ℝ)
(sampler :
(Fin n → Bool) → Option (Fin t) → Fin (affinePhaseOneRightBits n t a (affineIterationTarget t target)) → Bool)
(advice : Option (Fin t) → List Bool)
(j :
Fin
(matchedBlockOutputBits (growingMatchedBlockDepth t) (affinePhaseOneScale n t a (affineIterationTarget t target))))
{γ : ℝ}
(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))
(linear : ∀ (x y : Fin n → Bool) (i : Option (Fin t)), sampler (xorInput x y) i = xorInput (sampler x i) (sampler y i))
:
let σ := affineIterationTarget t target;
let d := affinePhaseOneRightBits n t a σ;
let h := growingMatchedBlockDepth t;
have L₀ := affinePhaseOneInitialScale n t a σ;
let L := affinePhaseOneScale n t a σ;
have e := affinePhaseOneLocalError σ;
have cb := affineCorrelationBreaker n d h L₀ e L (adviceErrorExponent a e) e (affineIterationRounds t);
have bad := affineLeakageBadSeeds cb p sampler advice γ;
↑bad.card ≤ (2 ^ target)⁻¹ / γ * ↑(Fintype.card (Fin d → Bool)) ∧ ∀ (b : Fin n → Bool),
sampler b none ∉ bad →
|∑ x : Fin n → Bool,
p x * ∏ i : Option (Fin t),
if cb (xorInput x b) (sampler (xorInput x b) i) (advice i) j = true then 1 else -1| ≤ 2 * γ
The actual construction gives a small seed test and all corresponding linear-sampler parities.