RAM snapshot word-width decoder

This module exposes the exact framed semantics of the first concrete snapshot decoder phase. Starting on a self-delimiting word, wordWidthTM stops on its zero separator and leaves the unary-prefix length as a canonical binary natural on a separate work tape.

theorem Complexity.RAM.RegisterStore.Machine.wordTargetRewind_reachesIn_frame {n : ℕ} (targetIdx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (htarget : (work₀ targetIdx).HasBinaryPrefix bits) (htargetStart : (work₀ targetIdx).cells 0 = Γ.start) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ targetIdx → (work₀ i).read ≠ Γ.start ∧ 1 ≤ (work₀ i).head) (houtput : out₀.read ≠ Γ.start) (houtputHead : 1 ≤ out₀.head) : ∃ (c' : Complexity.Cfg n (TM.rewindWorkTM targetIdx).Q), ∃ t ≤ bits.length + 3, (TM.rewindWorkTM targetIdx).reachesIn t { state := (TM.rewindWorkTM targetIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (TM.rewindWorkTM targetIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work targetIdx).HasBinaryString bits ∧ (∀ (i : Fin n), i ≠ targetIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Rewind a decoded append-position target to cell one without changing its binary contents or any framed tape. This converts HasBinaryPrefix into the read-position convention HasBinaryString in at most |bits| + 3 steps.

theorem Complexity.RAM.RegisterStore.Machine.wordWidthTM_reachesIn_frame {n : ℕ} (sourceIdx widthIdx : Fin n) (hindices : sourceIdx ≠ widthIdx) (width : ℕ) (payload : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (List.replicate width true ++ false :: payload)) (hwidth : (work₀ widthIdx).HasBinaryNat 0) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (wordWidthTM sourceIdx widthIdx).Q), (wordWidthTM sourceIdx widthIdx).reachesIn (wordWidthTime width) { state := (wordWidthTM sourceIdx widthIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordWidthTM sourceIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix (false :: payload) ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Exact framed execution of unary-width decoding. The source begins at the first prefix bit, the width counter begins at canonical zero, and all unrelated tapes are preserved exactly.

theorem Complexity.RAM.RegisterStore.Machine.wordWidthTM_isTransducer {n : ℕ} (sourceIdx widthIdx : Fin n) : (wordWidthTM sourceIdx widthIdx).IsTransducer

Unary-width decoding is safe for one-way-output composition.

theorem Complexity.RAM.RegisterStore.Machine.payloadBitTM_reachesIn_frame {n : ℕ} (sourceIdx targetIdx : Fin n) (hindices : sourceIdx ≠ targetIdx) (bit : Bool) (suffix pre : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (bit :: suffix)) (htarget : (work₀ targetIdx).HasBinaryPrefix pre) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (payloadBitTM sourceIdx targetIdx).Q), (payloadBitTM sourceIdx targetIdx).reachesIn 1 { state := (payloadBitTM sourceIdx targetIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (payloadBitTM sourceIdx targetIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix suffix ∧ (c'.work targetIdx).HasBinaryPrefix (pre ++ [bit]) ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Exact one-step framed execution of the payload-copy leaf. It consumes one source bit, appends it to the target, and preserves every unrelated tape.

theorem Complexity.RAM.RegisterStore.Machine.payloadBitTM_isTransducer {n : ℕ} (sourceIdx targetIdx : Fin n) : (payloadBitTM sourceIdx targetIdx).IsTransducer

The one-bit payload copier never moves the output head left.

theorem Complexity.RAM.RegisterStore.Machine.wordSeparatorTM_reachesIn_frame {n : ℕ} (sourceIdx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (false :: bits)) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (wordSeparatorTM sourceIdx).Q), (wordSeparatorTM sourceIdx).reachesIn 1 { state := (wordSeparatorTM sourceIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordSeparatorTM sourceIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix bits ∧ (∀ (i : Fin n), i ≠ sourceIdx → c'.work i = work₀ i) ∧ c'.output = out₀

The separator phase consumes one zero and otherwise preserves the frame.

theorem Complexity.RAM.RegisterStore.Machine.wordPayloadTM_reachesIn_frame {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) (hdistinct : PayloadLoopDistinct sourceIdx targetIdx counterIdx widthIdx) (payload rest : List Bool) (width : ℕ) (hwidthLength : payload.length = width) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (payload ++ rest)) (htarget : (work₀ targetIdx).HasBinaryPrefix []) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hwidth : (work₀ widthIdx).HasBinaryNat width) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).Q), (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).reachesIn (wordPayloadTime width) { state := (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix payload ∧ (c'.work counterIdx).HasBinaryNat width ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Exact framed execution of the bounded payload loop. The source begins on the first payload bit, the target is an empty appendable prefix, the counter is zero, and the preserved width tape equals the payload length. The machine copies the complete payload and leaves the source at the next encoded word.

theorem Complexity.RAM.RegisterStore.Machine.wordPayloadTM_isTransducer {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) : (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).IsTransducer

The bounded payload loop preserves one-way-output safety.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeTM_reachesIn_frame {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) (hdistinct : PayloadLoopDistinct sourceIdx targetIdx counterIdx widthIdx) (payload rest : List Bool) (width : ℕ) (hwidthLength : 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 []) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hwidth : (work₀ widthIdx).HasBinaryNat 0) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).Q), (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).reachesIn (wordDecodeTime width) { state := (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix payload ∧ (c'.work counterIdx).HasBinaryNat width ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Exact end-to-end decoding of one self-delimiting width/payload layout. The source is left at the next word and the target contains the complete payload as an appendable binary prefix.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeTM_prefix_withinAuxSpace {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) (width inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).reachesIn time start current) (htime : time ≤ wordDecodeTime width) : current.WithinAuxSpace inputLength (initialSpace + wordDecodeTime width)

Coarse all-prefix space envelope for complete word decoding. Starting from auxiliary-space budget initialSpace, no prefix of the exact decoder run can use more than initialSpace + wordDecodeTime width; this follows from the one-cell-per-transition head-growth bound and is independent of endpoint correctness.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeTM_reachesIn_frame_encode {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) (hdistinct : PayloadLoopDistinct sourceIdx targetIdx counterIdx widthIdx) (value : ℕ) (rest : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (WordCode.encode value ++ rest)) (htarget : (work₀ targetIdx).HasBinaryPrefix []) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hwidth : (work₀ widthIdx).HasBinaryNat 0) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).Q), (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).reachesIn (wordDecodeTime (bitlen value)) { state := (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix value.bits ∧ (c'.work counterIdx).HasBinaryNat (bitlen value) ∧ (c'.work widthIdx).HasBinaryNat (bitlen value) ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀

A canonical WordCode.encode prefix decodes to the natural's canonical little-endian bit string and leaves the following encoded stream untouched.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeTime_le_size (width : ℕ) : wordDecodeTime width ≤ 8 * (width + 1) * (width.size + 2)

The existing checked decoder is quasi-linear in the decoded word width. This tightens the former quadratic charging by retaining the bit-width of the binary loop limit instead of replacing it by the limit's numeric value.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeTM_isTransducer {n : ℕ} (sourceIdx targetIdx counterIdx widthIdx : Fin n) : (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).IsTransducer

Complete word decoding preserves one-way-output safety.

Linear unary-marker decoder

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTM_reachesIn_frame {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' : Complexity.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₀

Exact framed execution of the optimized decoder. It uses one unary marker instead of a binary width/counter pair and takes exactly 3 * width + 3 transitions.

theorem Complexity.RAM.RegisterStore.Machine.wordDecodeLinearTM_reachesIn_frame_encode {n : ℕ} (sourceIdx targetIdx markerIdx : Fin n) (hdistinct : LinearWordDistinct sourceIdx targetIdx markerIdx) (value : ℕ) (rest : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsource : (work₀ sourceIdx).HasBinarySuffix (WordCode.encode value ++ 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' : Complexity.Cfg n (wordDecodeLinearTM sourceIdx targetIdx markerIdx).Q), (wordDecodeLinearTM sourceIdx targetIdx markerIdx).reachesIn (wordDecodeLinearTime (bitlen value)) { 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 value.bits ∧ (c'.work markerIdx).HasBinaryPrefix (List.replicate (bitlen value) true) ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ markerIdx → c'.work i = work₀ i) ∧ c'.output = out₀

The optimized decoder handles a canonical natural-number word in time linear in the encoded word width.

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

The optimized decoder never moves the output head left.