Unique factorization in the Gaussian integers — Exact Proof Explorer

Every valid canonical Gaussian code has actual signed-coordinate representatives.

Proved equality of canonical natural codes preserves the actual signed representation.

An actual norm witness certifies membership in the Gaussian carrier.

Actual Gaussian add certifies the input left carrier, without treating every natural code as valid.

Actual Gaussian add certifies the input right carrier, without treating every natural code as valid.

Actual Gaussian add certifies the output carrier, without treating every natural code as valid.

Actual Gaussian multiply certifies the input left carrier, without treating every natural code as valid.

Actual Gaussian multiply certifies the input right carrier, without treating every natural code as valid.

Actual Gaussian multiply certifies the output carrier, without treating every natural code as valid.

Embed a natural real coordinate using its actual even signed code and the unchanged Gaussian pair encoding.

The actual canonical Gaussian zero code is 0, with its signed coordinates proved rather than asserted.

The canonical Gaussian zero belongs to the actual signed-pair carrier.

The actual squared Gaussian norm of zero is 0.

The actual canonical Gaussian one code is 6, with its signed coordinates proved rather than asserted.

The canonical Gaussian one belongs to the actual signed-pair carrier.

The actual squared Gaussian norm of one is 1.

Actual signed-coordinate Gaussian add is commutative by ordinary natural identities.

The actual canonical Gaussian add graph is commutative; output code equality is not assumed.

Actual signed-coordinate Gaussian multiply is commutative by ordinary natural identities.

The actual canonical Gaussian multiply graph is commutative; output code equality is not assumed.

Equality transports the uniquely defined actual Gaussian norm value.

A nonzero actual Gaussian integer has nonzero squared norm.

Zero actual Gaussian norm forces literal zero canonical code, by constructive equality decision.

The actual norm of the zero canonical code is zero, not a positive auxiliary value.

An actual inverse multiplies norms to one, forcing the unit norm to equal one.

Norm one constructs an actual inverse: the canonical conjugate multiplies the value to Gaussian identity code six.

The inverse-witness definition of Gaussian unit is equivalent to the independently defined squared norm being one.

Actual Gaussian units are constructively decidable by computing the actual norm and deciding equality with one.

A Gaussian multiplicative unit cannot have zero canonical code.

The inverse-witness unit definition enforces the actual Gaussian carrier.

The actual Gaussian ring has no zero divisors, proved from multiplicative norms and natural multiplication.

Equal represented Gaussian integers have literally equal canonical natural codes.

Actual signed-coordinate Gaussian sums associate by proved natural addition identities.

Cancel a common represented integer summand using ordinary natural addition cancellation.

A common Gaussian summand cancels in both actual represented integer coordinates.

The actual canonical Gaussian add graph associates, with all intermediate product/sum codes witnessed.

The actual canonical Gaussian multiply graph associates, with all intermediate product/sum codes witnessed.

The actual canonical Gaussian add zero identity holds on the entire valid carrier.

Commutativity supplies the actual left add zero identity.

The actual canonical Gaussian multiply one identity holds on the entire valid carrier.

Commutativity supplies the actual left multiply one identity.

The actual canonical Gaussian multiply zero identity holds on the entire valid carrier.

Commutativity supplies the actual left multiply zero identity.

Every actual Gaussian difference has a constructed canonical code solving c+b=a, without assuming a subtraction oracle.

The actual canonical Gaussian additive operation is cancellative, proved in both signed coordinates.

A proved equal output code preserves the actual Gaussian add graph.

A proved equal output code preserves the actual Gaussian multiply graph.

Actual Gaussian products can be reassociated in the reverse direction without assuming the unknown intermediate result.

Interchange the two tail factors of an actual Gaussian triple product while retaining its literal output code.

Guided ordinary-HA distributivity for the actual Gaussian real positive component; no AC search or new tactic.

Guided ordinary-HA distributivity for the actual Gaussian real negative component; no AC search or new tactic.

Guided ordinary-HA distributivity for the actual Gaussian imaginary positive component; no AC search or new tactic.

Guided ordinary-HA distributivity for the actual Gaussian imaginary negative component; no AC search or new tactic.

Actual Gaussian multiplication distributes over addition in both signed integer coordinates.

