Malformed empty-family execution

This file connects the malformed branches of the pure empty-family stream to the exact controller runs. A false tag on empty input must carry exactly one answer bit: a missing answer rejects in two steps, while trailing data rejects in three.

theorem Complexity.CircuitCode.Machine.Internal.emptyAnswer_step_reject_missing (input code wires counter output : Tape) (hcode : BinaryCursor code [false] 1) (hwires : BinaryCursor wires [] 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg CorePhase.emptyAnswer input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

A false family tag without an answer bit rejects from the empty-answer phase in one step.

theorem Complexity.CircuitCode.Machine.Internal.emptyEnd_step_reject_trailing (answer bit : Bool) (rest : List Bool) (input code wires counter output : Tape) (hcode : BinaryCursor code (false :: answer :: bit :: rest) 2) (hwires : BinaryCursor wires [] 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.step (coreCfg (CorePhase.emptyEnd answer) input code wires counter output) = some (coreCfg CorePhase.done input code wires counter (output.write Γ.zero))

Once the empty-family answer has been read, any further Boolean code bit rejects as trailing data.

theorem Complexity.CircuitCode.Machine.Internal.emptyFamily_run_missingAnswer (input code wires counter output : Tape) (hcode : BinaryCursor code [false] 0) (hwires : BinaryCursor wires [] 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.reachesIn 2 (coreCfg CorePhase.familyTag input code wires counter output) (coreCfg CorePhase.done input (code.move Dir3.right) wires counter (output.write Γ.zero))

A false tag with no answer bit rejects in exactly two controller steps.

theorem Complexity.CircuitCode.Machine.Internal.emptyFamily_run_trailing (answer bit : Bool) (rest : List Bool) (input code wires counter output : Tape) (hcode : BinaryCursor code (false :: answer :: bit :: rest) 0) (hwires : BinaryCursor wires [] 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtput : output.read ≠ Γ.start) : evalFamilyCoreTM.reachesIn 3 (coreCfg CorePhase.familyTag input code wires counter output) (coreCfg CorePhase.done input ((code.move Dir3.right).move Dir3.right) wires counter (output.write Γ.zero))

A false tag with an answer bit followed by more code rejects in exactly three controller steps.

theorem Complexity.CircuitCode.Machine.Internal.emptyFamily_run_none (rest : List Bool) (input code wires counter output : Tape) (hstream : familyStream? (false :: rest) [] = none) (hcode : BinaryCursor code (false :: rest) 0) (hwires : BinaryCursor wires [] 0) (hinput : input.read ≠ Γ.start) (hcounter : counter.read ≠ Γ.start) (houtputHead : output.head = 1) (houtputInv : output.StartInvariant) : ∃ (t : ℕ) (code' : Tape), t ≤ 3 ∧ evalFamilyCoreTM.reachesIn t (coreCfg CorePhase.familyTag input code wires counter output) (coreCfg CorePhase.done input code' wires counter (output.write Γ.zero)) ∧ BinaryCursor code' (false :: rest) (min 2 (false :: rest).length) ∧ (output.write Γ.zero).head = 1 ∧ (output.write Γ.zero).StartInvariant ∧ (output.write Γ.zero).cells 1 = Γ.zero

Every malformed false-tag encoding on empty input reaches a zero verdict within three controller steps. The final code cursor records whether rejection occurred at the missing answer or trailing-data check.