Squarefree kernels and perfect powers — Exact Proof Explorer

Squaring an actual divisor witness produces an actual squared divisor witness.

A squared prime divisor cannot evade the bounded squarefree definition: its base prime is itself a divisor and is at most the positive input.

The square of a genuine prime is never the unit.

Every squared divisor of a positive squarefree number has root one, not merely prime roots.

The squares of two coprime naturals are genuinely coprime.

Coprime cancellation turns a squared divisor of n times another square into a squared divisor of the squarefree n itself.

Restoring a prime-square factor multiplies the actual square root and preserves the squarefree kernel.

The square-root factor of a positive input is itself nonzero.

Finite induction decides absence of all squared prime divisors below any bound or constructs an actual bounded prime-square divisor.

Every positive input is squarefree or has a constructed actual prime-square divisor; no excluded-middle or factoring oracle is assumed.

Finite prime-square search and ordinary bounded induction construct the squarefree kernel and its square-factor root for every positive input.

Every positive natural is an actual squarefree natural times an actual natural square.

The unit is squarefree under the exact positive, prime-square-free definition.

Equal squarefree-times-square values with coprime square roots force both reduced roots to be one and both squarefree factors to agree.

Gcd reduction, coprime square cancellation and squarefreeness prove literal uniqueness of both the squarefree kernel and its natural square-factor root.

For every positive n, construct n=r*s² with squarefree r and prove every other natural such pair is exactly (r,s), including n=1.

Transport the actual terminal value of a power trace along equality.

Every nonnegative power of the unit has value one, proved by ordinary exponent induction.

Construct the actual identity 1=1^k uniformly for all nonnegative exponents, in particular every positive exponent required by the n=1 profile.

Two actual k-th power traces construct the power trace of the product of their roots.

A witnessed exponent quotient constructs the corresponding natural root of an actual prime power; this algebraic lemma needs no prime assumption.

An actual positive-degree power with positive value has a nonzero natural base.

Every positive k-th power has every actual prime valuation divisible by k, with a constructed quotient valuation of its nonzero base.

If all input prime valuations are multiples of k, removing one full prime power leaves that same property on the strictly smaller cofactor.

Construct a k-th root from divisibility of every prime valuation by strict full-prime-power descent; every quotient and recursive root is actually derived.

For every positive natural and positive degree, divisibility of all prime valuations constructs an actual natural root.

A common divisor of a successor beta prefix divides every entry of its predecessor.

A common divisor and its actual final divisibility witness extend to the entire successor prefix.

Every divisor of a common divisor is an actual common divisor of the same finite exponent list.

The empty exponent prefix has greatest common divisor zero, including all common divisors of the empty family.

The canonical gcd of the old actual prefix gcd and final decoded exponent is the gcd of the successor prefix.

Ordinary finite induction constructs a genuine gcd of every actual beta prefix, including empty and zero-entry prefixes.

The finite exponent gcd is literally unique by mutual actual divisibility.

A positive nonunit cannot have an empty actual prime-power support, since its empty product would be one.

The actual gcd of the positive valuations of a nonunit is positive; a decoded positive exponent prevents a zero gcd.

Every actual decoded exponent belongs to an actual prime and its exact valuation of the input.

Dividing all listed positive valuations implies dividing every prime valuation, using actual support coverage and zero valuation for absent primes.

Dividing every actual prime valuation implies being a common divisor of the actual finite exponent prefix.

A degree divides the finite exponent gcd exactly when it divides every prime valuation of the input.

The positive perfect-power degrees are exactly the divisors of the actual finite exponent gcd; the reverse direction constructs a real root.

Each positive divisor of the actual exponent gcd has a constructively available actual root, ready for finite beta tabulation.

Append one actual conditional root and preserve all earlier actual decoded roots in a beta prefix.

Decidable degree-zero and divisor tests construct a real root where required and a harmless zero filler elsewhere.

Finite induction constructs an actual beta table from the already proved pointwise root theorem, without any finite-choice axiom.

A positive gcd bounds all its positive divisors, so a finite table through index g covers every perfect-power degree.

Nine actual historical Pair constructors package the ten finite data fields without expanding a huge nested arithmetic numeral.

Every positive input constructs a real profile code: the uniform unit case or finite distinct valuations, their positive gcd and actual roots for every positive divisor of that gcd.

The gcd actually decoded from the supplied profile code classifies all positive perfect-power degrees in both directions.

A permitted positive degree retrieves an actual beta-decoded natural root from the constructed profile table, not a supplied arithmetic root.

Every profile really describes a positive input; zero is excluded by both branches of the definition.

The unit has exactly the distinguished uniform-identity profile tag, never a fictitious finite positive gcd of an empty valuation list.

Every nonunit profile exposes real decoded support, positive gcd and root-table data; the unit exception cannot masquerade as a finite gcd profile.

G010: every positive natural has a unique actual squarefree-times-square decomposition together with a genuinely encoded complete perfect-power profile, including the uniform unit exception.