Counting and bounding the scheduled field seeds

The nested seed tuple has one factor for each retained field seed. Exact finite-field cardinalities turn this product into a power of two. Sparse rounding and the finite width schedule then bound its exponent.

theorem Algebraic.Cutwidth.Extractor.Internal.card_scheduledBlockSeeds (n h Q E ell : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : Fintype.card (RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) = 2 ^ scheduledBlockSeedBits n h Q E ell

theorem Algebraic.Cutwidth.Extractor.Internal.scheduledBlockSeedBits_le (n L E h : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (depth : h ≤ L) : scheduledBlockSeedBits n h (recursiveBlockReserve L E) E L ≤ 8192 * (L + (h + 1) * (E + h + Nat.clog 2 (L + E + 1) + 1))