二元字串偶數1的scan decider

目標與範圍

完整machine、trace、ranking與全input正確性。

single-tape deterministic scan schema，不由一條halt trace證total。

已知條件與符號

• work

• G1 — Q={E,O,A,R}，input alphabet{0,1}，tape alphabet{0,1,_}，blank=_，start E，accept A，reject R，head初始0。輸入w長m置cells0≤j<m，其餘blank。
• G2 — 完整非halt轉移：[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沒有outgoing。tuple末位R指right，不是reject state。

• C=[q,h,T] — state、head、sparse tape
• ρ — 全input下降ranking

規則與來源

• mko_definition · cited — machine明示finite states、input alphabet、tape alphabet、blank、start、accept、reject及deterministic transition [state,read,next,write,move]，tape未列cells皆為blank。configuration固定[state,head,sparse nonblank tape]。exact step與finite trace只證指定input。全域decider certificate須提供對所有input成立且每步嚴格下降的ranking或明示step bound，並同時有answer correctness。recognizer可在nonmember上loop；bounded simulation failure不證rejection或nontermination，單一halting trace也不證全域decider。 · mko-turing-machine-decision-model
• work · prerequisite — deterministic TM一步語義、有限word按head順序掃描、prefix parity歸納、非負整數嚴格下降ranking保證termination。

逐步主鏈

\{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}

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, G2, S07, work — empty word m=0在一步accept；bounded timeout不是reject證書。
• S07 · premise_audit · G1, G2, S06, work — 只能在可達scan態0≤h≤m使用此ranking。
• S06 · premise_audit · G1, G2, S05, work — state只記已掃prefix，不偷看未讀suffix。
• S05 · premise_audit · G1, G2, S04, work — 此trace只證101，尚須全input義務。
• S04 · premise_audit · G1, G2, S03, work — 原input長度3，cell3確實blank。
• S03 · premise_audit · G1, G2, S02, work — 0也是nonblank tape symbol，仍保留於sparse table。
• S02 · premise_audit · G1, G2, S01, work — sparse tape未列cells都blank。
• S01 · premise_audit · G1, G2, work — 無缺transition，也無同pair兩個後繼。

錯誤控制與反例

R角色

tuple 的第 1、3 個 state slot 中，R 可表示 reject state；第 5 個 move slot 中的 R 只表示向右。

全稱證書

parity invariant給答案，ranking給termination，兩者都不可漏。

• 一條101 halt trace就證所有input halt。 → reject — 全input termination另由ranking證明。
• m步未halt就可reject。 → reject — 此正確機器需要m+1步讀末blank。
• empty input不在decider範圍。 → reject — 初始即讀blank，由E在一步accept，零個1為偶數。

結論與限制

此機器對所有二元words在m+1步內決定1的個數是否偶數；101於4步accept。

驗證及來源綁定

3 個本稿宣告算術檢查；只支持所列算式。

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）