# A complete finite reduction with preserved direction

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-many-one-reduction/)

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-many-one-reduction-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Check every x equivalence, composition and decider transfer.

Complete finite truth tables, not an infinite-domain algorithm claim.





## Givens and symbols


- 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 and composition
- D_B — target decider





## Rules and sources


- mko_definition · cited — Finite families declare complete source and target carriers, both decision predicates and an aligned mapping table. Qualify totality, then check both directions of membership equivalence for every x; yes-only checks are insufficient. Composition preserves direction: A≤mB and B≤mC give A≤mC. If A≤mB and B is decidable, compute f then run the B decider to decide A; the reverse implication is not supplied. Partial maps, reversed transfer and conflation with Turing reduction must be rejected. A finite table certifies only its declared finite domain; an infinite domain still needs a complete computable algorithm and termination argument. · mko-many-one-reduction
- work · prerequisite — A many-one reduction is a total computable map preserving x∈A iff f(x)∈B; complete finite tables are computable and halt; function composition and iff transitivity.





## Main derivation

S01 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Every source entry has a legal target image, and g is fully defined too.



S02 · impliesBefore

x=0,2

After

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

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Both no-instances preserve no-membership.



S03 · impliesBefore

x=1,3

After

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

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Both yes-instances preserve yes-membership.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

All four source elements satisfy both directions of membership equivalence.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

All three target elements establish B≤mC.



S06 · impliesBefore

h=g\circ f

After

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

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Compose the tables in direction A to C, retaining all four entries.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Compute f then consult the B decider, producing the complete A truth table with finite termination.



S08 · impliesBefore

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

After

A\text{ decidable; no reverse implication supplied}

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Algorithm composition explains the valid transfer; for general problems A decidable does not imply B decidable.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — Finite carriers are decidable by lookup; they must not be misused as infinite undecidability counterexamples.
- S07 · premise_audit · G1, S06, work — Decider transfer runs from target B to source A.
- S06 · premise_audit · G1, S05, work — f composed after g would mismatch both type and direction.
- S05 · premise_audit · G1, S04, work — The domain of g is all T, not only B.
- S04 · premise_audit · G1, S03, work — This finite conclusion does not extend to unlisted integers.
- S03 · premise_audit · G1, S02, work — Distinct1,3 may share an image; reductions need not be injective.
- S02 · premise_audit · G1, S01, work — Yes-only checking would omit these two obligations.
- S01 · premise_audit · G1, work — A partial table cannot be qualified as a many-one reduction.





## Error controls and negative controls

No casesAudit nonmembership separately at 0,2.

Transfer directionFollow f forward, using the target decider to decide the source.


- Checking1,3 map to b suffices;0 may also map to b. → reject — 0 is outside A while b lies in B, violating the reverse implication.
- f must be injective. → reject — 1 and 3 share image b while preserving every iff.
- Composition should be f after g. → reject — g outputs U while f expects S; the well-typed composition is g after f.





## Result and limitations

f gives A≤mB, g gives B≤mC, and g∘f gives A≤mC; applying f then DB decides A.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 1a1c76bdcb2cbe175d47046cb14542bfd1c9bd765be098a093d56ec92f7bd817
- original source SHA-256: 64cb4efb6449a3a14fcb1d7a0a1135fd167442065877da4e143010419d64892f
- 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-many-one-reduction-01.json)