Machine emission of raw circuit gates — proof internals

This module composes the fixed header emitter with two terminated-unary emitters. Both dynamic reference tapes and the reusable zero scratch are restored literally at the endpoint.

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

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

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