Concrete indices and advice for the source reduction

Enumerate Boolean words by their fixed-width little-endian binary codes. The advice for a sampler position concatenates its outer and candidate codes. These are the actual computable encodings used by the reduction; no arbitrary equivalence between finite types is chosen.

def Algebraic.Cutwidth.Extractor.sourceReductionIndexWord (width : ℕ) (index : Fin (2 ^ width)) (j : Fin width) : Bool

The fixed-width little-endian word at a finite enumeration index.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionIndexWord width index j = (width.toBitsLE ↑index)[↑j]?.getD false

def Algebraic.Cutwidth.Extractor.sourceReductionWordIndex (width : ℕ) (word : Fin width → Bool) : Fin (2 ^ width)

The exact finite index of a Boolean word under little-endian enumeration.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionWordIndex width word = ⟨Nat.fromBitsLE (List.ofFn word), ⋯⟩

def Algebraic.Cutwidth.Extractor.sourceReductionAdvice (outerBits candidateBits : ℕ) (position : Fin (2 ^ outerBits) × Fin (2 ^ candidateBits)) : List Bool

Concatenate the outer and candidate codes to give unique equal-length advice.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionAdvice outerBits candidateBits position = outerBits.toBitsLE ↑position.1 ++ candidateBits.toBitsLE ↑position.2