Direct polynomial-time binary arithmetic

Addition and comparison are the linear zip-transducer certificates of BinaryAddition and BinaryComparison. Multiplication weakens the cubic-time schoolbook certificate ComputableInO.natMul.

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

Addition of binary naturals, from the linear zip-transducer certificate Turing.MultiTapeTM.computableInTimeAndSpace_natAdd. 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, from the linear zip-transducer certificate Turing.MultiTapeTM.computableInTimeAndSpace_natLe. 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.