XOR additivity of the specified recursive extractor

For every fixed complete seed tuple, input XOR becomes pointwise addition of the actual output coordinates in ZMod 2. This holds for all numerical parameters, independently of the statistical entropy and error budgets.

The proof composes the checked source-addition identities of the concrete condenser, serializer, and one-shot extractor through the recursive program. It makes explicit the linearity invariant used in the recursive construction of Chattopadhyay--Goodman--Liao, credited in Recursion.Linearity. No field enumeration or uniform runtime assumption enters this identity.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockExtractor_xor (n h Q E ell : ℕ) (x x' : Fin n → Bool) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) : scheduledBlockExtractor n h Q E ell (fun (i : Fin n) => x i ^^ x' i) seeds = scheduledBlockExtractor n h Q E ell x seeds + scheduledBlockExtractor n h Q E ell x' seeds

At fixed retained seeds, the actual scheduled extractor sends input XOR to output addition.