The existing binary long-division word algorithm

The public step, quotient/remainder laws and prefix encoding bound are moved unchanged from the higher division facade, independently of any higher computability calculus.

def Turing.MultiTapeTM.BinaryDiv.divModStep (b : ℕ) (state : ℕ × ℕ) (bit : Bool) : ℕ × ℕ

One shift-and-subtract step of binary long division with divisor b, state (q, r), and next most-significant dividend bit bit. When b = 0, the quotient remains 0 and the remainder accumulates the binary value of the dividend.

theorem Turing.MultiTapeTM.BinaryDiv.divModStep_div_mod (v b : ℕ) (bit : Bool) : divModStep b (v / b, v % b) bit = ((2 * v + bit.toNat) / b, (2 * v + bit.toNat) % b)

theorem Turing.MultiTapeTM.BinaryDiv.foldl_divModStep (b : ℕ) (word : List Bool) : List.foldl (divModStep b) (0, 0) word = (Cslib.BitString.binaryValue word / b, Cslib.BitString.binaryValue word % b)

Folding divModStep over any most-significant-first bit word computes the quotient and remainder of Cslib.BitString.binaryValue word by b.

theorem Turing.MultiTapeTM.BinaryDiv.divMod_eq (p : ℕ × ℕ) : List.foldl (divModStep p.2) (0, 0) p.1.bits.reverse = (p.1 / p.2, p.1 % p.2)

Folding divModStep over the reversed binary digits of p.1 computes (p.1 / p.2, p.1 % p.2).

theorem Turing.MultiTapeTM.BinaryDiv.length_encPair_foldl_divModStep_le (b : ℕ) (word : List Bool) : ((encPair encNat encNat) (List.foldl (divModStep b) (0, 0) word)).length ≤ 3 * word.length + 1

The encoded state after folding word has length at most 3 * word.length + 1.