Flat seed words for the near-halving recursion

The trivial initial seed occupies no bits. Fresh field seeds follow in increasing level order, then the final condenser and hash seeds. Each field uses its canonical coefficient word, and the final concatenation is grouped as (prefix ++ condenser) ++ hash.

Decoding is total on arbitrary words. Exact inverse laws apply to words of the prescribed length. These semantic codecs use no field enumeration.

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

Total width of the first i fresh field seeds, with an empty initial prefix.

Equations

• Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedPrefixBits n h Q E i = (Finset.range i).sum (Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedWidth n h Q E)

noncomputable def Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockSeedPrefix (n h Q E i : ℕ) : RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i → List Bool

Encode fresh seeds in level order; the initial Unit seed contributes no bits.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockSeedPrefix n h Q E 0 x_2 = []

noncomputable def Algebraic.Cutwidth.Extractor.decodeNearHalvingBlockSeedPrefix (n h Q E i : ℕ) : List Bool → RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i

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

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Extractor.decodeNearHalvingBlockSeedPrefix n h Q E 0 x✝ = ()

noncomputable def Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockSeeds (n h Q E : ℕ) (seeds : NearHalvingBlockSeeds n h Q E) : 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.decodeNearHalvingBlockSeeds (n h Q E : ℕ) (bits : List Bool) : NearHalvingBlockSeeds n h Q E

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

Equations

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