Rejecting gate attempts

This file proves the rejecting half of the controller-ordered one-gate bridge: truncated headers, unterminated unary references, and decoded references outside the current wire memo. Every path first consumes exactly one gate-count mark and then halts with an explicit zero write.

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

A missing operation bit rejects from the gate-operation phase.

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

A missing first-negation bit rejects from the corresponding header phase.

theorem Complexity.CircuitCode.Machine.Internal.gateNeg1_step_reject_end (op negated0 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.read ≠ Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.gateNeg1 op negated0) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

A missing second-negation bit rejects from the final header phase.

theorem Complexity.CircuitCode.Machine.Internal.ref0_step_reject_code_end (op negated0 negated1 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.read ≠ Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Running out of serialized code during the first unary reference rejects.

theorem Complexity.CircuitCode.Machine.Internal.ref0_step_reject_wire_frontier (op negated0 negated1 bit : Bool) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (bit :: rest)) (hwires : BinaryCursor wires wireBits wireBits.length) (hcounter : counter.read ≠ Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Reaching the memo frontier before completing the first reference rejects.

theorem Complexity.CircuitCode.Machine.Internal.ref1_step_reject_code_end (op negated1 value0 : Bool) {wireBits : List Bool} {position : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.read ≠ Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Running out of serialized code during the second unary reference rejects.

theorem Complexity.CircuitCode.Machine.Internal.ref1_step_reject_wire_frontier (op negated1 value0 bit : Bool) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (bit :: rest)) (hwires : BinaryCursor wires wireBits wireBits.length) (hcounter : counter.read ≠ Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Reaching the memo frontier before completing the second reference rejects.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_reject_header0 (sawGate : Bool) {wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.reachesIn 2 (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input code wires (counter.writeAndMove Γ.blank Dir3.right) (output.write Γ.zero)) ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

An attempt with no header bits consumes its counter mark and rejects in exactly two steps.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_reject_header1 (sawGate op : Bool) {wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix [op]) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.reachesIn 3 (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input (code.move Dir3.right) wires (counter.writeAndMove Γ.blank Dir3.right) (output.write Γ.zero)) ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

An attempt with only an operation bit consumes its counter mark and rejects in exactly three steps.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_reject_header2 (sawGate op negated0 : Bool) {wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix [op, negated0]) (hwires : BinaryCursor wires wireBits position) (hcounter : counter.HasCounterRemainder used total) (hremaining : used < total) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.reachesIn 4 (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input ((code.move Dir3.right).move Dir3.right) wires (counter.writeAndMove Γ.blank Dir3.right) (output.write Γ.zero)) ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

An attempt with only the operation and first-negation bits consumes its counter mark and rejects in exactly four steps.

theorem Complexity.CircuitCode.Machine.Internal.ref0_run_reject_oob (op negated0 negated1 : Bool) (reference : ℕ) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (NatCode.encode reference ++ rest)) (hwires : BinaryCursor wires wireBits 0) (hreference : wireBits.length ≤ reference) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn (wireBits.length + 1) (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter (output.write Γ.zero))

A decoded first reference outside the memo rejects in exactly one more step than the memo length.

theorem Complexity.CircuitCode.Machine.Internal.ref1_run_reject_oob (op negated1 value0 : Bool) (reference : ℕ) (rest : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hcode : code.HasBinarySuffix (NatCode.encode reference ++ rest)) (hwires : BinaryCursor wires wireBits 0) (hreference : wireBits.length ≤ reference) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn (wireBits.length + 1) (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter (output.write Γ.zero))

A decoded second reference outside the memo rejects in exactly one more step than the memo length.

theorem Complexity.CircuitCode.Machine.Internal.ref0_run_reject_unterminated (op negated0 negated1 : Bool) (referenceBits : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hdecode : NatCode.decodePrefix? referenceBits = none) (hcode : code.HasBinarySuffix referenceBits) (hwires : BinaryCursor wires wireBits 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (t : ℕ) (code' : Tape) (wires' : Tape), t ≤ wireBits.length + 1 ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.ref0 op negated0 negated1) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter (output.write Γ.zero))

Failure of the pure first-reference decoder has a matching bounded machine rejection.

theorem Complexity.CircuitCode.Machine.Internal.ref1_run_reject_unterminated (op negated1 value0 : Bool) (referenceBits : List Bool) {wireBits : List Bool} (input code wires counter output : Tape) (hdecode : NatCode.decodePrefix? referenceBits = none) (hcode : code.HasBinarySuffix referenceBits) (hwires : BinaryCursor wires wireBits 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (t : ℕ) (code' : Tape) (wires' : Tape), t ≤ wireBits.length + 1 ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.ref1 op negated1 value0) input code wires counter output) (coreCfg CorePhase.done input code' wires' counter (output.write Γ.zero))

Failure of the pure second-reference decoder has a matching bounded machine rejection.

theorem Complexity.CircuitCode.Machine.Internal.gateAttempt_run_none (sawGate : Bool) {codeBits wireBits : List Bool} {position used total : ℕ} (input code wires counter output : Tape) (hstep : gateStep? codeBits wireBits = none) (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 + 8 ∧ evalFamilyCoreTM.reachesIn t (coreCfg (CorePhase.gateCheck sawGate) input code wires counter output) (coreCfg CorePhase.done input code' wires' (counter.writeAndMove Γ.blank Dir3.right) (output.write Γ.zero)) ∧ (counter.writeAndMove Γ.blank Dir3.right).HasCounterRemainder (used + 1) total

Every failed pure gate step has a matching machine rejection. The machine consumes exactly one counter mark, writes zero, and halts within the common linear gate-attempt budget.