Linear RAM snapshot word decoder — proof internals

This file proves the exact three-pass behavior of wordDecodeLinearTM: copy the unary width to a marker tape, rewind those markers, then consume one marker while copying one payload bit. Each pass is linear in the encoded word width.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTM_reachesIn_frame_internal {n : ℕ} (sourceIdx targetIdx markerIdx : Fin n) (hdistinct : LinearWordDistinct sourceIdx targetIdx markerIdx) (payload rest : List Bool) (width : ℕ) (hwidth : payload.length = width) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (List.replicate width true ++ false :: (payload ++ rest))) (htarget : (work₀ targetIdx).HasBinaryPrefix []) (hmarker : (work₀ markerIdx).HasBinaryPrefix []) (hmarkerStart : (work₀ markerIdx).cells 0 = Γ.start) (hinput : inp₀.read ≠ Γ.start) (hreads : ∀ (i : Fin n), (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (wordDecodeLinearTM sourceIdx targetIdx markerIdx).Q), (wordDecodeLinearTM sourceIdx targetIdx markerIdx).reachesIn (wordDecodeLinearTime width) { state := (wordDecodeLinearTM sourceIdx targetIdx markerIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordDecodeLinearTM sourceIdx targetIdx markerIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix payload ∧ (c'.work markerIdx).HasBinaryPrefix (List.replicate width true) ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ markerIdx → c'.work i = work₀ i) ∧ c'.output = out₀

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTM_isTransducer_internal {n : ℕ} (sourceIdx targetIdx markerIdx : Fin n) : (wordDecodeLinearTM sourceIdx targetIdx markerIdx).IsTransducer