Direct binary powers with unary exponents

The captured repeated-multiplication algorithm is the existing binary-power recipe. Its reachable encoded lengths are bounded directly; no high-level tidy certificate is transported. The resulting number may have exponential value, but only polynomially many encoded bits. Like the direct binary-addition rule, this is a named certificate: it does not add an automatic binary branch to goals with an undetermined intermediate encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_pow : ComputableInPolyTime (fun (p : ℕ × ℕ) => p.1 ^ p.2) (encPair encNat encUnary) encNat

Raise a binary natural to a unary exponent using direct captured multiplication.