Copying canonical binary naturals -- proof internals

The copy machine first clears its destination and then invokes width-linear ripple addition with the source and zero counter as preserved operands. These proofs compose the public literal-frame and all-prefix contracts of both phases, then recover the original literal copy frame from canonicality.

def Complexity.TM.binaryCopyNatTape (value : ℕ) : Tape

Canonical parked tape encoding of a natural for binary copying.

Equations

• Complexity.TM.binaryCopyNatTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

theorem Complexity.TM.binaryCopyTime_le_internal (srcValue dstValue : ℕ) : binaryCopyTime srcValue dstValue ≤ 3 * srcValue.size + 2 * dstValue.size + 20

theorem Complexity.TM.binaryCopyIntoTM_hoareTime_frame_internal {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) (hsrcDst : srcIdx ≠ dstIdx) (hsrcCounter : srcIdx ≠ counterIdx) (hdstCounter : dstIdx ≠ counterIdx) (srcValue dstValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrc : (work₀ srcIdx).HasBinaryNat srcValue) (hdst : (work₀ dstIdx).HasBinaryNat dstValue) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ srcIdx → i ≠ dstIdx → i ≠ counterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryCopyIntoTM srcIdx dstIdx counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ dstIdx (binaryCopyNatTape srcValue) ∧ out = out₀) (binaryCopyTime srcValue dstValue)

theorem Complexity.TM.binaryCopyIntoTM_hoareTimeSpace_frame_internal {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) (hsrcDst : srcIdx ≠ dstIdx) (hsrcCounter : srcIdx ≠ counterIdx) (hdstCounter : dstIdx ≠ counterIdx) (srcValue dstValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrc : (work₀ srcIdx).HasBinaryNat srcValue) (hdst : (work₀ dstIdx).HasBinaryNat dstValue) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ srcIdx → i ≠ dstIdx → i ≠ counterIdx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryCopyIntoTM srcIdx dstIdx counterIdx).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ dstIdx (binaryCopyNatTape srcValue) ∧ out = out₀) (binaryCopyTime srcValue dstValue) inputLength (binaryCopySpace initialSpace srcValue dstValue)

theorem Complexity.TM.binaryCopyIntoTM_isTransducer_internal {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (binaryCopyIntoTM srcIdx dstIdx counterIdx).IsTransducer