XOR through the actual scheduled recursive maps

Exact serialization transfers coordinate addition to padded bitwise XOR. Reading the two output halves preserves this operation. A local Boolean addition then lets the generic recursive additivity theorem compose these actual initial, level, and leaf maps without adding a global Boolean instance.

@[instance_reducible]

def Algebraic.Cutwidth.Extractor.Internal.scheduledBoolXorAdd : Add Bool

Local XOR addition for applying the generic recursive composition theorem.

Equations

• Algebraic.Cutwidth.Extractor.Internal.scheduledBoolXorAdd = { add := xor }

theorem Algebraic.Cutwidth.Extractor.Internal.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