The sum of two actual Gaussian products is the product with their actual summed second factors.

An actual Gaussian product of a sum equals the actual sum of the two given products.

Actual Gaussian multiplication also distributes when the common factor is on the right.

A common right summand cancels in the actual canonical Gaussian additive graph.

A nonzero Gaussian factor cancels, using an actually constructed difference, distributivity and the proved absence of zero divisors.

A nonzero common right Gaussian factor cancels in the actual canonical multiplication graph.

The actual canonical Gaussian identity code six is a unit with itself as inverse.

Every inverse witness is itself an actual unit and is a two-sided inverse.

An actual product of Gaussian units is a unit, by norm multiplicativity and the proved inverse construction at norm one.

Every actual left factor of a Gaussian unit has a constructed inverse, without an irreducibility assumption.

Every actual right factor of a Gaussian unit is also a genuine unit.

A witnessed Gaussian divisor belongs to the actual canonical Gaussian carrier.

An actually divisible Gaussian value has a valid canonical carrier code.

Each actual Gaussian integer divides itself with canonical quotient six, the Gaussian identity.

Each actual Gaussian integer divides zero with its actual zero quotient.

The actual Gaussian identity divides every valid Gaussian integer.

A zero Gaussian divisor can divide only the actual zero code.

Compose actual Gaussian quotient witnesses using the proved canonical multiplication law.

An actual divisor of the first factor divides the actual Gaussian product.

An actual divisor of the second factor also divides the actual Gaussian product.

A common Gaussian divisor divides the actual sum, with the sum of quotient codes genuinely constructed.

A common Gaussian divisor divides an actual difference; quotient subtraction is constructed and verified in the real ring graph.

An actual unit divides every valid Gaussian value via its inverse witness and the identity.

Every actual Gaussian divisor of a unit is itself a unit.

Every common divisor of the divisor and remainder divides the actual Gaussian dividend.

Every common divisor of the actual Gaussian dividend and divisor also divides the actual remainder.

An actual Gaussian zero remainder gives an actual quotient witnessing divisibility.

A strictly norm-bounded Gaussian remainder must vanish when the original divisor actually divides the dividend.

Constructively decide actual Gaussian divisibility by computing Euclidean quotient/remainder data; handle a zero divisor explicitly.

Every Gaussian integer is associated to itself by the actual unit code six.

Invert the actual unit witness to reverse Gaussian association, including the zero boundary.

Compose actual unit witnesses and their canonical products to prove transitive Gaussian association.

A genuinely unit cofactor supplies the witnessed association relation.

Associated Gaussian integers are actually divisible, using the given unit as quotient.

A witnessed Gaussian unit association preserves the actual squared norm.

Mutual actual divisibility is witnessed association, with the all-zero case handled explicitly and the nonzero case using real multiplication cancellation.

An actual Gaussian divisor has a constructed quotient norm, and the ordinary natural norms factor exactly.

Every actual divisor of a nonzero Gaussian value has norm at most the value norm; the positive quotient-norm gap is constructed explicitly.

An actual nonunit divisor of an irreducible Gaussian integer differs from it by a constructed unit, not merely a norm equality.

Two irreducible Gaussian factors with actual divisibility are associated by a witnessed unit.

The zero-right Gaussian gcd is the first input, with actual Bézout coefficients six and zero, including the all-zero pair.

A proved zero second code yields genuine gcd and Bézout witnesses without rewriting or assuming arbitrary carrier validity.

Every actual common Gaussian divisor divides an actual Bézout combination.

Transport the actual greatest-common-divisor property backwards through a proved Gaussian Euclidean equation.

Construct the coefficient u-qv and verify the complete Gaussian Bézout back-substitution using actual products, differences, distribution and addition.

Ordinary natural induction constructs Gaussian gcd and genuine signed Bézout coefficients for every valid pair; each actual Euclidean remainder strictly decreases the norm bound.

Every pair of actual Gaussian integers has a constructed gcd with actual Gaussian Bézout coefficients, without a supplied norm, trace or positivity premise.

Actual Gaussian gcd values are unique up to a witnessed unit, not falsely unique as canonical natural codes.

An actual unit-valued Gaussian Bézout combination proves Euclid cancellation for actual divisors, by constructing every multiplied term and the genuine unit inverse.

