Exact enumeration and advice for the actual source reduction

Little-endian coding is a bijection between the finite enumeration range and Boolean words. Concatenating the outer and candidate codes assigns distinct advice of one fixed length to every actual sampler position.

theorem Algebraic.Cutwidth.Extractor.sourceReductionIndexWord_ofFn (width : ℕ) (index : Fin (2 ^ width)) : List.ofFn (sourceReductionIndexWord width index) = width.toBitsLE ↑index

Enumerated Boolean words serialize to the actual fixed-width binary encoder.

theorem Algebraic.Cutwidth.Extractor.sourceReductionWordIndex_indexWord (width : ℕ) (index : Fin (2 ^ width)) : sourceReductionWordIndex width (sourceReductionIndexWord width index) = index

Decoding an enumerated word recovers its index.

theorem Algebraic.Cutwidth.Extractor.sourceReductionIndexWord_wordIndex (width : ℕ) (word : Fin width → Bool) : sourceReductionIndexWord width (sourceReductionWordIndex width word) = word

Re-encoding a decoded word recovers every coordinate.

def Algebraic.Cutwidth.Extractor.sourceReductionIndexEquiv (width : ℕ) : Fin (2 ^ width) ≃ (Fin width → Bool)

The concrete little-endian enumeration is an equivalence, including at width zero.

Equations

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

theorem Algebraic.Cutwidth.Extractor.sourceReductionAdvice_length (outerBits candidateBits : ℕ) (position : Fin (2 ^ outerBits) × Fin (2 ^ candidateBits)) : (sourceReductionAdvice outerBits candidateBits position).length = outerBits + candidateBits

Every actual position receives advice of the same total width.

theorem Algebraic.Cutwidth.Extractor.sourceReductionAdvice_injective (outerBits candidateBits : ℕ) : Function.Injective (sourceReductionAdvice outerBits candidateBits)

Distinct outer/candidate positions receive distinct advice words.