Direct certificates for the existing binary subtraction and division algorithms

The word programs and their arithmetic laws are unchanged. Subtraction reuses the shared charged schoolbook certificate. Division uses direct bit, pair, append and full-prefix fold primitives, retaining binary magnitudes throughout.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_sub : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 - p.2) (encPair encNat encNat) encNat

Truncated binary subtraction, reusing the shared charged schoolbook certificate. The quantitative interface takes the subtrahend first, so swap the two computed operands.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_divMod : ComputableInPolyTime (fun (p : ℕ × ℕ) => (p.1 / p.2, p.1 % p.2)) (encPair encNat encNat) (encPair encNat encNat)

Quotient and remainder by the original shift-and-subtract binary long division. The zero-divisor branch is retained; both outputs stay binary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_div : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 / p.2) (encPair encNat encNat) encNat

Binary quotient, with a / 0 = 0. This named rule adds no encoding-search alternative.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_mod : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 % p.2) (encPair encNat encNat) encNat

Binary remainder, with a % 0 = a. This named rule adds no encoding-search alternative.