A scan decider for an even number of ones

Goal and scope

Give the complete machine, trace, ranking and all-input correctness.

A deterministic single-tape scan schema, not totality inferred from one halting trace.

Givens and symbols

• work

• G1 — Q={E,O,A,R}, input alphabet{0,1}, tape alphabet{0,1,_}, blank_, start E, accept A, reject R, initial head0. Input w of length m occupies cells0≤j<m; all other cells are blank.
• G2 — The complete nonhalt transitions are[E,0,E,0,R],[E,1,O,1,R],[O,0,O,0,R],[O,1,E,1,R],[E,_,A,_,S],[O,_,R,_,S]; halt states A,R have no outgoing transitions. Final-position R means right, not reject state.

• C=[q,h,T] — state, head and sparse tape
• ρ — all-input decreasing ranking

Rules and sources

• mko_definition · cited — Specify finite states, input/tape alphabets, blank, start, accept, reject and deterministic transitions [state,read,next,write,move]. Unlisted tape cells are blank, and configurations are [state,head,sparse nonblank tape]. Exact steps and finite traces concern their supplied input only. A global decider certificate needs an all-input strictly decreasing ranking or explicit step bound and answer correctness. A recognizer may loop on nonmembers. Bounded simulation failure proves neither rejection nor nontermination, and one halting trace does not certify a global decider. · mko-turing-machine-decision-model
• work · prerequisite — Deterministic TM step semantics, scanning a finite word in head order, prefix-parity induction, and termination from a strictly decreasing nonnegative-integer ranking.

Main derivation

\{E,O\}\times\{0,1,\_\}

6\text{ deterministic transitions; A,R terminal}

w=101,\quad C_0=[E,0,\{0:1,1:0,2:1\}]

C_1=[O,1,\{0:1,1:0,2:1\}]

C_1=[O,1,\{0:1,1:0,2:1\}]

C_2=[O,2,\{0:1,1:0,2:1\}]

C_2=[O,2,\{0:1,1:0,2:1\}]

C_3=[E,3,\{0:1,1:0,2:1\}]

C_3=[E,3,T]

C_4=[A,3,T]\quad\text{accept}

h\text{ input cells scanned}

q=E\iff\#\{j<h:w_j=1\}\text{ even};\quad q=O\iff\text{odd}

\rho=m-h+1\text{ in scan states},\quad\rho=0\text{ in A,R}

\rho\in\mathbb N_0,\quad\rho\text{ strictly decreases at each step}

h=m,\quad q=E\text{ iff total ones even}

\text{accept iff }w\text{ has even ones; reject otherwise}

Substeps and lemmas

No substeps in this guide.

Reverse audits

• S08 · premise_audit · G1, G2, S07, work — The empty word accepts in one step; a bounded timeout is not a rejection certificate.
• S07 · premise_audit · G1, G2, S06, work — Use this ranking on reachable scan states0≤h≤m.
• S06 · premise_audit · G1, G2, S05, work — The state tracks the scanned prefix only, not unread suffix.
• S05 · premise_audit · G1, G2, S04, work — This trace proves only 101; all-input obligations remain.
• S04 · premise_audit · G1, G2, S03, work — The input length is 3, so cell3 is blank.
• S03 · premise_audit · G1, G2, S02, work — Zero is a nonblank tape symbol and remains in the sparse table.
• S02 · premise_audit · G1, G2, S01, work — All unlisted sparse-tape cells are blank.
• S01 · premise_audit · G1, G2, work — No transition pair is missing or multivalued.

Error controls and negative controls

R roles

R in a state slot may mean reject; R in the move slot means right.

Universal certificate

Parity invariance gives the answer and ranking termination; retain both.

• One101 halting trace proves halting on every input. → reject — All-input termination requires the separate ranking argument.
• Failure to halt in m steps proves rejection. → reject — This correct machine needs m+1 steps to read the final blank.
• Empty input is outside the decider's domain. → reject — Initially reading blank in E accepts in one step; zero ones is even.

Result and limitations

The machine decides even-one parity for every binary word within m+1 steps;101 accepts in four steps.

Verification and source binding

3 declared checks for this guide; only the listed expressions are covered.

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 77d53abdd344aeaf85e19bd50d683bd23ec41515448ac822ac05edcccf7c7a30
• original source SHA-256: 6afbbbf8fb1498115567f484c8776ccf5f2728c23bb439f5feb63e33c9327cd6
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

Same-source full JSON (formulas, ASTs, controls and revision log)