If a nonzero actual Gaussian product divides one factor, its other factor has a constructed inverse; no abstract domain axiom is assumed.

Every Gaussian irreducible is an actual prime divisor, proved constructively from the computed gcd and Bézout coefficients rather than assumed as a factorization axiom.

The actual irreducibility graph implies the full RingPrime divisor graph, retaining all carrier, nonzero and nonunit clauses.

The full Gaussian prime-divisor graph implies genuine factor irreducibility by constructing the inverse of a cofactor of every nonzero factorization.

Gaussian irreducibles and actual prime divisors coincide constructively, through proved arithmetic graph bridges in both directions.

Every natural is at most its square, including zero, by constructive equality decision.

A canonical signed code for an integer whose square is bounded by N is at most 2N, for both signs and zero.

Every pair of canonical signed-coordinate codes constructs a valid Gaussian code; arbitrary natural codes are not presumed valid.

An actual Gaussian norm bounds both canonical signed-coordinate codes; arbitrary non-normal representatives are never bounded.

The empty search interval has no index, proved in the original natural arithmetic.

A nonzero natural different from one is at least two, with both small boundaries explicit.

Equality of actual Gaussian natural codes preserves the witnessed proper-norm-divisor graph.

Decide a genuine nonunit divisor and strict actual norm bound using G081 division, norm functionality and natural order decision.

Finite induction checks every imaginary coordinate below k, returning an actual proper divisor or a proof that none is present.

Two ordinary finite inductions exhaust the actual signed-coordinate rectangle, with a witness or an explicit absence theorem.

A larger norm bound preserves the two actual finite signed-coordinate bounds.

A finite (2N+1)-by-(2N+1) coordinate search decides whether any actual Gaussian proper-norm divisor exists, with no validity oracle.

The actual nonzero norm of a Gaussian nonunit is at least two; a norm-one exception would construct an inverse.

In an actual nonzero product of two Gaussian nonunits, both natural factor norms are strictly smaller than the product norm.

Every actual product of two nonunits supplies a genuine proper-norm divisor, so the finite search cannot miss a reducible nonzero value.

An actual divisor of a nonzero Gaussian value is nonzero, including the canonical zero boundary.

A found proper-norm divisor yields an actual quotient; both factors are nonunits with strictly smaller actual norms.

A finite constructive search proves irreducibility or produces an actual strictly norm-decreasing nonunit factorization; no classical negated-universal extraction is used.

Irreducibility of any actual Gaussian integer is constructively decidable, with zero, all units, and actual nonunit factors handled separately.

Ordinary bounded-norm induction constructs an irreducible divisor of every nonzero Gaussian nonunit, using the actual finite factor search at each descent.

Every actual nonzero Gaussian nonunit has an actually witnessed irreducible Gaussian divisor, with no supplied search oracle.

Dividing a nonzero Gaussian value by an actual nonunit strictly decreases the quotient norm, even when the quotient itself is a unit.

Construct an actual irreducible factor and a nonzero, strictly norm-smaller quotient for every nonzero Gaussian nonunit; this is the finite-factorization recursion step.

Equality of beta indices transports the actual bounded remainder entry in both occurrences of its modulus.

Equality of factor codes transports both boundedness and the actual beta remainder equation.

Every empty Gaussian factor prefix has a genuine constant product trace with canonical value six, not natural one.

Functionality of the zero-th trace entry forces the actual empty product to be the Gaussian identity code.

Preserving actual factor entries preserves the same genuinely multiplied Gaussian product trace.

Every nonempty actual Gaussian product exposes its final factor, the actual shorter prefix product, and the genuine final multiplication.

Append a genuine Gaussian multiplication step using a constructed beta extension of the product trace, preserving all previous steps.

Equality of actual canonical product values transports the endpoint of a real beta multiplication trace.

Equality of natural lengths transports the exact endpoint and bound of an actual Gaussian multiplication trace.

Two actual Gaussian multiplication traces on the same finite beta prefix have literally equal canonical endpoint codes.

Every actual finite Gaussian product has a valid carrier code, including the empty product.

Literal equality of canonical Gaussian codes preserves the full actual-factorization irreducibility predicate.

Every shorter prefix of an actual all-irreducible Gaussian list remains all irreducible.

