Exact transcript identities for look-ahead refreshes

Right observations and subsequent left observations preserve the complete latent joint law. The refresh output laws only project these deterministic transcripts; no independent resampling is used in their identities.

theorem Algebraic.Cutwidth.Extractor.Internal.factoredWeight_observe_right_left {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {V : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (g : Z → B → U) (f : Z × U → A → V) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((((p.1.1, g p.1.1 p.1.2), f (p.1.1, g p.1.1 p.1.2) p.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight (observedTranscriptWeight w r g) (fun (zu : Z × U) => l zu.1) f) (observedTranscriptKernel (fun (zu : Z × U) => l zu.1) f) fun (zuv : (Z × U) × V) => observedTranscriptKernel r g zuv.1

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBase_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] (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) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => have zq := (p.1.1, q p.1.1 p.1.2, q' p.1.1 p.1.2); (((zq, lookAheadBaseMessage x x' initialSeed W QExt zq p.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) (lookAheadBaseLeft l x x' initialSeed W QExt) (lookAheadBaseRight r q q')

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBase_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} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] [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) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (lookAheadBaseWeight w l r x x' q q' initialSeed W QExt) ∧ (∀ (t : LookAheadBaseTranscript Z Q Mid), IsProbabilityWeight (lookAheadBaseLeft l x x' initialSeed W QExt t)) ∧ ∀ (t : LookAheadBaseTranscript Z Q Mid), IsProbabilityWeight (lookAheadBaseRight r q q' t)

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadFirstRefreshWeight_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 Q] [Fintype Mid] [Fintype Out] (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) (y : Z → B → Y) (R : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadTamperedRefreshWeight_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 Q] [Fintype Mid] [Fintype Out] (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) (y y' : Z → B → Y) (R : Y → Mid → Out) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)

theorem Algebraic.Cutwidth.Extractor.Internal.firstRefresh_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) => (q z b, q' z b)) fun (zq : Z × Q × Q) (a : A) => W (x zq.1 a) (initialSeed zq.2.1)) = mapWeight (fun (p : (Z × B) × Mid) => ((p.1.1, q p.1.1 p.1.2, 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.firstRefresh_output_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 Q] [Fintype Out] (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) (y : Z → B → Y) (R : Y → Mid → Out) : lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R = mapWeight (fun (p : ((Z × Q × Q) × A) × Out) => (((p.1.1, lookAheadBaseMessage x x' initialSeed W QExt p.1.1 p.1.2), p.1.2), p.2)) (alternatingExtractionWeight w l r (fun (z : Z) (b : B) => (q z b, q' z b)) (fun (zq : Z × Q × Q) (a : A) => W (x zq.1 a) (initialSeed zq.2.1)) y R)