Constructive Gaussian Euclidean division — Exact Proof Explorer

A checked adjacent natural-product permutation supplies small ordinary-tactic polynomial calculations for both quadratic integer rings.

Every signed pair admits an actual floor quotient and strict remainder for every nonzero natural divisor; one ordinary natural division suffices.

Replacing a quotient pair by any equal integer preserves the exact floor equation and the same strict remainder.

The constructed floor quotient has an actual canonical historic signed-integer code, with its normalized decoder witnesses.

Every canonical signed integer has a canonical floor quotient and a witnessed strict natural remainder for every positive divisor.

Construct the actual natural square of every represented integer from its witnessed absolute difference.

The actual nonnegative square of a signed pair is unique by cancellative natural arithmetic.

Negating an arbitrary signed representative leaves its actual square unchanged.

Squaring respects equality of represented integers, not equality of positive and negative components.

The positive square block of an actual signed product expands into its two positive convolution blocks.

The negative square block of an actual signed product expands into the two negative convolution blocks.

Two actual nonnegative signed gaps multiply with an exact, subtraction-free compensation identity.

The actual square of a signed product is the product of its two actual natural squares.

Positive square expansion for the sum of two genuine signed pairs.

Negative square expansion for the sum of two genuine signed pairs.

Exact signed cross-term compensation for a squared sum, with no unproved norm premise.

Exact signed cross-term compensation for a squared difference; sign reversal preserves the same actual square.

Every signed Gaussian coordinate pair has a constructed actual nonnegative squared norm.

The squared Gaussian norm is functional across every possible square-witness choice.

Actual signed-product positive components permit interchange of the first two factors, by ordinary semiring certificates.

Actual signed-product negative components permit interchange of the first two factors, by ordinary semiring certificates.

The two actual signed product components are commutative, before any quotient normalization.

Four actual signed factors admit the exact middle-factor interchange, assembled from checked associative and commutative components.

The actual cross products (ac)(bd) and (ad)(bc) agree in both signed components.

Lagrange cancellation for two signed squared coordinates, with exact cross-product equations and all four actual scalar squares.

The actual squared Gaussian norm is multiplicative for arbitrary signed representatives, by checked two-coordinate Lagrange cancellation.

The actual Gaussian norm is invariant under equality of both represented integer coordinates.

Complex conjugation preserves the actual squared Gaussian norm, for every signed representative.

A genuine natural signed square is zero exactly when the represented integer is zero.

Every nonzero represented Gaussian integer has an actually positive natural norm.

Scaling a genuine signed pair by any natural multiplies its actual square by the scalar square, including zero.

Exact real positive component associativity for the actual four-component Gaussian product.

Exact real negative component associativity for the actual four-component Gaussian product.

Exact imaginary positive component associativity for the actual four-component Gaussian product.

Exact imaginary negative component associativity for the actual four-component Gaussian product.

Exact real positive component distributivity over a genuine signed Gaussian difference.

Exact real negative component distributivity over a genuine signed Gaussian difference.

Exact imaginary positive component distributivity over a genuine signed Gaussian difference.

Exact imaginary negative component distributivity over a genuine signed Gaussian difference.

The actual Gaussian product is associative in represented integer coordinates.

The actual Gaussian product distributes over subtraction in represented integer coordinates.

Represented Gaussian integer equality is reflexive.

Represented Gaussian integer equality is symmetric.

Represented Gaussian integer equality is transitive by actual signed cross-sum cancellation.

The actual Gaussian multiplication preserves equality of represented integers in both operands.

Actual Gaussian subtraction preserves integer representative equivalence in both operands.

An actual Gaussian norm is exactly the difference of its positive-square and negative-cross blocks.

Multiplication by the genuine complex conjugate produces the actual natural norm with zero imaginary coordinate.

Gaussian multiplication by a natural real scalar is actual coordinatewise natural scaling.

The actual conjugate times a Gaussian product equals the genuine norm-scaled second factor.

For the actual residual a-bq, multiplication by the conjugate divisor gives exactly the rounded numerator error a*conjugate(b)-N(b)q.

