The recursive extractor with a near-halving entropy schedule

Start with the original Boolean input as a single block, with a trivial initial seed. Every internal level uses the actual paired condenser at rate 16*(h+1), its scheduled entropy, and its current rounded width. The final one-shot extractor is shared by all leaves. The complete tuple retains every fresh field seed and the final independent seed pair once.

This specifies the semantic construction. Its numerical budgets, extraction guarantee, Boolean seed representation, and evaluator are separate layers.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.NearHalvingBlockLevelSeed (n h Q E i : ℕ) : Type

The fresh field seed at one internal level of the near-halving recursion.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.NearHalvingBlockFinalSeed (n h Q E : ℕ) : Type

The final condenser and hash seeds, shared across every leaf.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.Extractor.NearHalvingBlockSeeds (n h Q E : ℕ) : Type

All retained seeds, with no random bits spent on the identity initialization.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.nearHalvingBlockStep (n h Q E i : ℕ) (x : Fin (nearHalvingBlockWidth n h Q E i) → Bool) (seed : NearHalvingBlockLevelSeed n h Q E i) : (Fin (nearHalvingBlockWidth n h Q E (i + 1)) → Bool) × (Fin (nearHalvingBlockWidth n h Q E (i + 1)) → Bool)

The actual paired condenser for one near-halving level.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.nearHalvingBlockExtractor (n h Q E : ℕ) (x : Fin n → Bool) (seeds : NearHalvingBlockSeeds n h Q E) : Fin (recursiveBlockCount 1 h) → Fin (nearHalvingBlockLeafLength h Q) → ZMod 2

The actual near-halving recursion followed by shared extraction at its leaves.

Equations

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