# Cardinality certificates from full maps

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

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-cardinality-comparison-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

There is an injection A to B with |A|=2<3=|B|; a reverse surjection is not injective.

Explicit finite sets and full maps only; no infinite-choice claim.





## Givens and symbols


- calc


- G1 — A={a,b}, B={1,2,3}; f(a)=1,f(b)=2; g(1)=a,g(2)=b,g(3)=a.


- f,g — maps with opposite directions
- A,B,C — complete finite sets





## Rules and sources


- calc · prerequisite — Assume finite counting and the definitions of injection and surjection.
- mko_definition · cited — This slice is limited to complete finite sets. An injection A→B certifies |A|≤|B|, a surjection certifies |A|≥|B|, and a bijection certifies equality. If |A|>|B| there is no injection. Reverse comparison from a surjection for infinite sets requires additional choice or section obligations and is outside this slice. · mko-cardinality-comparison





## Main derivation

S01 · impliesBefore

A=\{a,b\},\ B=\{1,2,3\}

After

|A|=2,\quad |B|=3

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Both carriers are complete with distinct entries, so their counts contain no duplicates.



S02 · impliesBefore

f:A\to B

After

\operatorname{graph}(f)=\{(a,1),(b,2)\}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Each source element has exactly one image in B, so f is total.



S03 · impliesBefore

f(a)=1,\ f(b)=2

After

f(a)\ne f(b)\Rightarrow f\text{ injective}

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

A has only two elements, and the only distinct pair has distinct images, exhausting collision checks.



S04 · impliesBefore

f(A)=\{1,2\}

After

3\notin f(A),\quad f\text{ not surjective},\quad 2\le3

Conditions: none

Rule: mko_definition · Uses: G1, S01, S03

Leaf basis: mko_definition

Missing 3 refutes surjectivity, while the two distinct images certify |A|≤|B|.



S05 · impliesBefore

g:B\to A

After

g^{-1}(\{a\})=\{1,3\},\quad g^{-1}(\{b\})=\{2\}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The full reverse map gives two nonempty fibers accounting for all of B.



S06 · impliesBefore

g(B)=A,\quad g(1)=g(3)

After

g\text{ surjective but not injective};\quad3\ge2

Conditions: none

Rule: mko_definition · Uses: G1, S05

Leaf basis: mko_definition

Both a and b have preimages, so g is onto; distinct 1 and 3 have the same image, so g is not injective.



S07 · impliesBefore

h:B\to A\text{ assumed injective}

After

h(1),h(2),h(3)\text{ distinct in a two-element set: impossible}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

An injection would require three distinct elements in explicitly two-element A, which is impossible.



S08 · impliesBefore

C=\{u,v\},\quad b(a)=u,\ b(b)=v

After

b:A\to C\text{ bijective};\quad |A|=|C|=2

Conditions: none

Rule: mko_definition · Uses: G1, S01

Leaf basis: mko_definition

A separate full map is both injective and onto u,v, certifying equality of cardinalities.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S01 — The equality has an actual bijection witness and does not mislabel the original f as onto.
- S07 · premise_audit · G1, S01 — This excludes every h, not merely g, using the complete carrier sizes.
- S06 · premise_audit · G1, S05 — Audit onto and one-to-one separately; the reverse surjection gives the finite reverse inequality only.
- S05 · premise_audit · G1 — A fiber is a source subset; inputs 1 and 3 cannot be counted as one element.
- S04 · premise_audit · G1, S01, S03 — Do not upgrade injection to bijection; the missing image is certified by the full source table.
- S03 · premise_audit · G1, S02 — 1 and 2 are distinct in B; injectivity does not require hitting 3.
- S02 · premise_audit · G1, S01 — Checking filled entries alone would miss an omitted source element.
- S01 · premise_audit · G1 — Fix the sets first; changing a codomain may change surjectivity.





## Error controls and negative controls

Total tablef needs two entries and g three; source lengths cannot be interchanged.

Comparison directionAn injection A to B gives ≤, whereas a surjection in that direction gives ≥.


- f is bijective. → reject — 3 has no preimage.
- g is injective. → reject — g(1)=g(3)=a with 1 distinct from 3.
- These finite examples prove every infinite surjection has a section. → reject — The certificates concern A,B,C only and handle neither infinite sets nor choice principles.





## Result and limitations

There is an injection A to B with |A|=2<3=|B|; a reverse surjection is not injective.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: f7395fd1e6ecb7e29d7182b804fa89d6a0e5440629fc2b259fbe84acd59ce55b
- original source SHA-256: f7395fd1e6ecb7e29d7182b804fa89d6a0e5440629fc2b259fbe84acd59ce55b
- 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-cardinality-comparison-01.json)