Exact look-ahead transcript identities #
Reindexing the original factored law identifies the successive alternating calls. The second transition observes the honest and tampered first outputs without replacing either input by an independent copy.
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAhead_first_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Mid]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
:
(alternatingSeedWeight w l r (fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
fun (zv : Z × Seed × Seed) (a : A) => W (x zv.1 a) zv.2.1) = mapWeight (fun (p : (Z × B) × Mid) => ((p.1.1, initialSeed (q p.1.1 p.1.2), initialSeed (q' p.1.1 p.1.2)), p.2))
(retainedExtractionWeight w l r x (fun (z : Z) (b : B) => initialSeed (q z b)) W)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSeedWeight_eq_alternating
{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}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
:
lookAheadSeedWeight w l r x q q' initialSeed W QExt = alternatingExtractionWeight w l r (fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
(fun (zv : Z × Seed × Seed) (a : A) => W (x zv.1 a) zv.2.1) q QExt
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAhead_second_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
(alternatingSeedWeight (observedTranscriptWeight w r fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
(observedTranscriptKernel r fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
(fun (zv : Z × Seed × Seed) => l zv.1)
(fun (zv : Z × Seed × Seed) (a : A) => (W (x zv.1 a) zv.2.1, W (x' zv.1 a) zv.2.2))
fun (zvr : (Z × Seed × Seed) × Mid × Mid) (b : B) => QExt (q zvr.1.1 b) zvr.2.1) = mapWeight
(fun (p : ((Z × Seed × Seed) × A) × Seed) =>
((p.1.1, W (x p.1.1.1 p.1.2) p.1.1.2.1, W (x' p.1.1.1 p.1.2) p.1.1.2.2), p.2))
(lookAheadSeedWeight w l r x q q' initialSeed W QExt)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadExtractionWeight_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
[Fintype Mid]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt = mapWeight (fun (p : (((Z × Seed × Seed) × Mid × Mid) × B) × Mid) => (((p.1.1.1.1, p.1.2), p.1.1.2), p.2))
(alternatingExtractionWeight
(observedTranscriptWeight w r fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
(observedTranscriptKernel r fun (z : Z) (b : B) => (initialSeed (q z b), initialSeed (q' z b)))
(fun (zv : Z × Seed × Seed) => l zv.1)
(fun (zv : Z × Seed × Seed) (a : A) => (W (x zv.1 a) zv.2.1, W (x' zv.1 a) zv.2.2))
(fun (zvr : (Z × Seed × Seed) × Mid × Mid) (b : B) => QExt (q zvr.1.1 b) zvr.2.1)
(fun (zv : Z × Seed × Seed) => x zv.1) W)