Flat seed words for the scheduled recursive extractor

The initial field seed is followed by the fresh level seeds in increasing order, then the final condenser and hash seeds. Each field element uses its canonical coefficient word. Prefixes grow by appending the next level seed; the full encoding groups the final appends as (prefix ++ condenser) ++ hash.

The total decoders split at these fixed widths. Inverse laws apply to words of the exact stated length. These are semantic codecs, with no field enumeration or runtime assertion.

def Algebraic.Cutwidth.Extractor.scheduledBlockSeedPrefixBits (n h Q E i : ℕ) : ℕ

Width of the initial field seed and the first i fresh level seeds.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.encodeScheduledBlockSeedPrefix (n h Q E i : ℕ) : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i → List Bool

Encode the initial seed followed by the executed fresh seeds in order.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.decodeScheduledBlockSeedPrefix (n h Q E i : ℕ) : List Bool → RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) i

Decode a prefix by splitting off its last fresh field word at the fixed prior width.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.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) : List Bool

Encode the recursive seed prefix, final condenser seed, then final hash seed.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.decodeScheduledBlockSeeds (n h Q E ell : ℕ) (bits : List Bool) : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell

Decode the recursive prefix and the two final field words at their fixed offsets.

Equations

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