Exact widths and inverse laws for near-halving seed words

The prefix induction starts at the empty word and appends one canonical field word at each level. The final two fields use the same fixed-width splitting. The resulting equivalence with Boolean words also gives the exact cardinality, without any field enumeration in the codec.

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockSeedPrefixBits_zero (n h Q E : ℕ) : nearHalvingBlockSeedPrefixBits n h Q E 0 = 0

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockSeedPrefixBits_succ (n h Q E i : ℕ) : nearHalvingBlockSeedPrefixBits n h Q E (i + 1) = nearHalvingBlockSeedPrefixBits n h Q E i + nearHalvingBlockSeedWidth n h Q E i

theorem Algebraic.Cutwidth.Extractor.Internal.encodeNearHalvingBlockSeedPrefix_length (n h Q E i : ℕ) (seeds : RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i) : (encodeNearHalvingBlockSeedPrefix n h Q E i seeds).length = nearHalvingBlockSeedPrefixBits n h Q E i

theorem Algebraic.Cutwidth.Extractor.Internal.decode_encodeNearHalvingBlockSeedPrefix (n h Q E i : ℕ) (seeds : RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i) : decodeNearHalvingBlockSeedPrefix n h Q E i (encodeNearHalvingBlockSeedPrefix n h Q E i seeds) = seeds

theorem Algebraic.Cutwidth.Extractor.Internal.encode_decodeNearHalvingBlockSeedPrefix (n h Q E i : ℕ) (bits : List Bool) (length : bits.length = nearHalvingBlockSeedPrefixBits n h Q E i) : encodeNearHalvingBlockSeedPrefix n h Q E i (decodeNearHalvingBlockSeedPrefix n h Q E i bits) = bits

theorem Algebraic.Cutwidth.Extractor.Internal.encodeNearHalvingBlockSeeds_length (n h Q E : ℕ) (seeds : NearHalvingBlockSeeds n h Q E) : (encodeNearHalvingBlockSeeds n h Q E seeds).length = nearHalvingBlockSeedBits n h Q E

theorem Algebraic.Cutwidth.Extractor.Internal.decode_encodeNearHalvingBlockSeeds (n h Q E : ℕ) (seeds : NearHalvingBlockSeeds n h Q E) : decodeNearHalvingBlockSeeds n h Q E (encodeNearHalvingBlockSeeds n h Q E seeds) = seeds

theorem Algebraic.Cutwidth.Extractor.Internal.encode_decodeNearHalvingBlockSeeds (n h Q E : ℕ) (bits : List Bool) (length : bits.length = nearHalvingBlockSeedBits n h Q E) : encodeNearHalvingBlockSeeds n h Q E (decodeNearHalvingBlockSeeds n h Q E bits) = bits

theorem Algebraic.Cutwidth.Extractor.Internal.card_nearHalvingBlockSeeds (n h Q E : ℕ) [(s : ℕ) → Fintype (AdjoinRoot (binaryModulus s))] : Fintype.card (NearHalvingBlockSeeds n h Q E) = 2 ^ nearHalvingBlockSeedBits n h Q E