Rejecting positive-family setup

This file proves the rejecting execution paths before the positive-family gate loop begins. An unterminated unary gate count is scanned to its first trailing blank while the counter prefix is built, then rejected explicitly. The frontier-level wrappers also cover a positive tag paired with the empty input.

def Complexity.CircuitCode.Machine.Internal.positiveCountRejectTime (countLength inputLength : ℕ) : ℕ

Time for rejecting an unterminated unary count from the staging frontiers. The arguments are the count-field length and the primary-input length.

Equations

• Complexity.CircuitCode.Machine.Internal.positiveCountRejectTime countLength inputLength = 2 * countLength + inputLength + 7

theorem Complexity.CircuitCode.Machine.Internal.count_step_reject_end (used : ℕ) (input code wires counter output : Tape) (hcode : code.HasBinarySuffix []) (hcounter : counter.HasUnaryPrefix used) (hinput : input.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg CorePhase.count input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Reaching the end of an unterminated gate count rejects from the count phase without changing any work tape.

theorem Complexity.CircuitCode.Machine.Internal.count_run_reject_unterminated (countBits : List Bool) (used : ℕ) (input code wires counter output : Tape) (hdecode : NatCode.decodePrefix? countBits = none) (hcode : code.HasBinarySuffix countBits) (hcounter : counter.HasUnaryPrefix used) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (hwires : wires.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (counter' : Tape), evalFamilyCoreTM.reachesIn (countBits.length + 1) (coreCfg CorePhase.count input code wires counter output) (coreCfg CorePhase.done input code' wires counter' (output.write Γ.zero)) ∧ code'.HasBinarySuffix [] ∧ counter'.HasUnaryPrefix (used + countBits.length) ∧ counter'.cells 0 = Γ.start

Failure of the unary count decoder has a matching exact count-phase machine rejection.

theorem Complexity.CircuitCode.Machine.Internal.positiveHeader_run_reject_unterminated (countBits inputRest : List Bool) (input code wires counter output : Tape) (bit : Bool) (hdecode : NatCode.decodePrefix? countBits = none) (hcode : BinaryCursor code (true :: countBits) 0) (hwires : BinaryCursor wires (bit :: inputRest) 0) (hcounter : counter.HasUnaryPrefix 0) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : ∃ (code' : Tape) (counter' : Tape), evalFamilyCoreTM.reachesIn (countBits.length + 2) (coreCfg CorePhase.familyTag input code wires counter output) (coreCfg CorePhase.done input code' wires counter' (output.write Γ.zero)) ∧ code'.HasBinarySuffix [] ∧ counter'.HasUnaryPrefix countBits.length ∧ counter'.cells 0 = Γ.start

A positive family whose unary gate count is unterminated rejects from the family-tag phase in exactly countBits.length + 2 steps.

theorem Complexity.CircuitCode.Machine.Internal.positiveCount_fromFrontiers_run_reject (countBits inputRest : List Bool) (input code wires counter output : Tape) (bit : Bool) (hdecode : NatCode.decodePrefix? countBits = none) (hcode : BinaryCursor code (true :: countBits) (true :: countBits).length) (hwires : BinaryCursor wires (bit :: inputRest) (bit :: inputRest).length) (hcounter : counter.HasUnaryPrefix 0) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) : ∃ (code' : Tape) (wires' : Tape) (counter' : Tape), evalFamilyCoreTM.reachesIn (positiveCountRejectTime countBits.length (bit :: inputRest).length) (coreCfg CorePhase.rewindCode input code wires counter output) (coreCfg CorePhase.done input code' wires' counter' (output.write Γ.zero)) ∧ code'.HasBinarySuffix [] ∧ BinaryCursor wires' (bit :: inputRest) 0 ∧ counter'.HasUnaryPrefix countBits.length ∧ counter'.cells 0 = Γ.start ∧ (output.write Γ.zero).head = 1 ∧ (output.write Γ.zero).StartInvariant ∧ (output.write Γ.zero).cells 1 = Γ.zero

From the staging frontiers, an unterminated positive-family gate count reaches an explicit zero verdict in the named exact time.

theorem Complexity.CircuitCode.Machine.Internal.positiveEmptyInput_fromFrontiers_run_reject (rest : List Bool) (input code wires counter output : Tape) (hcode : BinaryCursor code (true :: rest) (true :: rest).length) (hwires : BinaryCursor wires [] 0) (hcounter : counter.HasUnaryPrefix 0) (hcounter0 : counter.cells 0 = Γ.start) (hinput : input.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) : ∃ (code' : Tape) (wires' : Tape), evalFamilyCoreTM.reachesIn ((true :: rest).length + 5) (coreCfg CorePhase.rewindCode input code wires counter output) (coreCfg CorePhase.done input code' wires' counter (output.write Γ.zero)) ∧ BinaryCursor code' (true :: rest) 0 ∧ BinaryCursor wires' [] 0 ∧ counter.HasUnaryPrefix 0 ∧ counter.cells 0 = Γ.start ∧ (output.write Γ.zero).head = 1 ∧ (output.write Γ.zero).StartInvariant ∧ (output.write Γ.zero).cells 1 = Γ.zero

A positive-family tag paired with the empty input rejects from the staging frontiers before attempting to parse a gate count.