Self-delimiting word emission #
theorem
Complexity.RAM.RegisterStore.Machine.workEmitTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(mode : WorkEmitMode)
(bits emitted : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ idx).HasBinarySuffix bits)
(hinput : TM.Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i))
(houtput : out₀.HasBinaryPrefix emitted)
:
(workEmitTM idx mode).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = (work₀ idx).head + bits.length ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ workEmitBits mode bits))
(workEmitTime bits)
One generic work-tape pass appends either the unary width header or the payload bits while preserving input and every unrelated work tape exactly.
theorem
Complexity.RAM.RegisterStore.Machine.wordEncodeTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(value : ℕ)
(emitted : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hvalue : (work₀ idx).HasBinaryNat value)
(hinput : TM.Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i))
(houtput : out₀.HasBinaryPrefix emitted)
:
(wordEncodeTM idx).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = value.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ WordCode.encode value))
(wordEncodeTime value)
Emit WordCode.encode value from a canonical natural-number work tape,
preserving the input, source cells, and every unrelated work tape exactly.
theorem
Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTM_hoareTime_frame
{n : ℕ}
(idx : Fin n)
(value headBound : ℕ)
(emitted : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hcontent : (work₀ idx).HasBinaryContent value.bits)
(hstart : (work₀ idx).cells 0 = Γ.start)
(hhead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound)
(hinput : TM.Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → TM.Parked (work₀ i))
(houtput : out₀.HasBinaryPrefix emitted)
:
(rewindWordEncodeTM idx).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 idx).HasBinarySuffix [] ∧ (work idx).cells = (work₀ idx).cells ∧ (work idx).head = value.bits.length + 1 ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out.HasBinaryPrefix (emitted ++ WordCode.encode value))
(rewindWordEncodeTime value headBound)
Rewind any bounded cursor over canonical binary contents and emit the complete self-delimiting word, retaining a literal external frame.
theorem
Complexity.RAM.RegisterStore.Machine.workEmitTM_isTransducer
{n : ℕ}
(idx : Fin n)
(mode : WorkEmitMode)
:
(workEmitTM idx mode).IsTransducer
Each emission pass is append-only on the output tape.
theorem
Complexity.RAM.RegisterStore.Machine.wordEncodeTM_isTransducer
{n : ℕ}
(idx : Fin n)
:
(wordEncodeTM idx).IsTransducer
Complete word emission is append-only on the output tape.
theorem
Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTM_isTransducer
{n : ℕ}
(idx : Fin n)
:
Rewind-and-emit word encoding is append-only on the output tape.
theorem
Complexity.RAM.RegisterStore.Machine.workEmitTM_prefix_withinAuxSpace
{n : ℕ}
(idx : Fin n)
(mode : WorkEmitMode)
(bits : List Bool)
(inputLength initialSpace time : ℕ)
(start current : Complexity.Cfg n (workEmitTM idx mode).Q)
(hinitial : start.WithinAuxSpace inputLength initialSpace)
(hreach : (workEmitTM idx mode).reachesIn time start current)
(htime : time ≤ workEmitTime bits)
:
current.WithinAuxSpace inputLength (initialSpace + workEmitTime bits)
Coarse all-prefix auxiliary-space envelope for one emission pass.
theorem
Complexity.RAM.RegisterStore.Machine.wordEncodeTM_prefix_withinAuxSpace
{n : ℕ}
(idx : Fin n)
(value inputLength initialSpace time : ℕ)
(start current : Complexity.Cfg n (wordEncodeTM idx).Q)
(hinitial : start.WithinAuxSpace inputLength initialSpace)
(hreach : (wordEncodeTM idx).reachesIn time start current)
(htime : time ≤ wordEncodeTime value)
:
current.WithinAuxSpace inputLength (initialSpace + wordEncodeTime value)
Coarse all-prefix auxiliary-space envelope for complete word emission.
theorem
Complexity.RAM.RegisterStore.Machine.rewindWordEncodeTM_prefix_withinAuxSpace
{n : ℕ}
(idx : Fin n)
(value headBound inputLength initialSpace time : ℕ)
(start current : Complexity.Cfg n (rewindWordEncodeTM idx).Q)
(hinitial : start.WithinAuxSpace inputLength initialSpace)
(hreach : (rewindWordEncodeTM idx).reachesIn time start current)
(htime : time ≤ rewindWordEncodeTime value headBound)
:
current.WithinAuxSpace inputLength (initialSpace + rewindWordEncodeTime value headBound)
Coarse all-prefix envelope for rewind followed by word emission.