Adding a Gaussian subtrahend to its actual signed residual reconstructs the dividend in both integer coordinates.

Every nonzero natural has an explicit strict-positive gap witness.

Twice the square of a positive natural is strictly smaller than the square of its double.

For every positive modulus, any half-size magnitude has twice-square strictly below the full modulus square, including magnitude zero.

The sum of two genuinely half-bounded coordinate squares is strictly below the positive modulus square; no parity or positive-remainder assumption is needed.

Construct an actual nearest signed quotient, signed error, and half-bounded magnitude from one floor division and the checked centered natural remainder constructor.

Construct a genuine Gaussian quotient and remainder with exact a=bq+r and strict norm decrease for every nonzero divisor; neither quotients nor a remainder bound are assumed.

The unchanged canonical signed code continues to represent every equal signed difference.

Two signed pairs represented by the same historic canonical integer code are genuinely equal integers.

Pair two actual normalized signed-integer codes into their genuine canonical natural Gaussian coordinate code.

A canonical Gaussian coordinate code has exactly one normalized four-component signed decoding.

Every pair of arbitrary represented integers has an actually constructed canonical natural Gaussian code.

The canonical Gaussian natural code representing two specified integer differences is unique.

A canonical Gaussian coordinate code is invariant under arbitrary equal signed representatives.

Any two signed representatives of the same canonical Gaussian natural code denote the same Gaussian integer.

Every possibly overlapping signed representation yields actual unique normalized decoder coordinates of the same canonical code.

Every normalized Gaussian decoding also represents its two actual integer coordinates.

A genuinely represented pair always belongs to the canonical signed-coordinate Gaussian carrier.

The zero canonical pair code has exactly zero real and imaginary signed codes.

A canonical signed-coordinate pair is zero exactly when both represented integer differences vanish, even for overlapping raw representatives.

The unchanged normalized signed-coordinate decoding detects the zero pair code in both directions.

Actual arbitrary signed-pair add contribution balances construct the unchanged historic canonical signed-add graph.

The unchanged historic signed-add graph has the exact arbitrary-representative contribution balance; this proves the converse rather than an unproved notation alias.

Actual arbitrary signed-pair mul contribution balances construct the unchanged historic canonical signed-mul graph.

The unchanged historic signed-mul graph has the exact arbitrary-representative contribution balance; this proves the converse rather than an unproved notation alias.

An actual represented pair and its actual squared modulus construct the canonical Gaussian norm graph.

The canonical norm is the actual squared modulus of every equal signed representative, not merely its selected witness.

Construct the actual natural squared norm of every canonical Gaussian integer, with zero and units included.

The actual canonical Gaussian squared norm is unique across all arbitrary signed representatives.

Every canonical Gaussian integer has one genuinely constructed and uniquely determined natural squared norm.

Actual complex addition respects represented integer equality in both coordinates and both inputs.

Actual signed-coordinate add representatives construct the canonical Gaussian operation graph.

The canonical Gaussian add graph agrees with actual arithmetic on every chosen integer representative.

Construct an actual canonical Gaussian add output for every pair of valid canonical Gaussian inputs.

Actual Gaussian add has one literal canonical natural output code, independent of all representative choices.

Actual signed-coordinate multiply representatives construct the canonical Gaussian operation graph.

The canonical Gaussian multiply graph agrees with actual arithmetic on every chosen integer representative.

Construct an actual canonical Gaussian multiply output for every pair of valid canonical Gaussian inputs.

Actual Gaussian multiply has one literal canonical natural output code, independent of all representative choices.

The actual squared norm of a canonical Gaussian product equals the product of its actual natural squared norms.

The actual arbitrary signed-coordinate equation a=bq+r yields the genuine canonical Gaussian multiplication-and-addition graph.

Full constructive Gaussian Euclidean division: every canonical dividend and nonzero canonical divisor produce actual canonical quotient and remainder codes satisfying a=bq+r and strict decrease of their actual squared norms.