# Counting phi(12) representative by representative

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

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-euler-totient-function-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

phi(12)=4, phi(1)=1, and here phi(3*4)=phi(3)*phi(4).

Complete representative ranges 1≤k≤n; multiplicativity is checked for a coprime instance only.





## Givens and symbols


- calc


- G1 — n=12; count gcd(k,12)=1 over exactly 1,2,3,4,5,6,7,8,9,10,11,12.


- \varphi(n) — number of coprime representatives
- U_n — complete reduced representatives





## Rules and sources


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus.
- mko_definition · cited — This slice consistently uses the complete range 1≤k≤n and counts gcd(k,n)=1. Multiplicativity is checked only for explicit instances with gcd(m,n)=1, not extrapolated from noncoprime inputs. · mko-euler-totient-function





## Main derivation

S01 · impliesBefore

1\le k\le12

After

K=\{1,2,3,4,5,6,7,8,9,10,11,12\}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

List all twelve representatives first, with neither zero nor a duplicated endpoint.



S02 · impliesBefore

k=1,2,3,4,5,6

After

\gcd(k,12)=1,2,3,4,1,6\text{ respectively}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Exact gcds for the first six entries leave only 1 and 5 coprime.



S03 · impliesBefore

k=7,8,9,10,11,12

After

\gcd(k,12)=1,4,3,2,1,12\text{ respectively}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Checking all remaining six entries leaves 7 and 11 coprime.



S04 · impliesBefore

U_{12}=\{1,5,7,11\}

After

\varphi(12)=|U_{12}|=4

Conditions: none

Rule: mko_definition · Uses: G1, S02, S03

Leaf basis: mko_definition

The two complete gcd lists give all and only the four coprime representatives.



S05 · impliesBefore

n=1,\quad K_1=\{1\}

After

\gcd(1,1)=1\Rightarrow\varphi(1)=1

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Under the same 1-through-n convention, n=1 has one valid coprime representative.



S06 · impliesBefore

K_3=\{1,2,3\},\quad K_4=\{1,2,3,4\}

After

U_3=\{1,2\},\quad U_4=\{1,3\},\quad\varphi(3)=2,\ \varphi(4)=2

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The complete gcd lists (1,1,3) and (1,2,1,4) give both values.



S07 · impliesBefore

\gcd(3,4)=1,\quad12=3\cdot4

After

\varphi(12)=4=2\cdot2=\varphi(3)\varphi(4)

Conditions: none

Rule: calc · Uses: G1, S04, S06

Leaf basis: calc

After checking coprimality, the computed values verify this multiplicativity instance.



S08 · impliesBefore

U_2=\{1\},\quad U_8=\{1,3,5,7\}

After

\varphi(2)\varphi(4)=1\cdot2=2\ne4=\varphi(8)

Conditions: none

Rule: calc · Uses: G1, S06, S07

Leaf basis: calc

The full modulo-8 gcd list (1,2,1,4,1,2,1,8) shows noncoprime factors 2,4 cannot be used unconditionally.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S06, S07 — This refutes dropping coprimality, not S07.
- S07 · premise_audit · G1, S04, S06 — This is the specified coprime instance, not a proof of general multiplicativity.
- S06 · premise_audit · G1 — Each small representative range includes its endpoint, which is not coprime here.
- S05 · premise_audit · G1 — The observation that n is noncoprime for n≥2 does not apply to n=1.
- S04 · premise_audit · G1, S02, S03 — This counts neither coprime pairs nor proper divisors, only this representative set.
- S03 · premise_audit · G1, S01 — 12 is in the representative range but gcd(12,12)=12, not a unit.
- S02 · premise_audit · G1, S01 — For example gcd(5,12)=1 since 12=2*5+2 and 5=2*2+1.
- S01 · premise_audit · G1 — This slice uses 1 through n; adding zero would duplicate a residue.





## Error controls and negative controls

Representative rangeUse 1 through n consistently, not a mixture with 0 through n-1.

Coprimality gateCheck gcd(m,n)=1 before multiplicativity.


- phi(12)=5 because zero is coprime too. → reject — Zero is outside 1 through 12 and gcd(0,12)=12.
- phi(1)=0. → reject — Its sole representative 1 is coprime to 1.
- phi(mn)=phi(m)phi(n) for every m,n. → reject — m=2,n=4 gives 4 distinct from 2.





## Result and limitations

phi(12)=4, phi(1)=1, and here phi(3*4)=phi(3)*phi(4).







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ca0b196e2434f2d382e24c3145852b45b5cf3005501150b6d891d5af24fa9d03
- original source SHA-256: ca0b196e2434f2d382e24c3145852b45b5cf3005501150b6d891d5af24fa9d03
- 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-euler-totient-function-01.json)