Rejecting gate-stream execution

This file lifts the failed one-gate bridge to every rejecting counted gate stream. It reuses the successful loop's frontier and counter invariants and the same named budget, while preserving a well-formed counter remainder and recording the machine's zero verdict.

theorem Complexity.CircuitCode.Machine.Internal.gateLoop_run_none (remaining maxWireLength : ℕ) (sawGate : Bool) (last : Option Bool) {codeBits wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hstream : gateStream? remaining codeBits wireBits last = none) (hsaw : sawGate = last.isSome) (hposition : position = if sawGate = true then wireBits.length else 0) (hcode : code.HasBinarySuffix codeBits) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hcount : used + remaining = total) (hmax : wireBits.length + remaining ≤ maxWireLength) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) : ∃ (t : ℕ) (code' : Tape) (wires' : Tape) (counter' : Tape) (output' : Tape) (finalUsed : ℕ), t ≤ gateLoopBudget remaining maxWireLength ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' output') ∧ counter'.HasCounterRemainder finalUsed total ∧ output'.head = 1 ∧ output'.StartInvariant ∧ output'.cells 1 = Γ.zero

Every rejecting pure counted gate stream has a matching machine run to the halted controller. The counter remains a well-formed remainder and output cell one contains zero.