Pure-to-machine gate-attempt bridge

This file packages the exact canonical gate execution theorem behind the controller-ordered gateStep? interface. The pure result intentionally omits the first reference, so the machine runtime is existential but carries a uniform linear bound in the current wire-memo length.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_run_some (sawGate : Bool) {codeBits wireBits : List Bool} {step : GateStepResult} {position used total : ℕ} (input code wires counter output : Tape) (hstep : gateStep? codeBits wireBits = some step) (hcode : code.HasBinarySuffix codeBits) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (t : ℕ) (code' : Tape) (wires' : Tape), t ≤ 4 * wireBits.length + 9 ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg (CorePhase.gateCheck true) input code' wires' (counter.writeAndMove Γ.blank Dir3.right) (output.write (Γ.ofBool step.value))) ∧ code'.HasBinarySuffix step.rest ∧ BinaryCursor wires' step.wires step.wires.length ∧ step.wires.length = wireBits.length + 1 ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

Every successful pure gate step has a matching machine execution. The machine consumes one counter mark, appends exactly step.value, exposes step.rest, and finishes within 4 * wireBits.length + 9 steps.

theorem Complexity.CircuitCode.Machine.Internal.gateCheck_step_done {wireBits : List Bool} {position total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder total total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateCheck true) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter output)

With every counter mark consumed, a nonempty stream that has produced a gate and consumed all code halts successfully in one step.

theorem Complexity.CircuitCode.Machine.Internal.gateCheck_step_reject_no_gate {codeBits wireBits : List Bool} {position total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix codeBits) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder total total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateCheck false) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

An exhausted counter with no previously evaluated gate rejects in one step, even when the code stream is empty.

theorem Complexity.CircuitCode.Machine.Internal.gateCheck_step_reject_trailing (bit : Bool) (rest : List Bool) {wireBits : List Bool} {position total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (bit :: rest)) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder total total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateCheck true) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

After at least one gate, exhausting the declared counter while serialized code remains rejects the trailing data in one step.