Unsigned binary minimum

This module exposes a linear-size fan-in-two circuit that compares two little-endian words and returns the word with smaller unsigned value.

@[simp]

theorem Complexity.BitString.unsignedValue_unsignedMin {width : ℕ} (left right : BitString width) : (left.unsignedMin right).unsignedValue = min left.unsignedValue right.unsignedValue

Selecting the smaller word also selects the minimum unsigned value.

@[simp]

theorem Complexity.Circuit.size_unsignedLEWithPayload (width : ℕ) [NeZero width] : (unsignedLEWithPayload width).size = 17 * width + 1

The comparator-with-payload circuit has exact linear size.

@[simp]

theorem Complexity.Circuit.eval_unsignedLEWithPayload (width : ℕ) [NeZero width] (left right : BitString width) : (unsignedLEWithPayload width).eval (Fin.append left right) = BitString.multiplexerInput (decide (left.unsignedValue ≤ right.unsignedValue)) left right

Comparator-with-payload emits its decision bit before the original words.

@[simp]

theorem Complexity.Circuit.size_unsignedMin (width : ℕ) [NeZero width] : (unsignedMin width).size = 20 * width + 1

The unsigned-minimum selector has exact linear size.

@[simp]

theorem Complexity.Circuit.eval_unsignedMin (width : ℕ) [NeZero width] (left right : BitString width) : (unsignedMin width).eval (Fin.append left right) = left.unsignedMin right

The selector returns the smaller unsigned word, choosing left on ties.