Direct signed shifts and runtime radix digits

Named certificates keep natural magnitudes binary and digit positions unary. Quotient iteration only decreases the magnitude, so its prefix bound follows from the encoded input, not from the numeric value of the dividend. No global encoding-search rule or raw transport is added.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_subNatNat : ComputableInPolyTime (fun (p : ℕ × ℕ) => Int.subNatNat p.1 p.2) (encPair encNat encNat) encIntBin

Shift a natural digit by a natural radius, returning an ordinary sign-magnitude integer. This is the existing Int.subNatNat function, not a second integer representation.

theorem Turing.MultiTapeTM.ComputableInPolyTime.radix_digit : ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => Cslib.Radix.digit p.1.1 p.1.2 p.2) (encPair (encPair encNat encNat) encUnary) encNat

Read the existing radix digit with binary base/value and a unary runtime position. The certificate is total, including bases zero and one.