Constructive binary modular execution and power correctness — Exact Proof Explorer

Every empty beta-coded prefix is constructively a valid binary digit sequence.

Every valid successor-length binary digit prefix has a valid predecessor prefix.

Every nonempty valid beta-coded binary prefix has a genuine final zero-or-one digit.

There is a real beta code whose initial square-and-multiply accumulator is one.

Every actual modular square-and-multiply transition explicitly carries a binary digit.

For every guarded modulus, the actual initial accumulator one is the canonical zeroth power.

One exact binary zero transition preserves the witnessed canonical power invariant.

One exact binary one transition preserves the witnessed canonical power invariant.

Every actual zero-or-one modular transition preserves the matching binary-prefix power.

Append one genuine beta-coded binary digit and canonical modular transition while preserving every previous execution state.

Natural induction constructs a complete genuine beta-coded square-and-multiply trace for every supplied valid finite binary digit prefix.

Every guarded valid coded binary digit prefix has a genuine witnessed modular execution and decoded terminal result.

The terminal accumulator of any actual empty binary execution is exactly one.

Every nonempty actual binary execution decomposes into its exact valid predecessor and final modular transition.

A valid final Horner digit yields the exact exponent decomposition e=2h+d.

Every genuine coded square-and-multiply execution is the canonical modular power of the exact base-two Horner exponent represented by its digit prefix.

Every valid beta-coded binary prefix has a witnessed Horner exponent, complete actual modular execution, and independently proved canonical power invariant.

Any two complete actual coded square-and-multiply executions of the same guarded binary prefix have identical terminal residues.

Every supplied valid beta-coded binary prefix has exactly one genuine guarded square-and-multiply execution result.