Exact binary enumeration and distinct positional advice

The natural-number codec round trips every word and every bounded index. Taking and dropping the known outer width recovers the two components of the concatenated advice, so all sampler positions receive distinct advice.

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

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

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

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

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