Constructive Eisenstein Euclidean division — Exact Proof Explorer

The natural-coordinate Eisenstein norm is symmetric in its two coordinates.

Ordering the coordinates gives the explicit subtraction-free norm a²+ad+d².

Every pair of natural coordinates has an actual natural Eisenstein norm, constructed by a decidable order comparison.

A zero Eisenstein norm forces both natural coordinates to vanish, including the diagonal boundary.

If a≤b then a²−ab+b²≤b², with an actual natural gap witness.

Every lattice residue pair 0≤a,b<m has norm strictly below m², including zero and a=b=m−1.

The subtraction-free signed-coordinate norm has a unique natural value.

Negating both genuine signed coordinates leaves the Eisenstein norm unchanged.

Every normalized signed-coordinate pair has an actual natural norm, in all four sign quadrants.

An equal signed-pair representative preserves the same natural value.

The norm depends only on the represented integers, not on a chosen positive/negative decomposition of either coordinate.

Every arbitrary signed-coordinate representation has a natural Eisenstein norm, by actual signed normalization and checked representative invariance.

Actual natural coordinate squares give the exact signed cross-term balance sa+sb=ENorm+ab.

The elementary compensation proves 4N=(2a-b)²+3b² without integer subtraction or an inequality assumption.

The actual signed square identity 4ENorm(a,b)=(2a-b)²+3b² holds for every signed representative.

Every genuine signed coordinate pair has a constructed positive-definite weight-three squared norm.

The weighted norm is a genuine functional arithmetic relation, independent of chosen square witnesses.

The exact linear embedding (a,b)↦(2a-b,b) has actual weight-three norm four times the Eisenstein norm.

The positive-definite weighted norm respects actual equality of both integer coordinates.

Scaling both actual integer coordinates multiplies the weighted norm by the exact natural square of the scale.

Scaling one genuine signed factor scales both exact natural product components.

A weight-three multiple of the summed-square equation cancels the exact difference-square cross terms.

Weighted Lagrange cancellation uses actual scalar squares and exact signed cross-component equations, with no norm oracle.

The actual positive weight-three norm is multiplicative under (x,y)(u,v)=(xu−3yv,xv+yu), for all arbitrary signed representatives.

The left associated Eisenstein real positive contribution is the checked Gaussian contribution plus the actual triple-imaginary contribution.

The left associated Eisenstein real negative contribution is the checked Gaussian contribution plus the actual triple-imaginary contribution.

The right associated Eisenstein real positive contribution is the checked Gaussian contribution plus the actual triple-imaginary contribution.

The right associated Eisenstein real negative contribution is the checked Gaussian contribution plus the actual triple-imaginary contribution.

Real Eisenstein associativity follows from checked Gaussian real associativity and associative scalar triple products, with all natural contribution equations explicit.

Exact real positive contribution of Eisenstein multiplication distributes over an actual signed difference.

Exact real negative contribution of Eisenstein multiplication distributes over an actual signed difference.

Exact imaginary positive contribution of Eisenstein multiplication distributes over an actual signed difference.

Exact imaginary negative contribution of Eisenstein multiplication distributes over an actual signed difference.

Actual Eisenstein multiplication distributes over signed subtraction in the second argument.

Eisenstein multiplication respects the represented integers in both inputs; overlapping natural representatives cause no ambiguity.

The genuine coordinate rotation for multiplication by ω commutes with right multiplication; this small bilinear identity recovers imaginary associativity from real associativity.

Imaginary Eisenstein associativity follows constructively from real associativity under the exact ω rotation, avoiding an oversized polynomial expansion.

Actual Eisenstein multiplication is associative on represented integer coordinates.

The actual Eisenstein conjugate (a-b)-bω has the same norm as a+bω for all signed representatives.

The actual product of an Eisenstein integer with its genuine conjugate is its natural norm plus zero times ω.

Multiplication by a natural real Eisenstein scalar is actual coordinatewise scaling.

The Eisenstein adjugate identity conjugate(a)*(a*b)=N(a)*b follows from checked coordinate associativity and the actual conjugate product.

Multiplying the actual residual a-bq by conjugate(b) yields exactly the numerator error conjugate(b)*a-N(b)*q.

Genuine Eisenstein multiplication is commutative on represented integer coordinates.

Actual Eisenstein conjugation preserves multiplication for all signed coordinate representatives.

The checked commutative Eisenstein product admits four-factor interchange without expanding a quartic polynomial.

The genuine Eisenstein norm is multiplicative, from checked conjugation, commutativity and associativity, without a norm or polynomial oracle.

A genuine Eisenstein norm can be zero only when both represented integer coordinates are zero, with no sign-normality or positivity hypothesis.

Every nonzero represented Eisenstein integer has a strictly positive natural norm.

The natural fundamental-parallelogram norm is exactly the signed-coordinate norm of the same nonnegative integers.

Construct a genuine Eisenstein quotient and remainder for every nonzero signed divisor, with exact a=bq+r and strict actual norm decrease; neither quotient, norm existence, nor a bound is supplied as a premise.

Actual signed coordinates and their actual norm construct the canonical Eisenstein norm graph.

The canonical Eisenstein norm equals the actual norm of every representative of the same pair of integers.

Every canonical Eisenstein integer has a genuinely constructed natural norm, including zero and all units.

The canonical natural Eisenstein norm is unique, independently of all signed-coordinate representatives.

Every valid canonical Eisenstein code has one actually computed and uniquely determined natural norm.

Eisenstein addition is exactly the shared neutral ZPair addition, with its already-checked constructive existence theorem.

The same canonical ZPair addition has one literal output code in the Eisenstein presentation; no duplicate additive definition is introduced.

The genuine signed-coordinate Eisenstein product constructs the exact canonical multiplication graph.

Every witness of canonical Eisenstein multiplication represents the same actual product of any chosen integer representatives.

Construct the actual canonical Eisenstein product of every two valid signed-coordinate codes.

Eisenstein multiplication has one literal canonical output code, not merely equivalent signed representatives.

The actual canonical Eisenstein norm of a product is exactly the product of the two actual natural norms.

An actual signed-coordinate a=bq+r equation constructs the genuine canonical Eisenstein product-and-sum graph.

Full constructive Eisenstein Euclidean division: every canonical dividend and nonzero canonical divisor produce actual canonical quotient and remainder, an exact a=bq+r equation, and strict decrease of their actual norms a²-ab+b².