Direct unary comparison and bit-access frontends

These canonical interfaces use direct unary iteration (ComputableInPolyTime.iterate): unary subtraction iterates predecessor, unary-to-binary conversion iterates the binary successor, and indexed access iterates the word tail before using the existing head codec. No higher tidy calculus supplies a plain primitive.

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

Truncated subtraction of unary naturals.

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

Comparison of unary naturals.

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

Strict comparison of unary naturals.

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

Compare computed unary values, with both operand encodings fixed.

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

Strictly compare computed unary values, with both operand encodings fixed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_to_binary : ComputableInPolyTime (fun (n : ℕ) => n) encUnary encNat

Convert a unary natural to its binary encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsGetD (fallback : Bool) : ComputableInPolyTime (fun (p : List Bool × ℕ) => p.1.getD p.2 fallback) (encPair encBits encUnary) encBool

Read a bit at a unary index with a fixed fallback. Fixing the raw encoding avoids guessing a list-encoding instance during compositional proof search.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_testBit {α : Type} {input : α ↪ List Bool} {n i : α → ℕ} (hn : ComputableInPolyTime n input encNat) (hi : ComputableInPolyTime i input encUnary) : ComputableInPolyTime (fun (a : α) => (n a).testBit (i a)) input encBool

Read the bit of a computed binary number at a computed unary position.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_testBit' {α : Type} {input : α ↪ List Bool} {n i : α → ℕ} (hn : ComputableInPolyTime n input encUnary) (hi : ComputableInPolyTime i input encUnary) : ComputableInPolyTime (fun (a : α) => (n a).testBit (i a)) input encBool

Read the bit of a computed unary number at a computed unary position.