Appending an actual irreducible Gaussian factor preserves all irreducible entries of the newly constructed beta prefix.

Every actual Gaussian unit is factored by its own unit code and an empty prime list, with the actual identity product.

Construct and verify a longer Gaussian prime-factor list by appending one actual irreducible factor while retaining the actual leading unit.

Construct a genuine finite irreducible Gaussian factorization by ordinary norm induction; each recursive quotient has strictly smaller proved norm.

Every actual nonzero Gaussian integer has an actual unit coefficient and an actually multiplied finite list of irreducible factors, including every unit boundary.

Every listed Gaussian irreducible is an actual prime divisor by the checked Bezout theorem, with the unit and product trace unchanged.

The actual Gaussian prime-divisor graph implies irreducibility, so the two finite factorization specifications are equivalent.

Every actual nonzero Gaussian integer has a genuine finite RingPrime factorization, not merely a conditional gcd or a supplied factor-list certificate.

Equality of lengths transports the exact finite bound of an all-irreducible Gaussian factor prefix.

Construct an actual Gaussian product trace for every all-irreducible beta prefix, including empty prefixes and repeated associate factors.

A finite product of actual irreducible Gaussian factors is nonzero, by the proved absence of Gaussian zero divisors and the genuine empty product.

An actual all-irreducible Gaussian product is a unit only at length zero; no nonempty unit factorization is allowed by the arithmetic.

Every actual Gaussian factorization reconstructs a value in the genuine canonical carrier.

The actual unit coefficient and actual irreducible product prevent any Gaussian factorization of zero.

Find an actual occurrence associated to an irreducible divisor in any finite irreducible Gaussian product, using the proved prime-divisor product theorem at every step.

Ordinary induction proves the actual Gaussian replacement balance Q*p=P*q with genuine product traces and actual common output code, including zero and unit factors.

The actual Gaussian replacement balance holds in both directions; reflection of unchanged beta entries is proved rather than assumed.

An actual interior/last beta swap preserves the literal canonical value of a genuine Gaussian multiplication trace, without nonzero, irreducibility or unit hypotheses.

Equality of actual canonical codes transports an unchanged witnessed Gaussian unit association.

A witnessed Gaussian association transports actual unit status by multiplying the two actual units.

Cancel associated nonzero last factors from associated actual products, constructing the resulting prefix association from actual unit witnesses.

Expose the actual prefix product before a specifically decoded last Gaussian factor; beta functionality fixes the chosen factor exactly.

The actual zero beta map is a bounded, injective, surjective unit-matching bijection between any two empty factor prefixes.

Adjoining associated actual last factors and a fresh fixed last index preserves witnessed unit matching; literal factor-code equality is not required.

Construct a real fully bijective beta index map after appending any two associated Gaussian factors, retaining all actual prefix entries.

An actual finite swap retains all Gaussian irreducible factors, including repetitions and distinct unit associates.

Undo an actual target factor swap by swapping the corresponding actual map entries; original unit witnesses remain valid at both moved positions and every unchanged index.

Construct a real full unit-matching bijection into the unswapped target list using the recursive permutation, its actual preimage, a fresh last index and an actual transposed beta map.

Equality of lengths transports all actual last-entry indices and the finite preservation bound of a witnessed swap.

Construct a swapped actual irreducible beta list and a real product trace with exactly the original Gaussian value, using the independently proved Gaussian swap law.

Any two actual finite irreducible Gaussian products which differ by a witnessed unit have equal length and an actually constructed bounded/injective/surjective matching permutation, including empty lists and repeated associates.

Any two actual irreducible Gaussian factorizations of the same value have equal length and an actual unit-matching finite bijection; distinct leading units are allowed.

The uniqueness theorem applies to every actual RingPrime factorization, using the proved prime/irreducible equivalence rather than redefining a prime label.

Full constructive G082: every actual nonzero Gaussian integer has a finite actual RingPrime factorization, and every other such factorization differs by a constructed beta permutation and witnessed multiplicative units.

The actual zero Gaussian code has no finite unit-times-prime factorization; the nonzero guard is mathematically necessary.

Every factorization of any of the four actual Gaussian units has an empty prime list, proved from actual product and inverse witnesses.