Canonical binary digits and certified repeated squaring — Exact Proof Explorer

Every genuine beta-coded prefix can be recoded while appending any exact last digit.

Recoding that preserves every earlier beta entry preserves its actual zero-or-one digit invariant.

An independently witnessed base-two Horner trace remains valid under every exact prefix recoding.

Every valid beta-coded binary prefix can append a real zero-or-one digit without changing any older entry.

Append a witnessed zero-or-one beta digit and prove that its new Horner value is exactly twice the prior exponent plus that digit.

If a binary quotient/digit value is below twice a bound, its exact quotient is below that bound.

Induction on the exact power exponent constructs a genuine length-l beta-coded binary representation of every natural strictly below 2^l.

Every actual BitLen witness supplies the exact beta-coded upper power 2^l and the strict inequality n < 2^l, including zero.

Every canonical binary-length witness constructs a genuine beta-coded equally long zero-or-one prefix whose base-two Horner value is the original exponent.

Every arbitrary natural exponent has an actual canonical-length beta-coded binary digit prefix with exactly that exponent as its Horner value.

A fixed actual beta-coded binary digit sequence represents exactly one natural Horner exponent.

All canonical beta-coded binary representations of one exponent have the identical genuine BitLen length.

Every universal genuine digit-prefix invariant yields actual beta-decoded zero-or-one witnesses at every position.

Every actual beta-coded binary prefix has an independently beta-witnessed exact population count.

The initialization-plus-three-per-digit arithmetic expression is exactly 3*l+2 in the unchanged Peano kernel.

Every actual coded digit prefix has a witnessed operation cost of two initializations, two operations per digit, and one optional multiply per one bit.

The independently witnessed initialization/square/multiply operation count is functional for every fixed beta-coded digit prefix.

The actual beta-counted initialization/square/optional-multiply cost of any binary prefix is at most 3*l+2.

Every actual execution driven by canonical digits of the supplied arbitrary exponent has exactly that exponent's proved modular power.

For every arbitrary natural exponent and guarded modulus, construct canonical beta-coded digits, their full genuine square-and-multiply history, and its proved modular-power result.

Complete actual executions for the same arbitrary exponent have identical canonical residues even when their independently constructed digit codes differ.

Every arbitrary natural exponent has exactly one canonical modular result produced by genuine constructed canonical-length beta-coded execution.

Every complete actual canonical-length square-and-multiply execution has genuine BitCount-measured operation cost at most 3*BitLen(exponent)+2.

For every arbitrary natural exponent and guarded modulus, construct canonical BitLen digits, an actual beta-coded square-and-multiply trace and modular power, the exact beta-counted operation cost, and the constructive bound operations <= 3*BitLen(exponent)+2.