# Complete inverse pairing and both Wilson directions

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

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-wilson-theorem-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For n>1, (n-1)!=-1 mod n exactly when n is prime; the full modulo-7 inverse table checks 6!=6 mod 7.

A general two-direction teaching argument plus full modulo-7 data and the p=2 branch; finite tests do not replace proof.





## Givens and symbols


- calc


- G1 — n is an integer greater than 1; use p in the prime direction, with p=7 as the example.


- d — proper positive divisor
- p — prime modulus





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus. Explicitly assume coprime Bezout and Euclid's prime lemma p dividing ab implies p dividing a or b.
- mko_definition · cited — Qualify the integer domain n>1. For a prime modulus list the inverses of every nonzero residue and cancel the distinct inverse pairs. When p>2 the self-inverse residues are 1 and p−1; at p=2 they coincide. Exact factorial tables check the congruence at the specified modulus. Composite instances do not replace the converse proof, and a finite testing range does not prove the universal equivalence. Wilson factorial congruence and Fermat power congruence are different statements. · mko-wilson-theorem





## Main derivation

S01 · impliesBefore

p\text{ prime},\quad1\le a<p

After

\gcd(a,p)=1\Rightarrow\exists a^{-1}\pmod p

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

A prime has only proper positive divisor 1, so every nonzero class is coprime and Bezout provides an inverse.



S02 · impliesBefore

a=a^{-1}\pmod p

After

a^2\equiv1\Rightarrow p\mid(a-1)(a+1)\Rightarrow a\equiv1\text{ or }-1\pmod p

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Euclid's lemma determines all self-inverse classes; for p>2,1 and -1 are distinct.



S03 · impliesBefore

p>2,\quad a\ne a^{-1}

After

\{a,a^{-1}\}\text{ disjoint inverse pairs},\quad aa^{-1}\equiv1\pmod p

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Inversion is an involution, partitioning all non-self-inverse classes into disjoint two-element pairs.



S04 · impliesBefore

\prod_{a=1}^{p-1}a\text{ paired as above}

After

(p-1)!\equiv1\cdot(-1)\cdot1\equiv-1\pmod p

Conditions: none

Rule: calc · Uses: G1, S02, S03

Leaf basis: calc

In the product of all nonzero classes, ordinary inverse pairs give 1 and self-inverses 1,-1 leave -1.



S05 · impliesBefore

p=2

After

(2-1)!=1\equiv-1\pmod2

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

At even prime 2,1 and -1 are the same single class; the formula holds directly.



S06 · impliesBefore

p=7,\quad a=1,2,3,4,5,6

After

a^{-1}=1,4,5,2,3,6\text{ respectively}

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

The complete six-entry inverse list gives pairs {1},{6},{2,4},{3,5}.



S07 · impliesBefore

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

After

j!\bmod7=1,2,6,3,1,6\text{ respectively};\quad6!=720\equiv6\pmod7

Conditions: none

Rule: calc · Uses: G1, S04, S06

Leaf basis: calc

A complete incremental factorial table independently checks prime 7, with residue 6 representing -1.



S08 · impliesBefore

n>1\text{ composite},\quad1<d<n,\quad d\mid n

After

d\mid(n-1)!

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

A composite has a proper divisor d, which appears as a factor in 1 through n-1, so d divides the factorial.



S09 · impliesBefore

(n-1)!\equiv-1\pmod n,\quad d\mid n,\quad d\mid(n-1)!

After

d\mid((n-1)!+1)\text{ and }d\mid(n-1)!\Rightarrow d\mid1\text{ impossible}

Conditions: none

Rule: calc · Uses: G1, S08

Leaf basis: calc

If a composite passed Wilson, subtraction would make d>1 divide 1, a contradiction, proving the converse.



S10 · impliesBefore

n>1,\quad\text{prime direction and composite contradiction}

After

n\text{ prime}\iff(n-1)!\equiv-1\pmod n

Conditions: none

Rule: mko_definition · Uses: G1, S04, S05, S07, S09

Leaf basis: mko_definition

Both directions together with p=2 complete the equivalence; the modulo-7 table is only an instance certificate.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S10 · premise_audit · G1, S04, S05, S07, S09 — n=1 is outside the domain and cannot be added from a degenerate factorial residue.
- S09 · premise_audit · G1, S08 — This is a general contradiction argument, not a substitute based on several composite tests.
- S08 · premise_audit · G1 — No claim that every composite factorial is zero modulo n is needed; n=4 is covered too.
- S07 · premise_audit · G1, S04, S06 — Wilson uses a factorial rather than a Fermat base power.
- S06 · premise_audit · G1, S01, S02 — 2*4=8,3*5=15,6^2=36 all reduce to 1, checking every listed pair.
- S05 · premise_audit · G1, S01 — Do not count the coincident self-inverse representatives twice.
- S04 · premise_audit · G1, S02, S03 — This argument covers arbitrary odd primes rather than extrapolating the p=7 table.
- S03 · premise_audit · G1, S01, S02 — The inverse of a inverse is a, so no class is missed or paired twice.
- S02 · premise_audit · G1, S01 — Primality is essential for the zero-product implication; composite moduli need not satisfy it.
- S01 · premise_audit · G1 — The inverse is unique as a class: ab=ac=1 gives b=b(ac)=(ba)c=c.





## Error controls and negative controls

Complete pairingEvery nonzero class must be paired or listed as self-inverse.

Both directionsSeparate prime pairing from the composite proper-divisor contradiction, without universal inference from tests.


- Composite 4 also passes Wilson. → reject — 3!=6 is 2 modulo 4, while -1 is 3.
- p=2 has two distinct self-inverse classes. → reject — 1=-1 modulo 2, giving one class.
- Wilson is the statement a^(p-1)=1. → reject — Wilson concerns (p-1)!; Fermat concerns powers of a fixed base.





## Result and limitations

For n>1, (n-1)!=-1 mod n exactly when n is prime; the full modulo-7 inverse table checks 6!=6 mod 7.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 21bca817d48683970a4a4d8b31d62b9415855aa678ab3aa40682b18bfd6d1cdb
- original source SHA-256: a2d4d999d4312d01eaa71a10b634018e935b72665829e46b09f492efd7ebc702
- 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-wilson-theorem-01.json)