Lifting the exponent for odd primes — Exact Proof Explorer

The square difference has a genuine nonnegative geometric quotient.

A power-difference quotient advances by the actual recurrence a*Q+B.

The first correction term advances by b*C+Q without division or subtraction.

The doubled correction recurrence has an ordinary polynomial certificate with explicit coefficient carriers.

Consecutive triangular coefficients advance by exactly twice the next index.

Twice the correction has the exact triangular coefficient and an actual next remainder.

Every natural base has an actual beta-coded zeroth power equal to one.

The relational first power is constructed, not supplied as an oracle.

The relational second power is the actual square, including a zero base.

Construct the real powers, difference quotient, first correction, and doubled triangular correction at every exponent at least two.

A value not divisible by p is nonzero, for every p including zero.

An actual prime does not divide one.

Nondivisibility of a product excludes divisibility of its right factor.

Adding any actual p-multiple preserves nondivisibility; natural differences are witnessed by balanced equality.

Two is a nondivisor unit for every prime explicitly different from two.

Every witnessed power of a nondivisor remains a nondivisor of the actual prime, including the zeroth power.

The doubled second-order remainder is divisible by an odd prime, so its actual correction is divisible too.

The prime-step quotient is exactly p times a genuine p-nondivisible cofactor; no valuation conclusion is assumed.

Equality transports one actual relational-power argument without changing the graph or adding a choice principle.

Equality transports one actual relational-power argument without changing the graph or adding a choice principle.

Construct a composed power graph from two actual powers and their exact multiplied exponent.

Every maximal valuation of a prime at itself is exactly one, derived by actual cofactor cancellation.

Construct the actual bounded maximal valuation graph Val(p,p,1) for an actual prime.

Construct the exact sum valuation of a nonzero product instead of requiring its output valuation as an input.

The actual e-th power of a prime has exactly valuation e, including exponent zero.

An actual prime-power times a genuine nondivisor cofactor constructs its precise maximal valuation, including the unit boundary.

Construct the actual p-th powers and their geometric quotient p*u with a genuine p-nondivisible cofactor for every odd prime.

For every exponent not divisible by the actual prime, construct real power differences with a nondivisible geometric quotient; exponent one is handled explicitly.

Combine real power graphs, a nonzero difference quotient, and its independently constructed valuation into the exact lifted difference.

Raising a genuine nonzero p-divisible difference to an odd-prime exponent increases its exact valuation by one and constructs all power/difference witnesses.

Every exponent not divisible by p preserves the exact valuation of the difference, with actual power/difference witnesses and nonzero guards.

Ordinary HA induction constructs every prime-power exponent and its power difference, raising the valuation by exactly the number of prime steps.

For every positive exponent, strip its actual prime-power valuation, iterate the prime step, and apply the nondivisor cofactor step to construct the full exact LTE valuation.

A witnessed strictly positive natural difference is nonzero.

The exact p>2 guard excludes the binary prime without an implicit case extension.

Full guarded odd-prime LTE: for p>2, x>y>0, n>0, p|(x-y), and p not dividing xy, construct x^n,y^n and their positive difference of exact valuation v_p(x-y)+v_p(n).

Any two witnesses for the same natural power difference have exactly the same value; no selected representation can change the valuation output.

The full LTE valuation holds for every actual supplied power/difference witness, by extensionality of the constructed power graphs.