Two equal bit-vector outputs from the scheduled condenser

Every selected field element has width 2 * 3^s, so the complete coordinate output has even length. Split that actual output word into two consecutive halves, without adding padding or dropping any coordinate bits.

The semantic field seed is encoded by the existing quotient codec before calling the runtime condenser. These definitions add no new randomness or parameter promise; their statistical guarantees require a positive rate.

def Algebraic.Cutwidth.Extractor.explicitCondenserHalfWidth (n k e u : ℕ) : ℕ

Half the scheduled condenser's exact bit-output length.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.explicitCondenserPair (n k e u : ℕ) (x : Fin n → Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : (Fin (explicitCondenserHalfWidth n k e u) → Bool) × (Fin (explicitCondenserHalfWidth n k e u) → Bool)

Read the first and second halves of the actual scheduled output at a canonical field seed.

Equations

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