Subtraction-free power differences · prime steps · full exponent decomposition · Constructive arithmetic

Lifting the exponent for odd primes

vₚ(xⁿ−yⁿ)=vₚ(x−y)+vₚ(n) for odd prime p, x>y>0, n>0, p∣x−y, p∤xy

Construct the powers and their positive difference, and calculate its exact prime valuation.

Open the definition-aware map Read the final theorem See campaign milestone G036

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 2157 native tactic lines and 189 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EL0026 and follow only the lemmas and conservative definitions supporting odd_prime_lifting_the_exponent_value.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G036 milestone → theorem and definition dependencies.
Major independently established statements: EL0024 odd_prime_lifting_the_exponent · EL0026 odd_prime_lifting_the_exponent_value.
Independently verified Alpha v34 checked-use theorem family: 38 dependency-curried kernel-checked theorem bodies · 189 proof prerequisites · 13 linked definitions · 16 definition-dependency arrows · 2157 exact tactic lines · first admitted v29 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 566 bundle nodes; SHA-256 4fcb3cd45e83448776abb9e33692496a7acfa98a051cae15761826a0b15fda44.
Exact mathematical boundary: All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.