Experimental effect contracts for emitter machines

TM.Experimental.EmitSpec packages the common endpoint effect of a machine that preserves a parked input tape, tracks exact before/after work-tape families, and updates an output accumulator. Its sequencing rule owns the parked phase-boundary proof required by TM.seqTM_hoareTime.

This is deliberately an endpoint-and-time-bound contract. It does not claim an exact running time, all-reachable auxiliary-space safety, or structural transducer safety. In particular, it does not assert that the final output extends the initial output; callers needing append-only behavior must prove that separately.

This contract complements TM.bigSeqTM_hoareTime: that theorem handles an indexed list fold with one uniform per-stage bound, while EmitSpec handles short heterogeneous machine trees and retains each stage's structural bound.

structure Complexity.TM.Experimental.EmitSpec {n : ℕ} (machine : TM n) (input : Tape) (beforeWork afterWork : Fin n → Tape) (beforeOutput afterOutput : List Bool) (time : ℕ) : Prop

A concrete machine contract with exact before/after tape families and an upper time bound. The parked endpoint facts are precisely what sequential composition needs at the next phase boundary.

• inputParked : Parked input

  The fixed input is stable across combinator phase transitions.

• afterWorkParked (i : Fin n) : Parked (afterWork i)

  Every work tape at the endpoint is stable across the next phase transition.

• hoareTime : machine.HoareTime (EmitPred input beforeWork beforeOutput) (EmitPred input afterWork afterOutput) time

  The machine realizes the stated endpoint effect within the supplied time bound.

theorem Complexity.TM.Experimental.EmitSpec.ofHoareTime {n : ℕ} {machine : TM n} {input : Tape} {beforeWork afterWork : Fin n → Tape} {beforeOutput afterOutput : List Bool} {time : ℕ} (inputParked : Parked input) (afterWorkParked : ∀ (i : Fin n), Parked (afterWork i)) (hoareTime : machine.HoareTime (EmitPred input beforeWork beforeOutput) (EmitPred input afterWork afterOutput) time) : EmitSpec machine input beforeWork afterWork beforeOutput afterOutput time

Package one concrete machine's endpoint-and-time contract.

theorem Complexity.TM.Experimental.EmitSpec.seq {n : ℕ} {first second : TM n} {input : Tape} {startWork middleWork endWork : Fin n → Tape} {startOutput middleOutput endOutput : List Bool} {firstTime secondTime : ℕ} (hfirst : EmitSpec first input startWork middleWork startOutput middleOutput firstTime) (hsecond : EmitSpec second input middleWork endWork middleOutput endOutput secondTime) : EmitSpec (first.seqTM second) input startWork endWork startOutput endOutput (firstTime + 1 + secondTime)

Compose two emitter effects. The intermediate parked frame discharges the concrete seqTM transition seam, and the resulting bound includes that real one-step phase change.