Canonical seed-word equivalences for the scheduled extractor

One flat word contains the initial seed, fresh level seeds in increasing order, and the final condenser and hash seeds. Prefix append laws and exact widths expose the same layout to a runtime loop. The complete word has exactly scheduledBlockSeedBits bits, and its codec is a bijection at that length, including zero-depth schedules.

These are finite representation results built from BinaryFieldCodec and list splitting. They need no enumeration instances and make no polynomial-time claim about operations on abstract field elements or the complete recursion.

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

The zero-level prefix contains only the initial field seed.

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

A prefix grows by the exact field width of its next fresh seed.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockSeedBits_eq_prefix (n h Q E ell : ℕ) : have width := recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E h; scheduledBlockSeedBits n h Q E ell = scheduledBlockSeedPrefixBits n h Q E h + (2 * 3 ^ oneShotCondenserExponent width ell E + 2 * 3 ^ oneShotHashExponent width ell E)

The full width consists of the recursive prefix and the final seed pair.

theorem Algebraic.Cutwidth.Extractor.encodeScheduledBlockSeedPrefix_zero (n h Q E : ℕ) (seed : ScheduledInitialSeed n h Q E) : encodeScheduledBlockSeedPrefix n h Q E 0 seed = BinaryFieldCodec.encode (sparseFieldExponent 1 (explicitCondenserBudget n (recursiveBlockEntropy h Q 0) E)) seed

The zero-level encoding is the initial field's canonical word.

theorem Algebraic.Cutwidth.Extractor.encodeScheduledBlockSeedPrefix_succ (n h Q E i : ℕ) (prior : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i) (fresh : ScheduledLevelSeed n h Q E i) : encodeScheduledBlockSeedPrefix n h Q E (i + 1) (prior, fresh) = encodeScheduledBlockSeedPrefix n h Q E i prior ++ BinaryFieldCodec.encode (sparseFieldExponent 3 (explicitCondenserBudget (recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E i) (recursiveBlockEntropy h Q i) E)) fresh

The next fresh seed is appended after all earlier seeds.

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

Every prefix encoding has its prescribed initial-plus-level width.

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

Decoding a canonical prefix recovers all its semantic field seeds.

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

Every word of the exact prefix width is recovered, including coefficient padding.

noncomputable def Algebraic.Cutwidth.Extractor.scheduledBlockSeedPrefixEquiv (n h Q E i : ℕ) : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i ≃ { bits : List Bool // bits.length = scheduledBlockSeedPrefixBits n h Q E i }

A recursive seed prefix is equivalent to one word of its exact width.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Extractor.encodeScheduledBlockSeeds_append (n h Q E ell : ℕ) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) : let width := recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E h; encodeScheduledBlockSeeds n h Q E ell seeds = encodeScheduledBlockSeedPrefix n h Q E h seeds.1 ++ BinaryFieldCodec.encode (oneShotCondenserExponent width ell E) seeds.2.1 ++ BinaryFieldCodec.encode (oneShotHashExponent width ell E) seeds.2.2

The final words follow the prefix in condenser-then-hash order, with left grouping.

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

The flat seed word has exactly the previously specified complete seed budget.

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

The full decoder recovers every initial, internal, and final field seed.

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

Every word of the full prescribed length is its decoded tuple's exact encoding.

noncomputable def Algebraic.Cutwidth.Extractor.scheduledBlockSeedEquiv (n h Q E ell : ℕ) : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell ≃ { bits : List Bool // bits.length = scheduledBlockSeedBits n h Q E ell }

The complete semantic seed tuple is equivalent to a flat word of the exact total width.

Equations

• One or more equations did not get rendered due to their size.