Second-output extraction after a left-only tampered seed #
First reveal the leak. Its alphabet multiplies the total original left envelope, while both right-source envelope totals and the average original prefix discrepancy are preserved. The actual two-round theorem supplies the second output with the full right state retained. Project to the right observation, alternate back to the original right source, and append both honest outputs using the retained left state and right input.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_fixedTampering_second_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Fintype Y]
[Fintype Out]
[Nonempty Seed]
[Nonempty Mid]
[Nonempty Out]
{W : X → Seed → Mid}
{QExt : Q → Mid → Seed}
{R : Y → Mid → Out}
{K L J : ℕ}
{ε η θ δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor QExt L η)
(second_error : 0 ≤ η)
(refresh : WeightedStrongSeededExtractor R J θ)
(refresh_error : 0 ≤ θ)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q : Z → B → Q)
(y y' : Z → B → Y)
(leak : Z → A → Mid)
(initialSeed : Q → Seed)
(μ ν ξ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(left_nonnegative : ∀ (z : Z), 0 ≤ μ z)
(right_nonnegative : ∀ (z : Z), 0 ≤ ν z)
(refresh_nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν z)
(refresh_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ξ z)
(seed :
weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))
(uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) ≤ δ)
:
weightDist (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R)
(uniformSecondWeight (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R)) ≤ θ + 2 * ε + η + δ + ↑K * ↑(Fintype.card Mid) * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z + ↑J * ↑(Fintype.card Q) * ↑(Fintype.card Out) * ∑ z : Z, ξ z