Complementary divisors and finite involutions — Exact Proof Explorer

Every divisor of a positive input has a unique actual positive quotient, itself a divisor bounded by the input.

Decide zero and divisibility constructively, extracting a real quotient only in the positive-divisor branch.

The actual quotient and identity branches are disjoint and determine one output; beta-code equality is not assumed.

At every genuine positive divisor the complement output satisfies n=d*q; the identity convention cannot supply that branch.

For positive n the actual complementary quotient is reversible; zero and nondivisors remain fixed.

Divisor complementation stays in the exact inclusive interval 0..n, including its explicitly fixed omitted indices.

Finite HA induction constructs a genuine beta prefix of quotient values, rather than assuming a finite-choice or coding oracle.

Every actual beta lookup in the constructed finite window has the literal complementary-divisor graph.

The real S n-entry complement code is bounded and injective by its proved involution; constructive finite surjectivity yields a genuine permutation.

Every positive natural has an actually constructed finite divisor-complement permutation, with exact quotient equations on positive divisors.

Decoding the constructed finite map twice returns the original index, with the intermediate index proved to remain in bounds.

The actual beta code at a positive divisor is precisely its witnessed quotient, not merely an unspecified bounded permutation image.