Seeded extraction retaining a correlated right variable

The left and right variables are independent given a transcript. The seed may be correlated arbitrarily with the remaining right state. The actual extraction law retains that entire state, including any mask added to the left source. The combining operation is explicit to support both addition and pointwise Boolean XOR without changing the program's representation.

noncomputable def Algebraic.Cutwidth.Extractor.retainedSeedWeight {Z : Type u_1} {B : Type u_2} {Seed : Type u_3} [Fintype Z] [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (y : Z → B → Seed) : Z × Seed → ℝ

The transcript and seed sampled from the complete right-side state.

Equations

• Algebraic.Cutwidth.Extractor.retainedSeedWeight w r y = Algebraic.Cutwidth.Extractor.mapWeight (fun (zb : Z × B) => (zb.1, y zb.1 zb.2)) fun (zb : Z × B) => w zb.1 * r zb.1 zb.2

noncomputable def Algebraic.Cutwidth.Extractor.retainedExtractionWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (E : X → Seed → Out) : (Z × B) × Out → ℝ

Extract from the left source while retaining the transcript and every right-side value.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.affineExtractionWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (mask : Z → B → X) (y : Z → B → Seed) (combine : X → X → X) (E : X → Seed → Out) : (Z × B) × Out → ℝ

Extract from the combined left source and right mask, retaining the full right state.

Equations

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