One streaming raw-gate step

This module exposes the atomic operation of an append-only raw-circuit serializer: emit one encoded gate from preserved binary references and advance the binary first-unused-wire counter by one. The emitter's private counter is restored to zero and every other tape is preserved literally.

Main results

• emitRawGateStepTM_hoareTime gives exact output and wire-counter effects.
• emitRawGateStepTM_hoareTimeSpace adds an all-prefix width bound.
• emitRawGateStepTM_isTransducer proves append-only-output safety.

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_hoareTime {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) (hdistinct : RawGateStepDistinct emitCounterIdx availableIdx input₀Idx input₁Idx) (available input₀ input₁ : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hemitCounter : (work₀ emitCounterIdx).HasBinaryNat 0) (havailable : (work₀ availableIdx).HasBinaryNat available) (hinput₀ : (work₀ input₀Idx).HasBinaryNat input₀) (hinput₁ : (work₀ input₁Idx).HasBinaryNat input₁) (hother : ∀ (i : Fin n), i ≠ emitCounterIdx → i ≠ availableIdx → i ≠ input₀Idx → i ≠ input₁Idx → TM.Parked (work₀ i)) : (emitRawGateStepTM op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).HoareTime (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ (Function.update work₀ availableIdx ((Tape.init (List.map Γ.ofBool (available + 1).bits)).move Dir3.right)) (ys ++ { op := op, input₀ := input₀, input₁ := input₁, negated₀ := negated₀, negated₁ := negated₁ }.encode)) (emitRawGateStepTime available input₀ input₁)

Emit one encoded gate and advance availableIdx; all other tapes, including both references and the zero emitter counter, are restored literally.

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_hoareTimeSpace {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) (hdistinct : RawGateStepDistinct emitCounterIdx availableIdx input₀Idx input₁Idx) (available input₀ input₁ inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hemitCounter : (work₀ emitCounterIdx).HasBinaryNat 0) (havailable : (work₀ availableIdx).HasBinaryNat available) (hinput₀ : (work₀ input₀Idx).HasBinaryNat input₀) (hinput₁ : (work₀ input₁Idx).HasBinaryNat input₁) (hother : ∀ (i : Fin n), i ≠ emitCounterIdx → i ≠ availableIdx → i ≠ input₀Idx → i ≠ input₁Idx → TM.Parked (work₀ i)) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (emitRawGateStepTM op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).HoareTimeSpace (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ (Function.update work₀ availableIdx ((Tape.init (List.map Γ.ofBool (available + 1).bits)).move Dir3.right)) (ys ++ { op := op, input₀ := input₀, input₁ := input₁, negated₀ := negated₀, negated₁ := negated₁ }.encode)) (emitRawGateStepTime available input₀ input₁) inputLength (emitRawGateStepSpace initialSpace available input₀ input₁)

Time-and-space form of one streaming gate step.

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_isTransducer {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) : (emitRawGateStepTM op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).IsTransducer

A streaming gate step never moves the output head left.