One streaming raw-gate step -- proof internals

These proofs compose raw-gate emission with canonical binary successor. The adapter for the successor phase keeps the append-only output accumulator as a ghost while converting successor's full-frame result into an exact work-tape update.

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_hoareTime_internal {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₁)

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_hoareTimeSpace_internal {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₁)

theorem Complexity.CircuitCode.Machine.emitRawGateStepTM_isTransducer_internal {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