Unique squarefree part · prime-exponent gcd · actual root tables · Constructive arithmetic

Squarefree kernels and perfect powers

n>0 ⇒ ∃r,s,w. Squarefree(r) ∧ n=r·s² ∧ PowerProfile(n,w), with r,s unique

Construct n=r·s² with unique squarefree r and a finite certificate classifying every positive perfect-power exponent.

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

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 2020 native tactic lines and 148 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem SK0035 and follow only the lemmas and conservative definitions supporting positive_squarefree_kernel_and_power_profile.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G010 milestone → theorem and definition dependencies.
Major independently established statements: SK0010 squarefree_decomposition_exists_unique · SK0030 perfect_power_profile_data_degree_classification · SK0031 perfect_power_profile_data_root_lookup · SK0033 perfect_power_profile_unit_code · SK0035 positive_squarefree_kernel_and_power_profile.
Independently verified Alpha v34 checked-use theorem family: 53 dependency-curried kernel-checked theorem bodies · 148 proof prerequisites · 26 linked definitions · 51 definition-dependency arrows · 2020 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: For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.