Conditioning on all deterministic seed leakage

The observation graph keeps every original source occurrence. Its conditional rows have the existing normalized completion at null events, and multiplying by the observation marginal recovers the exact original mass. These identities implement the conditioning step in Chattopadhyay--Liao, Lemma 5.3, printed pp.19--20: https://arxiv.org/abs/2110.12652.

theorem Algebraic.Cutwidth.Extractor.Internal.leakageConditioning_factor {X : Type u_1} {Z : Type u_2} [Fintype X] (p : X → ℝ) (leak : X → Z) (nonnegative : ∀ (x : X), 0 ≤ p x) (z : Z) (x : X) : mapWeight leak p z * conditionalWeight (mapWeight (fun (x : X) => (leak x, x)) p) z x = if leak x = z then p x else 0

theorem Algebraic.Cutwidth.Extractor.Internal.leakageConditioning_factored {X : Type u_1} {Z : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] (p : X → ℝ) (leak : X → Z) (right : Y → ℝ) (nonnegative : ∀ (x : X), 0 ≤ p x) : (mapWeight (fun (yx : Y × X) => ((leak yx.2, yx.1), yx.2)) fun (yx : Y × X) => right yx.1 * p yx.2) = factoredWeight (mapWeight leak p) (conditionalWeight (mapWeight (fun (x : X) => (leak x, x)) p)) fun (x : Z) => right

theorem Algebraic.Cutwidth.Extractor.Internal.leakage_map_tagged {Y : Type u_1} {X : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype Y] [Fintype X] (w : Y → ℝ) (p : X → ℝ) (f : Y → X → A × B) : (mapWeight (fun (yx : Y × X) => ((yx.1, (f yx.1 yx.2).1), (f yx.1 yx.2).2)) fun (yx : Y × X) => w yx.1 * p yx.2) = fun (yab : (Y × A) × B) => w yab.1.1 * mapWeight (f yab.1.1) p (yab.1.2, yab.2)

theorem Algebraic.Cutwidth.Extractor.Internal.leakage_xor_uniform {d : ℕ} (z : Fin d → Bool) : mapWeight (fun (y : Fin d → Bool) => xorInput y z) (uniformWeight (Fin d → Bool)) = uniformWeight (Fin d → Bool)

theorem Algebraic.Cutwidth.Extractor.Internal.leakage_envelope_sum (t d k : ℕ) : ∑ x : Option (Fin t) → Fin d → Bool, (2 ^ (k + (t + 1) * d))⁻¹ = (2 ^ k)⁻¹