Exact widths and inverse laws for scheduled seed words

The prefix induction appends one canonical field word at each level. Taking and dropping at its prior width recover both components. The final condenser and hash words use the same fixed-width decomposition, preserving all coefficient zeros without enumerating any quotient field.

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockSeedPrefixBits_zero (n h Q E : ℕ) : scheduledBlockSeedPrefixBits n h Q E 0 = sparseFieldBits 1 (explicitCondenserBudget n (recursiveBlockEntropy h Q 0) E)

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockSeedPrefixBits_succ (n h Q E i : ℕ) : scheduledBlockSeedPrefixBits n h Q E (i + 1) = scheduledBlockSeedPrefixBits n h Q E i + recursiveBlockSeedWidth (scheduledBlockInitialWidth n h Q E) h Q E i

theorem Algebraic.Cutwidth.Extractor.Internal.encodeScheduledBlockSeedPrefix_length (n h Q E i : ℕ) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i) : (encodeScheduledBlockSeedPrefix n h Q E i seeds).length = scheduledBlockSeedPrefixBits n h Q E i

theorem Algebraic.Cutwidth.Extractor.Internal.decode_encodeScheduledBlockSeedPrefix (n h Q E i : ℕ) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i) : decodeScheduledBlockSeedPrefix n h Q E i (encodeScheduledBlockSeedPrefix n h Q E i seeds) = seeds

theorem Algebraic.Cutwidth.Extractor.Internal.encode_decodeScheduledBlockSeedPrefix (n h Q E i : ℕ) (bits : List Bool) (length : bits.length = scheduledBlockSeedPrefixBits n h Q E i) : encodeScheduledBlockSeedPrefix n h Q E i (decodeScheduledBlockSeedPrefix n h Q E i bits) = bits

theorem Algebraic.Cutwidth.Extractor.Internal.encodeScheduledBlockSeeds_length (n h Q E ell : ℕ) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) : (encodeScheduledBlockSeeds n h Q E ell seeds).length = scheduledBlockSeedBits n h Q E ell

theorem Algebraic.Cutwidth.Extractor.Internal.decode_encodeScheduledBlockSeeds (n h Q E ell : ℕ) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) : decodeScheduledBlockSeeds n h Q E ell (encodeScheduledBlockSeeds n h Q E ell seeds) = seeds

theorem Algebraic.Cutwidth.Extractor.Internal.encode_decodeScheduledBlockSeeds (n h Q E ell : ℕ) (bits : List Bool) (length : bits.length = scheduledBlockSeedBits n h Q E ell) : encodeScheduledBlockSeeds n h Q E ell (decodeScheduledBlockSeeds n h Q E ell bits) = bits