Constructive arithmetic and unique factorization — Exact Proof Explorer

G001: construct the quotient and strict remainder for every nonzero divisor and prove the pair is literally unique.

G002: every pair, including (0,0), has a canonical gcd value and actual signed-natural Bezout coefficient codes. Only the gcd is asserted unique, not its coefficients.

G003: coprimality and a witnessed divisor of the product construct an actual quotient of the other factor, with no positivity premise added.

G004: every positive natural has a genuinely constructed finite beta-coded prime-factor list and actual product trace; the existing sorted construction is used only to obtain witnesses, not required as a premise.

There is no natural index below zero; empty list and permutation contracts are genuinely vacuous.

Actual beta functionality turns a finite forward entry preservation into reverse preservation at every original index.

Every actual decoded entry of an all-prime prefix is prime, without a supplied choice of matching factor.

Construct an actual product value and trace for every finite beta prefix, including empty prefixes.

Cancel an actual final prime factor, retaining the nonzero predecessor product and all actual prime prefix entries.

Every nonempty prime factorization supplies an actual last prime, its actual quotient, and a genuine shorter factorization.

The only prime factorization of one has empty length; this is an actual-product statement, not a convention imposed on a list.

An actual prime divisor is found at an actual occurrence of every unordered prime factorization of the product.

The actual literal zero beta code is a bounded/injective/surjective matching permutation between any two empty factor prefixes.

Append the fresh top index to any actual finite permutation, construct the new beta code, and prove all three bijection conditions.

A matching map stays matching when the same actual last factor is appended to both lists and the fresh last index is appended to the map.

Construct a genuine matching permutation after adjoining the same last factor, retaining the exact prefix-preservation and fresh-index equations.

Existence-only append interface still returns an actual fully bijective matching beta map.

An actual swapped prefix reflects back to the original entry at every index other than the two moved indices.

Swapping two actual map entries preserves boundedness and injectivity and constructively recovers full finite surjectivity.

A genuine index swap retains every prime factor, including duplicate equal primes; no distinct-factor hypothesis is required.

The swapped prime list has an actual product trace with the identical nonzero product, not merely a proposed rearrangement equality.

Construct a full recoded prime-factor list moving a selected interior prime to the last position, with exact swap witnesses and an unchanged actual product.

Undo a target-list swap by swapping the two corresponding actual source-map entries. Entry alignment follows at the two moved positions and everywhere else by map injectivity.

Use the recursively constructed finite permutation's actual preimage, construct both extended and transposed map codes, and return a full matching bijection into the original unswapped target list.

Full induction on an arbitrary source factor list: locate the last prime in the arbitrary target, genuinely swap and cancel it, recursively match the shorter lists, and construct the restored index bijection. Neither list is assumed sorted or distinct.

Exact G005: every two arbitrary unordered prime factorizations of the same positive natural admit an actual coded matching bijection, with equal lengths and explicit boundedness, injectivity, and surjectivity.

Construct an actual prime-factor list for every positive natural and an actual matching permutation to every competing unordered factorization. Both factor-list existence and uniqueness witnesses are conclusions, with no supplied canonical factorization.