Phi-hiding: disproof and Lean formalization

21 July 2026

Disproof (Markdown) Lean source

What is disproved

The claim that e ∣ φ(N) is equivalent to the map x ↦ x^e on ℤ/Nℤ* being exactly e-to-one. Consequently, the associated “exactly e-to-one versus permutation” restatement is also invalid. For e = 3, those exact-map promises are publicly distinguishable by reducing N modulo 3.

What is not disproved

A phi-hiding assumption defined directly as indistinguishability between two explicit modulus samplers—one satisfying e ∣ φ(N), the other satisfying gcd(e, φ(N)) = 1. Its truth depends on the samplers and their public side conditions. The argument below does not give a universal distinguisher for every such pair of distributions.

Counterexample to the equivalence

For N = pq, the kernel of exponentiation has cardinality

|ker(x ↦ x^e)| = gcd(e, p − 1) · gcd(e, q − 1).

Take N = 91 = 7 · 13 and e = 3. Then

3⁴ = 81 < 91,      3 ∣ φ(91) = 72,
|ker(x ↦ x³)| = gcd(3, 6) · gcd(3, 12) = 9.

Every nonempty fiber therefore has nine elements, not three.

Public distinguisher for the exact-map promises

Let p and q be primes other than 3.

Thus N % 3 == 2 distinguishes these two promises perfectly.

Lean coverage

PhiHiding.lean proves the RSA kernel formula, equality of nonempty fiber sizes, the N = 91 counterexample, and correctness of the modulo-3 distinguisher. The file contains no sorry, admit, or added axioms.

lake update
lake exe cache get
lake build