The scheduled finite recursive extractor

The initial rate-one condenser compresses the source to one Boolean block. Each executed level uses the rate-three paired condenser at the prescribed entropy and the actual current width. A shared one-shot extractor finishes all leaves. The complete semantic map retains its initial, level, and final field seeds exactly once. Its uniform bit evaluator is a separate construction.

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

Exact width of the initial compressed block.

Equations

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

@[reducible, inline]

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

Field seed for the initial compression.

Equations

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

@[reducible, inline]

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

One fresh field seed for an internal level.

Equations

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

@[reducible, inline]

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

The pair of independent field seeds shared by all final leaf extractors.

Equations

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

def Algebraic.Cutwidth.Extractor.scheduledBlockSeedBits (n h Q E ell : ℕ) : ℕ

Total number of bits in the initial, internal, and final field seeds.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.scheduledBlockInitial (n h Q E : ℕ) (x : Fin n → Bool) (seed : ScheduledInitialSeed n h Q E) : Fin (scheduledBlockInitialWidth n h Q E) → Bool

Recombine both initial condenser halves into its full compressed Boolean block.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.scheduledBlockStep (n h Q E i : ℕ) (x : Fin (recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E i) → Bool) (seed : ScheduledLevelSeed n h Q E i) : (Fin (recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E (i + 1)) → Bool) × (Fin (recursiveBlockWidth (scheduledBlockInitialWidth n h Q E) h Q E (i + 1)) → Bool)

The actual paired condenser used at each internal level.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.scheduledBlockExtractor (n h Q E ell : ℕ) (x : Fin n → Bool) (seeds : RecursiveSeeds (ScheduledInitialSeed n h Q E) (ScheduledLevelSeed n h Q E) h × ScheduledFinalSeed n h Q E ell) : Fin (recursiveBlockCount 1 h) → Fin ell → ZMod 2

The complete finite semantic extractor, with every component and seed type specified.

Equations

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