Finite prime-valuation support — Exact Proof Explorer

Equality transports an actual bounded valuation exponent without changing its prime or value.

Construct valuation zero for a positive value not divisible by the actual prime.

Valuation zero excludes divisibility, with both intended domain guards explicit.

The exact valuation of any witnessed nonnegative power is its exponent times the base valuation; zero powers are included.

Construct the actual maximal valuation graph of a witnessed power, not merely an equation between supplied output valuations.

Every positive power has its base as an actual divisor; no prime or positivity oracle is needed.

A power of a prime has zero valuation at every genuinely distinct prime, including exponent zero.

Every actual prime divisor of a witnessed prime power is its base prime.

Multiplying by a positive valuation-zero factor preserves the actual maximal exponent.

Removing a full prime power does not change any other prime valuation of the remaining positive cofactor.

Every decoded support entry is a prime that genuinely divides the supported value.

Restoring a removed full prime power preserves every old positive valuation, because its base prime is absent from the cofactor.

Actual prefix-preserving beta recodings preserve all prime/exponent/power data, without a sequence oracle.

A real final beta entry extends the prime-exponent data by one, including the empty-prefix boundary.

One has the actual empty distinct-prime support and empty product one, with no fictitious prime or positive valuation.

An equal positive value retains exactly the same actual prime, exponent and product codes.

Every positive nonunit has an actual full prime-power cofactor strictly smaller than itself; the exponent, power and nondivisibility are all constructed.

Append an actual new full prime power to three beta prefixes, preserving distinctness, all exact valuations, complete divisor support and the literal finite product.

Ordinary natural induction on an explicit upper bound constructs the whole distinct-prime support; every recursive cofactor is strictly smaller.

Every positive natural has a genuinely constructed finite list of distinct prime divisors, their positive exact valuations, corresponding powers and product equal to the input.