Machine emission of raw circuit gates

This module exposes a serializer leaf for append-only tableau generators. A fixed operation-and-negation header is followed by two terminated-unary wire references read from canonical binary work tapes. The input, all work tapes, and the reusable zero scratch are restored literally.

Main results

• emitRawGateTM_hoareTime appends exactly one RawGate.encode word.
• emitRawGateTM_hoareTimeSpace adds an all-prefix auxiliary-space bound.
• emitRawGateTM_isTransducer proves one-way-output safety.

theorem Complexity.CircuitCode.Machine.emitRawGateTM_hoareTime {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (counterIdx input₀Idx input₁Idx : Fin n) (hcounterInput₀ : counterIdx ≠ input₀Idx) (hcounterInput₁ : counterIdx ≠ input₁Idx) (input₀ input₁ : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinput₀ : (work₀ input₀Idx).HasBinaryNat input₀) (hinput₁ : (work₀ input₁Idx).HasBinaryNat input₁) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ input₀Idx → i ≠ input₁Idx → TM.Parked (work₀ i)) : (emitRawGateTM op negated₀ negated₁ counterIdx input₀Idx input₁Idx).HoareTime (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ work₀ (ys ++ { op := op, input₀ := input₀, input₁ := input₁, negated₀ := negated₀, negated₁ := negated₁ }.encode)) (emitRawGateTime input₀ input₁)

Emit one complete raw-gate code from two preserved binary references, restoring the zero scratch and complete external frame.

theorem Complexity.CircuitCode.Machine.emitRawGateTM_hoareTimeSpace {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (counterIdx input₀Idx input₁Idx : Fin n) (hcounterInput₀ : counterIdx ≠ input₀Idx) (hcounterInput₁ : counterIdx ≠ input₁Idx) (input₀ input₁ inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinput₀ : (work₀ input₀Idx).HasBinaryNat input₀) (hinput₁ : (work₀ input₁Idx).HasBinaryNat input₁) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ input₀Idx → i ≠ input₁Idx → TM.Parked (work₀ i)) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (emitRawGateTM op negated₀ negated₁ counterIdx input₀Idx input₁Idx).HoareTimeSpace (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ work₀ (ys ++ { op := op, input₀ := input₀, input₁ := input₁, negated₀ := negated₀, negated₁ := negated₁ }.encode)) (emitRawGateTime input₀ input₁) inputLength (emitRawGateSpace initialSpace input₀ input₁)

Time-and-space form of emitRawGateTM_hoareTime.

theorem Complexity.CircuitCode.Machine.emitRawGateTM_isTransducer {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (counterIdx input₀Idx input₁Idx : Fin n) : (emitRawGateTM op negated₀ negated₁ counterIdx input₀Idx input₁Idx).IsTransducer

Raw-gate emission never moves its output head left.