# A scan decider for an even number of ones

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-turing-machine-decision-model/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-turing-machine-decision-model-01 · ocme-new142-reader-adoption-20261021



## 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

S01 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, work

Leaf basis: work

Every nonhalt state has one transition for each of three read symbols.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, S01, work

Leaf basis: work

Read1 at cell0, switch to O and move right without changing tape.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, S02, work

Leaf basis: work

Reading0 preserves parity and moves the head to 2.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, S03, work

Leaf basis: work

The second1 switches parity back to E and moves to the first blank.



S05 · impliesBefore

C_3=[E,3,T]

After

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

Conditions: none

Rule: work · Uses: G1, G2, S04, work

Leaf basis: work

E reading blank stays and accepts; this trace has four steps.



S06 · impliesBefore

h\text{ input cells scanned}

After

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

Conditions: none

Rule: work · Uses: G1, G2, S05, work

Leaf basis: work

The empty prefix is E;0 preserves parity and 1 toggles it, proving the invariant by induction on h.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, S06, work

Leaf basis: work

Reading a bit increments h; blank changes rank1 to 0, so every input halts within m+1 steps.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, G2, S07, work

Leaf basis: work

At the first blank the invariant covers the whole word; the two blank transitions give correct answers and total termination.







## 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 rolesR in a state slot may mean reject; R in the move slot means right.

Universal certificateParity 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)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-turing-machine-decision-model-01.json)