Fixed-seed additivity of recursive block extraction

Pair splitting preserves pointwise addition. The recursive block map and its final extractor therefore preserve addition whenever their supplied component maps do so at each fixed seed. Only the levels below the chosen recursion depth need an addition law.

This is the algebraic composition invariant for the linear maps used in Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. The statements require only addition operations; statistical guarantees, an encoded evaluator, and the short-seed parameter schedule are separate.

theorem Algebraic.Cutwidth.Extractor.splitBlockEquiv_add {α : Type u_1} [Add α] {t : ℕ} (x x' : Fin t → α × α) : (splitBlockEquiv α t) (x + x') = (splitBlockEquiv α t) x + (splitBlockEquiv α t) x'

Splitting pairs into successive coordinates preserves pointwise addition.

theorem Algebraic.Cutwidth.Extractor.condenseSplitMap_add {α : Type u_1} {β : Type u_2} {Fresh : Type u_3} [Add α] [Add β] (C : α → Fresh → β × β) (C_add : ∀ (a b : α) (y : Fresh), C (a + b) y = C a y + C b y) (t : ℕ) (x x' : Fin t → α) (y : Fresh) : condenseSplitMap C t (x + x') y = condenseSplitMap C t x y + condenseSplitMap C t x' y

One shared-seed condensation and splitting step preserves addition.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockMap_add {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} [Add X] [(i : ℕ) → Add (α i)] {t : ℕ} (initial : X → Earlier → Fin t → α 0) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (n : ℕ) (initial_add : ∀ (x x' : X) (y : Earlier), initial (x + x') y = initial x y + initial x' y) (C_add : ∀ i < n, ∀ (a b : α i) (y : Fresh i), C i (a + b) y = C i a y + C i b y) (x x' : X) (seeds : RecursiveSeeds Earlier Fresh n) : recursiveBlockMap initial C n (x + x') seeds = recursiveBlockMap initial C n x seeds + recursiveBlockMap initial C n x' seeds

Fixed-seed recursive block condensation is additive when its executed maps are additive.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockExtractor_add {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} {Last : Type z} {Ω : Type r} [Add X] [(i : ℕ) → Add (α i)] [Add Ω] (initial : X → Earlier → α 0) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (n : ℕ) (E : α n → Last → Ω) (initial_add : ∀ (x x' : X) (y : Earlier), initial (x + x') y = initial x y + initial x' y) (C_add : ∀ i < n, ∀ (a b : α i) (y : Fresh i), C i (a + b) y = C i a y + C i b y) (E_add : ∀ (a b : α n) (y : Last), E (a + b) y = E a y + E b y) (x x' : X) (seeds : RecursiveSeeds Earlier Fresh n × Last) : recursiveBlockExtractor initial C n E (x + x') seeds = recursiveBlockExtractor initial C n E x seeds + recursiveBlockExtractor initial C n E x' seeds

The complete finite recursive extractor preserves addition for every fixed retained seed.