Signed verdict routing

On an encoded Boolean verifier result, this fixed one-step machine emits the chosen sign once when the result is true. A false result instead produces one accepting and one rejecting branch. Thus unsuccessful witnesses cancel in the integer gap, including when the witness length is zero. Every local view has a nonempty choice list and all branches halt in one instruction.

Main definitions

• Turing.MultiTapeCTM.verdictMachine: the actual one-versus-two native routing machine.

Main results

• Turing.MultiTapeCTM.VerdictMachine.haltsWithin: one native instruction on any input.
• Turing.MultiTapeCTM.VerdictMachine.branchCount_eq: exact counts on encoded Booleans.
• Turing.MultiTapeCTM.VerdictMachine.branchCount_comp: charged, count-preserving routing.

References

Balanced accepting/rejecting cancellation is the standard GapP mechanism [FFK94]. Native occurrence semantics are credited in MultiTape.Counting.

def Turing.MultiTapeCTM.VerdictMachine.halt (sign : Bool) : Action 0 Bool Unit

Emit one Boolean verdict and halt without moving a head.

def Turing.MultiTapeCTM.verdictMachine (sign : Bool) : MultiTapeCTM 0 Bool Unit

True yields one chosen-sign leaf; false (or a blank input) yields a balanced pair.

theorem Turing.MultiTapeCTM.VerdictMachine.nonblocking (sign : Bool) : (verdictMachine sign).Nonblocking

Both the singleton and balanced local choice lists are nonempty.

theorem Turing.MultiTapeCTM.VerdictMachine.haltsWithin (sign : Bool) (input : List Bool) : (verdictMachine sign).HaltsWithin 1 (Cfg.init () input)

Every branch halts in one native instruction, even on inputs outside the Boolean encoding.

theorem Turing.MultiTapeCTM.VerdictMachine.branchCount_eq (sign bit : Bool) (verdict : List Bool → Bool) : (verdictMachine sign).branchCount verdict 1 (Cfg.init () (MultiTapeTM.encBool bit)) = if bit = true then (verdict [sign]).toNat else (verdict [true]).toNat + (verdict [false]).toNat

The exact one-step verdict count: unsuccessful witnesses contribute one of each sign.

theorem Turing.MultiTapeCTM.VerdictMachine.branchCount_comp {k : ℕ} {State : Type} (source : MultiTapeCTM k Bool State) (hnon : source.Nonblocking) (input : List Bool) (fuel : ℕ) (hhalt : source.HaltsWithin fuel (Cfg.init source.initial input)) (hbool : ∀ result ∈ source.runList fuel (Cfg.init source.initial input), ∃ (bit : Bool), result.output = MultiTapeTM.encBool bit) (sign verdict : Bool) : ((verdictMachine sign).comp source true).branchCount (fun (out : List Bool) => (out == [true]) == verdict) (fuel + (fuel + 4 + 1)) (MultiTapeMachine.initialConfig ((verdictMachine sign).comp source true) input).tapes = if sign = verdict then (source.runList fuel (Cfg.init source.initial input)).length else source.rejectCount fuel (Cfg.init source.initial input)

Buffered routing preserves the chosen-sign branch for every witness and cancels false ones. The source must really output encoded Booleans; arbitrary words beginning in true are not accepted as a substitute. The buffer and its preparation are included in the displayed clock.