Exact seed averaging and laws for the second-output refresh #
A normalized message from the independent left kernel only splits each old transcript row. It preserves the original retained-seed discrepancy exactly after averaging, including null messages. The deterministic laws below then identify the actual second seed and final retained transcript.
theorem
Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_observe_left_dist
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{U : Type u_4}
{Seed : Type u_5}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype U]
[Fintype Seed]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(f : Z → A → U)
(s : Z → B → Seed)
(hw : ∀ (z : Z), 0 ≤ w z)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
weightDist (retainedSeedWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) fun (zu : Z × U) => s zu.1)
(uniformSecondWeight
(retainedSeedWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) fun (zu : Z × U) => s zu.1)) = weightDist (retainedSeedWeight w r s) (uniformSecondWeight (retainedSeedWeight w r s))
theorem
Algebraic.Cutwidth.Extractor.Internal.fixedTamperingSecondRefreshWeight_probability
{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 Mid]
[Fintype Q]
[Fintype Out]
(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)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(R : Y → Mid → Out)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R)
theorem
Algebraic.Cutwidth.Extractor.Internal.fixedTamperingSecond_seed_eq_map
{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 Mid]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q : Z → B → Q)
(y' : Z → B → Y)
(leak : Z → A → Mid)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(R : Y → Mid → Out)
:
(alternatingSeedWeight (observedTranscriptWeight w l leak) (observedTranscriptKernel l leak)
(fun (zm : Z × Mid) => r zm.1) (fixedTamperingRightMessage q y' R) fun (t : (Z × Mid) × Q × Out) (a : A) =>
(fixedTamperingSecondHonestMessage x initialSeed W QExt t a).2) = mapWeight
(fun (p : (((Z × Mid) × B) × Mid × Mid) × Mid) =>
((p.1.1.1, fixedTamperingRightMessage q y' R p.1.1.1 p.1.1.2), p.2))
(lookAheadExtractionWeight (observedTranscriptWeight w l leak) (observedTranscriptKernel l leak)
(fun (zm : Z × Mid) => r zm.1) (fun (zm : Z × Mid) => x zm.1) (fun (zm : Z × Mid) => x zm.1)
(fun (zm : Z × Mid) => q zm.1) (fun (zm : Z × Mid) => q zm.1) initialSeed W QExt)
theorem
Algebraic.Cutwidth.Extractor.Internal.fixedTamperingSecondRefreshWeight_eq_alternating_map
{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 Mid]
[Fintype Q]
[Fintype Out]
(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)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(R : Y → Mid → Out)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
fixedTamperingSecondRefreshWeight w l r x q y y' leak initialSeed W QExt R = mapWeight
(fun (p : (((Z × Mid) × Q × Out) × A) × Out) =>
(((p.1.1, fixedTamperingSecondHonestMessage x initialSeed W QExt p.1.1 p.1.2), p.1.2), p.2))
(alternatingExtractionWeight (observedTranscriptWeight w l leak) (observedTranscriptKernel l leak)
(fun (zm : Z × Mid) => r zm.1) (fixedTamperingRightMessage q y' R)
(fun (t : (Z × Mid) × Q × Out) (a : A) => (fixedTamperingSecondHonestMessage x initialSeed W QExt t a).2)
(fun (zm : Z × Mid) => y zm.1) R)