Linear sampler outputs turn leakage bounds into parity bounds #
After fixing the second summand, linearity expresses each actual sampler seed as the XOR of a fixed seed and a source observation. The honest output controls the full product of signs of the selected calls.
theorem
Algebraic.Cutwidth.Extractor.Internal.affineLeakage_linear_parity_le
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(sampler : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(linear : ∀ (x y : Fin n → Bool) (i : Option (Fin t)), sampler (xorInput x y) i = xorInput (sampler x i) (sampler y i))
(bit : Out → Bool)
(balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool)
(γ : ℝ)
(b : Fin n → Bool)
(good : sampler b none ∉ affineLeakageBadSeeds cb p sampler advice γ)
: