完整有限reduction與方向保持

目標與範圍

逐x核iff、組合及decider transfer。

有限完整truth tables；不宣稱無限domain算法。

已知條件與符號

• work

• G1 — source S={0,1,2,3}，A={1,3}；target T={a,b,c}，B={b}；f=(a,b,c,b)。U={u,v}，C={v}；g(a)=u、g(b)=v、g(c)=u。

• f,g,h — total reductions及composition
• D_B — target decider

規則與來源

• mko_definition · cited — 有限題族明示source carrier、target carrier、decision predicates與完整total mapping table，逐x雙向驗x∈A iff f(x)∈B；只驗yes instances不足。composition須保留方向：A≤mB且B≤mC推出A≤mC。若A≤mB且B decidable，先算f再跑B decider可得A decider；反向transfer不成立。partial map、倒轉方向與Turing reduction混同均須拒絕。有限mapping table只證指定finite domain；無限domain仍需完整可計算算法及termination certificate。 · mko-many-one-reduction
• work · prerequisite — many-one reduction是total computable map保持x∈A iff f(x)∈B；有限完整table可計算且halt；函數合成與iff傳遞。

逐步主鏈

f=(a,b,c,b),\quad g=(u,v,u)

f:S\to T,\quad g:T\to U\text{ are total}

x=0,2

x\notin A,\quad f(0)=a\notin B,\quad f(2)=c\notin B

x=1,3

x\in A,\quad f(1)=f(3)=b\in B

\forall x\in S:\ x\in A\iff f(x)\in B

A\le_m B\quad\text{on the declared carriers}

a,c\notin B,\quad b\in B

g(a)=g(c)=u\notin C,\quad g(b)=v\in C

h=g\circ f

h=(u,v,u,v),\quad x\in A\iff h(x)\in C

D_B(a)=0,D_B(b)=1,D_B(c)=0

D_A(x)=D_B(f(x))=(0,1,0,1)_x

A\le_mB\text{ and }B\text{ decidable}

A\text{ decidable; no reverse implication supplied}

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S07, work — 有限carriers本來皆可查表，不能用它們偽造無限不可決反例。
• S07 · premise_audit · G1, S06, work — decider transfer是從target B到source A。
• S06 · premise_audit · G1, S05, work — 不能用f∘g，型別和方向都不匹配。
• S05 · premise_audit · G1, S04, work — g定義域是整個T，而不只B。
• S04 · premise_audit · G1, S03, work — 這個有限結論不延伸未列的整數。
• S03 · premise_audit · G1, S02, work — x=1、3不同但可同像，reduction不要求injective。
• S02 · premise_audit · G1, S01, work — 只核yes會漏掉這兩個責任。
• S01 · premise_audit · G1, work — partial table不能先稱many-one reduction。

錯誤控制與反例

no cases

0、2的membership否定也逐一核。

transfer方向

沿f計算方向走，使用target decider來解source。

• 只要f在1、3送b即可，0也可送b。 → reject — 0非A但b屬B會破壞iff反向。
• f必須injective。 → reject — 1與3同像b仍完整保持iff。
• composition應是f∘g。 → reject — g輸出U但f輸入S，不合型別；正確g∘f。

結論與限制

f證A≤mB，g證B≤mC，g∘f證A≤mC；先f後DB決定A。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 1a1c76bdcb2cbe175d47046cb14542bfd1c9bd765be098a093d56ec92f7bd817
• original source SHA-256: 64cb4efb6449a3a14fcb1d7a0a1135fd167442065877da4e143010419d64892f
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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