Direct polynomial-time binary arithmetic

The existing carry folds are certified using plain machine closure. Reachable word states are bounded by the encoded input length, not the numeric operands. Strict comparison is the linear zip-transducer certificate of BinaryComparison. Captured multiplication uses the original shift-and-add fold over the first operand's bits, with the unchanged full-prefix state bound; its pair certificate remains private.

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

Addition of binary naturals, using the carry and remaining-word folds. Compose this certificate with the producers' .prod certificate. Global automatic addition remains separate from this named rule, since an unconstrained intermediate encoding can select a binary branch where a surrounding computation needs a unary size.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_lt : ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 < p.2)) (encPair encNat encNat) encBool

Strict comparison of binary naturals, from the linear zip-transducer certificate Turing.MultiTapeTM.computableInTimeAndSpace_natLt.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a * right a) input encNat

Multiply computed binary values, fixing their intermediate encodings for proof search.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_le : ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)) (encPair encNat encNat) encBool

Non-strict binary comparison, composed from the existing strict comparison certificate. Automatic composition uses the computed-operand rule binary_le'.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_le' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => decide (left a ≤ right a)) input encBool

Compare two binary naturals computed uniformly from the same encoded input.