Exact fixed-tampering transcript identities

Three deterministic observations identify the actual law with normalized left and right kernels. The statistical proof can process the left leak before the independent right input observation and then retain the honest first output as a deterministic function of the already retained state.

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTampering_factored_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] [Fintype Q] [Fintype Out] (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) (R : Y → Mid → Out) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : factoredWeight (fixedTamperingTranscriptWeight w l r x q y' leak initialSeed W R) (fixedTamperingLeft l x leak initialSeed W) (fixedTamperingRight r q y' R) = mapWeight (fun (p : (Z × B) × A) => ((fixedTamperingTranscriptValue x q y' leak initialSeed W R p.1.1 p.2 p.1.2, p.1.2), p.2)) (factoredWeight w l r)

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTampering_factors_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' : Z → B → Y) (leak : Z → A → Mid) (initialSeed : Q → Seed) (W : X → Seed → Mid) (R : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (fixedTamperingTranscriptWeight w l r x q y' leak initialSeed W R) ∧ (∀ (t : FixedTamperingTranscript Z Q Mid Out), IsProbabilityWeight (fixedTamperingLeft l x leak initialSeed W t)) ∧ ∀ (t : FixedTamperingTranscript Z Q Mid Out), IsProbabilityWeight (fixedTamperingRight r q y' R t)

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTamperingRefreshWeight_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) (R : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R)

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTamperingRefreshWeight_eq_factored {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) (R : Y → Mid → Out) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R = mapWeight (fun (p : (FixedTamperingTranscript Z Q Mid Out × B) × A) => ((p.1.1, p.2), R (y p.1.1.1.1.1 p.1.2) p.1.1.2)) (factoredWeight (fixedTamperingTranscriptWeight w l r x q y' leak initialSeed W R) (fixedTamperingLeft l x leak initialSeed W) (fixedTamperingRight r q y' R))

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTampering_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) (R : Y → Mid → Out) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : alternatingSeedWeight (observedTranscriptWeight w l leak) (observedTranscriptKernel l leak) (fun (zm : Z × Mid) => r zm.1) (fixedTamperingRightMessage q y' R) (fixedTamperingHonestMessage x initialSeed W) = mapWeight (fun (p : ((Z × B) × Unit × Mid) × Mid) => (((p.1.1.1, p.1.2.2), fixedTamperingRightMessage q y' R (p.1.1.1, p.1.2.2) p.1.1.2), p.2)) (twoSidedExtractionWeight w l r x (fun (z : Z) (b : B) => initialSeed (q z b)) (fun (x : Z) (x_1 : A) => ()) (fun (x : Z) (x_1 : B) => ()) (fun (z : Z) (x : Unit) (a : A) => leak z a) W)

theorem Algebraic.Cutwidth.Extractor.Internal.fixedTamperingRefreshWeight_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) (R : Y → Mid → Out) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R = mapWeight (fun (p : (((Z × Mid) × Q × Out) × A) × Out) => (((p.1.1, fixedTamperingHonestMessage x initialSeed W 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) (fixedTamperingHonestMessage x initialSeed W) (fun (zm : Z × Mid) => y zm.1) R)