# A universal code for three natural-number tracks

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-at-most-countable-set/)

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-at-most-countable-set-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

N0 times {0,1,2} injects into N0 by c(n,j)=3n+j and is at most countable.

Finite-set certificates and a universal integer affine code; no uncountability conclusion.





## Givens and symbols


- calc


- G1 — N0={n in Z:n≥0}; X=N0 times {0,1,2}; c(n,j)=3n+j.


- N_0 — natural numbers including zero
- c — integer affine code
- j — three-track index





## Rules and sources


- calc · prerequisite — Assume integer quotient/remainder arithmetic, nonnegative integers and injectivity; at most countable means admitting an injection into N0.
- mko_definition · cited — This slice uses complete finite-set certificates or universal injectivity certificates from integer affine encodings. A failed encoding refutes that particular witness, not countability of the set. · mko-at-most-countable-set





## Main derivation

S01 · impliesBefore

(n,j)\in X

After

n\ge0,\quad j\in\{0,1,2\}\Rightarrow3n+j\in N_0

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The code is an integer and nonnegative, so its codomain is valid.



S02 · impliesBefore

c(n,j)=c(m,k)

After

3(n-m)=k-j

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

For arbitrary inputs with equal codes, rearranging gives a multiple of 3 equal to a small difference.



S03 · impliesBefore

j,k\in\{0,1,2\}

After

-2\le k-j\le2,\quad3\mid(k-j)\Rightarrow k-j=0

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

Zero is the only multiple of 3 in that range, forcing j=k.



S04 · impliesBefore

3(n-m)=0,\quad j=k

After

n=m,\quad(n,j)=(m,k)

Conditions: none

Rule: calc · Uses: G1, S02, S03

Leaf basis: calc

Since 3 is nonzero in the integers, cancellation gives n=m, so c is universally injective.



S05 · impliesBefore

c:X\hookrightarrow N_0

After

X\text{ is at most countable}

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

The universal injection directly meets the definition of at most countable, without finite testing.



S06 · impliesBefore

r\in N_0

After

r=3q+j,\quad q\in N_0,\quad j\in\{0,1,2\}

Conditions: none

Rule: calc · Uses: G1, S04

Leaf basis: calc

Nonnegative division with remainder also gives a preimage for every r, so this particular c is bijective.



S07 · impliesBefore

Y=\{a,b,c\},\quad e(a)=0,e(b)=1,e(c)=2

After

e:Y\hookrightarrow N_0,\quad |Y|=3

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The full three-element map has distinct images, certifying a finite set as at most countable.



S08 · impliesBefore

b(n,j)=3n

After

b(0,0)=b(0,1)=0,\quad c(0,0)=0\ne1=c(0,1)

Conditions: none

Rule: calc · Uses: G1, S05

Leaf basis: calc

Another code b collides, refuting only b; the proven c still certifies the same X.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S05 — One bad code cannot imply uncountability when a valid full code already exists.
- S07 · premise_audit · G1 — Y is at most countable but not countably infinite, distinguishing the terms.
- S06 · premise_audit · G1, S04 — This extra onto certificate permits countable infinitude here; the injection alone established only at most countable.
- S05 · premise_audit · G1, S01, S04 — Surjectivity is not needed for this conclusion; finite sets are at most countable too.
- S04 · premise_audit · G1, S02, S03 — Equal images force equality of both coordinates, not just the first.
- S03 · premise_audit · G1, S02 — Both endpoints -2 and 2 are included; neither 3 nor -3 occurs.
- S02 · premise_audit · G1, S01 — No n or m is sampled; this is a universal collision analysis.
- S01 · premise_audit · G1 — Allowing negative n could leave N0, so the parameter domain matters.





## Error controls and negative controls

Parameter domainThe proof fixes n≥0 and 0≤j≤2; allowing j=3 collides with the next track.

Witness versus setFailure refutes that function, not countability of the set.


- b(n,j)=3n is injective. → reject — (0,0) and (0,1) both map to 0.
- Failure of b means X is uncountable. → reject — c(n,j)=3n+j is already universally injective.
- Finite Y is at most countable, hence countably infinite. → reject — Y has three elements and cannot biject with infinite N0.





## Result and limitations

N0 times {0,1,2} injects into N0 by c(n,j)=3n+j and is at most countable.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bcd07b59b5e83e1216ba1fb8c780353d2a97cf3c8fd58ec701dee7656e7f25d5
- original source SHA-256: bcd07b59b5e83e1216ba1fb8c780353d2a97cf3c8fd58ec701dee7656e7f25d5
- 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-at-most-countable-set-01.json)