Canonical seed words for the near-halving extractor

The initial Unit seed occupies the empty prefix. Each internal field seed is appended in level order, followed by the final condenser and hash seeds. The complete encoding is a bijection with words of exactly nearHalvingBlockSeedBits bits, for all parameters including zero depth.

Lengths, append order, and both inverse laws need no enumeration instances. The cardinality corollary accepts caller-supplied finite field instances. These are semantic representation results; runtime evaluation is separate.

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

Identity initialization spends no random bits.

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

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

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedBits_eq_prefix (n h Q E : ℕ) : have width := nearHalvingBlockWidth n h Q E h; have ell := nearHalvingBlockLeafLength h Q; nearHalvingBlockSeedBits n h Q E = nearHalvingBlockSeedPrefixBits 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.encodeNearHalvingBlockSeedPrefix_zero (n h Q E : ℕ) (seed : Unit) : encodeNearHalvingBlockSeedPrefix n h Q E 0 seed = []

The trivial initial seed encodes as the empty word.

theorem Algebraic.Cutwidth.Extractor.decodeNearHalvingBlockSeedPrefix_zero (n h Q E : ℕ) (bits : List Bool) : decodeNearHalvingBlockSeedPrefix n h Q E 0 bits = ()

The zero-level decoder always returns the trivial initial seed.

theorem Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockSeedPrefix_succ (n h Q E i : ℕ) (prior : RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i) (fresh : NearHalvingBlockLevelSeed n h Q E i) : encodeNearHalvingBlockSeedPrefix n h Q E (i + 1) (prior, fresh) = encodeNearHalvingBlockSeedPrefix n h Q E i prior ++ BinaryFieldCodec.encode (sparseFieldExponent (nearHalvingBlockRate h) (explicitCondenserBudget (nearHalvingBlockWidth n h Q E i) (nearHalvingBlockEntropy h Q i) E)) fresh

The next fresh field word follows all earlier field words.

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

Every prefix encoding has the prescribed sum of fresh field widths.

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

Decoding a canonical prefix recovers every retained seed.

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

Every word of the exact prefix width is recovered, preserving all coefficient zeros.

noncomputable def Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedPrefixEquiv (n h Q E i : ℕ) : RecursiveSeeds Unit (NearHalvingBlockLevelSeed n h Q E) i ≃ { bits : List Bool // bits.length = nearHalvingBlockSeedPrefixBits n h Q E i }

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

Equations

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

theorem Algebraic.Cutwidth.Extractor.encodeNearHalvingBlockSeeds_append (n h Q E : ℕ) (seeds : NearHalvingBlockSeeds n h Q E) : let width := nearHalvingBlockWidth n h Q E h; let ell := nearHalvingBlockLeafLength h Q; encodeNearHalvingBlockSeeds n h Q E seeds = encodeNearHalvingBlockSeedPrefix 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

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

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

The encoded word has exactly the complete near-halving seed budget.

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

The full decoder recovers every internal and final field seed.

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

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

noncomputable def Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedEquiv (n h Q E : ℕ) : NearHalvingBlockSeeds n h Q E ≃ { bits : List Bool // bits.length = nearHalvingBlockSeedBits n h Q E }

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

Equations

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

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedEquiv_apply (n h Q E : ℕ) (seeds : NearHalvingBlockSeeds n h Q E) : ↑((nearHalvingBlockSeedEquiv n h Q E) seeds) = encodeNearHalvingBlockSeeds n h Q E seeds

The forward seed equivalence is the canonical ordered encoding.

theorem Algebraic.Cutwidth.Extractor.nearHalvingBlockSeedEquiv_symm_apply (n h Q E : ℕ) (bits : { bits : List Bool // bits.length = nearHalvingBlockSeedBits n h Q E }) : (nearHalvingBlockSeedEquiv n h Q E).symm bits = decodeNearHalvingBlockSeeds n h Q E ↑bits

The inverse seed equivalence is the total decoder restricted to words of the exact width.

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

The exact number of semantic seeds is the power of two specified by their bit budget.