Copying canonical binary naturals

This module exposes a literal-frame copy operation assembled from work-tape clearing and width-linear ripple addition. The source is preserved, the destination becomes an exact copy, and the zero scratch is restored literally.

Main results

• TM.binaryCopyIntoTM_hoareTime_frame gives the literal endpoint and time bound.
• TM.binaryCopyIntoTM_hoareTimeSpace_frame adds an all-prefix width bound.
• TM.binaryCopyTime_le exposes the linear operand-width envelope.
• TM.binaryCopyIntoTM_isTransducer proves append-only-output safety.

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

Canonical binary copying is linear in the source and old-destination widths.

theorem Complexity.TM.binaryCopyIntoTM_hoareTime_frame {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 ((Tape.init (List.map Γ.ofBool srcValue.bits)).move Dir3.right) ∧ out = out₀) (binaryCopyTime srcValue dstValue)

Binary copying changes only the destination tape. The source, zero counter, input, output, and every unrelated work tape are preserved literally.

theorem Complexity.TM.binaryCopyIntoTM_hoareTimeSpace_frame {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 ((Tape.init (List.map Γ.ofBool srcValue.bits)).move Dir3.right) ∧ out = out₀) (binaryCopyTime srcValue dstValue) inputLength (binaryCopySpace initialSpace srcValue dstValue)

Time-and-space form of canonical binary copying. Every reachable configuration stays within the maximum of the clearing and ripple-addition bounds.

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

Canonical binary copying never moves the output head left.