Actual extraction laws for a smooth left source

The transcript retains an original left observation and then an actual finite prefix message. The right seed and its observation may depend on both messages. Every law is a deterministic image of the original factored sample. In particular, the prefix and the extra leak are read from the original left variable, even when a proof repairs its honest source coordinate.

These laws support the smooth-source step of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1: https://arxiv.org/abs/2110.12652. Definitions alone impose no source uniformity or extraction guarantee.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.SmoothMergingTranscript (Z : Type u_1) (U : Type u_2) (Q : Type u_3) : Type (max (max u_2 u_1) u_3)

The original tag, selected left observation, and actual prefix message.

Equations

• Algebraic.Cutwidth.Extractor.SmoothMergingTranscript Z U Q = ((Z × U) × Q)

def Algebraic.Cutwidth.Extractor.smoothMergingTranscript {Z : Type u_1} {A : Type u_2} {U : Type u_3} {Q : Type u_4} (u : Z → A → U) (q : Z → A → Q) (z : Z) (a : A) : SmoothMergingTranscript Z U Q

Both original left observations extend the original tag in their execution order.

Equations

• Algebraic.Cutwidth.Extractor.smoothMergingTranscript u q z a = ((z, u z a), q z a)

noncomputable def Algebraic.Cutwidth.Extractor.smoothMergingSeedWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {Q : Type u_5} {V : Type u_6} {Seed : Type u_7} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (u : Z → A → U) (q : Z → A → Q) (v : SmoothMergingTranscript Z U Q → B → V) (y : SmoothMergingTranscript Z U Q → B → Seed) : (SmoothMergingTranscript Z U Q × V) × Seed → ℝ

The actual right-derived seed retains both original left messages and its right observation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Extractor.smoothTwoSidedExtractionWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {U : Type u_5} {Q : Type u_6} {V : Type u_7} {W : Type u_8} {Seed : Type u_9} {Out : Type u_10} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (u : Z → A → U) (q : Z → A → Q) (v : SmoothMergingTranscript Z U Q → B → V) (y : SmoothMergingTranscript Z U Q → B → Seed) (leak : SmoothMergingTranscript Z U Q → V → A → W) (E : X → Seed → Out) : ((SmoothMergingTranscript Z U Q × B) × W) × Out → ℝ

Actual extraction retaining both left messages, the entire right variable, and its left leak.

Equations

• One or more equations did not get rendered due to their size.