Shared signed-pair carrier · explicit floor quotient · strict norm decrease · Constructive arithmetic

Constructive Eisenstein Euclidean division

a,b∈ℤ[ω], b≠0 ⇒ ∃q,r. a=bq+r ∧ N(r)<N(b)

Construct actual Eisenstein quotient and remainder codes in ℤ[ω], with ω²+ω+1=0 and the genuine norm a²−ab+b².

Open the definition-aware map Read the final theorem See campaign milestone G084

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 5414 native tactic lines and 308 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem EI0041 and follow only the lemmas and conservative definitions supporting eisenstein_euclidean_division_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G084 milestone → theorem and definition dependencies.
Major independently established statements: EI0036 eisenstein_norm_exists · EI0037 eisenstein_norm_functional · EI0039 eisenstein_add_exists · EI003D eisenstein_multiply_exists · EI003F eisenstein_norm_multiply · EI0041 eisenstein_euclidean_division_exists.
Independently verified Alpha v34 checked-use theorem family: 65 dependency-curried kernel-checked theorem bodies · 308 proof prerequisites · 17 linked definitions · 17 definition-dependency arrows · 5414 exact tactic lines · first admitted v28 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 862 bundle nodes; SHA-256 e56dda386bf60759d1bacda45417eacd7e6a67fd6e23799f002aac9964253ae1.
Exact mathematical boundary: A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.