GF001F

gaussian_multiply_zero_implies_zero_factor

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

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. GMul(a,b,0) → a = 0 ∨ b = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GNorm(z,n) · 2GMul(a,b,c) · 1

Actual proof prerequisites

gaussian_norm_exists · checked external prerequisitegaussian_multiply_input_left_validgaussian_multiply_input_right_validgaussian_norm_functional · checked external prerequisitegaussian_norm_multiply · checked external prerequisitegaussian_zero_normmul_eq_zero · checked external prerequisitegaussian_norm_zero_implies_code_zerogaussian_norm_value_transport
Original expanded first-order statement 
forall a b. (exists ge_first_rp_zero_product ge_first_rn_zero_product ge_first_ip_zero_product ge_first_in_zero_product ge_second_rp_zero_product ge_second_rn_zero_product ge_second_ip_zero_product ge_second_in_zero_product. ((exists ge_representation_real_code_zero_productfirst ge_representation_imaginary_code_zero_productfirst. (((a) = ((ge_representation_real_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst)) * S ((ge_representation_real_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst)) + ((ge_representation_imaginary_code_zero_productfirst) + (ge_representation_imaginary_code_zero_productfirst))) /\ ((exists ge_balance_positive_zero_productfirstreal ge_balance_negative_zero_productfirstreal. (((((ge_representation_real_code_zero_productfirst) = 2 * (ge_balance_positive_zero_productfirstreal) /\ (ge_balance_negative_zero_productfirstreal) = 0) \/ exists ge_signed_half_zero_productfirstrealdecode. (((ge_representation_real_code_zero_productfirst) = 2 * ge_signed_half_zero_productfirstrealdecode + 1 /\ (ge_balance_positive_zero_productfirstreal) = 0) /\ (ge_balance_negative_zero_productfirstreal) = S ge_signed_half_zero_productfirstrealdecode))) /\ ((ge_first_rp_zero_product) + ge_balance_negative_zero_productfirstreal = (ge_first_rn_zero_product) + ge_balance_positive_zero_productfirstreal))) /\ (exists ge_balance_positive_zero_productfirstimaginary ge_balance_negative_zero_productfirstimaginary. (((((ge_representation_imaginary_code_zero_productfirst) = 2 * (ge_balance_positive_zero_productfirstimaginary) /\ (ge_balance_negative_zero_productfirstimaginary) = 0) \/ exists ge_signed_half_zero_productfirstimaginarydecode. (((ge_representation_imaginary_code_zero_productfirst) = 2 * ge_signed_half_zero_productfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_productfirstimaginary) = 0) /\ (ge_balance_negative_zero_productfirstimaginary) = S ge_signed_half_zero_productfirstimaginarydecode))) /\ ((ge_first_ip_zero_product) + ge_balance_negative_zero_productfirstimaginary = (ge_first_in_zero_product) + ge_balance_positive_zero_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_productsecond ge_representation_imaginary_code_zero_productsecond. (((b) = ((ge_representation_real_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond)) * S ((ge_representation_real_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond)) + ((ge_representation_imaginary_code_zero_productsecond) + (ge_representation_imaginary_code_zero_productsecond))) /\ ((exists ge_balance_positive_zero_productsecondreal ge_balance_negative_zero_productsecondreal. (((((ge_representation_real_code_zero_productsecond) = 2 * (ge_balance_positive_zero_productsecondreal) /\ (ge_balance_negative_zero_productsecondreal) = 0) \/ exists ge_signed_half_zero_productsecondrealdecode. (((ge_representation_real_code_zero_productsecond) = 2 * ge_signed_half_zero_productsecondrealdecode + 1 /\ (ge_balance_positive_zero_productsecondreal) = 0) /\ (ge_balance_negative_zero_productsecondreal) = S ge_signed_half_zero_productsecondrealdecode))) /\ ((ge_second_rp_zero_product) + ge_balance_negative_zero_productsecondreal = (ge_second_rn_zero_product) + ge_balance_positive_zero_productsecondreal))) /\ (exists ge_balance_positive_zero_productsecondimaginary ge_balance_negative_zero_productsecondimaginary. (((((ge_representation_imaginary_code_zero_productsecond) = 2 * (ge_balance_positive_zero_productsecondimaginary) /\ (ge_balance_negative_zero_productsecondimaginary) = 0) \/ exists ge_signed_half_zero_productsecondimaginarydecode. (((ge_representation_imaginary_code_zero_productsecond) = 2 * ge_signed_half_zero_productsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_productsecondimaginary) = 0) /\ (ge_balance_negative_zero_productsecondimaginary) = S ge_signed_half_zero_productsecondimaginarydecode))) /\ ((ge_second_ip_zero_product) + ge_balance_negative_zero_productsecondimaginary = (ge_second_in_zero_product) + ge_balance_positive_zero_productsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_productoutput ge_representation_imaginary_code_zero_productoutput. (((0) = ((ge_representation_real_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput)) * S ((ge_representation_real_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput)) + ((ge_representation_imaginary_code_zero_productoutput) + (ge_representation_imaginary_code_zero_productoutput))) /\ ((exists ge_balance_positive_zero_productoutputreal ge_balance_negative_zero_productoutputreal. (((((ge_representation_real_code_zero_productoutput) = 2 * (ge_balance_positive_zero_productoutputreal) /\ (ge_balance_negative_zero_productoutputreal) = 0) \/ exists ge_signed_half_zero_productoutputrealdecode. (((ge_representation_real_code_zero_productoutput) = 2 * ge_signed_half_zero_productoutputrealdecode + 1 /\ (ge_balance_positive_zero_productoutputreal) = 0) /\ (ge_balance_negative_zero_productoutputreal) = S ge_signed_half_zero_productoutputrealdecode))) /\ ((((((((ge_first_rp_zero_product) * (ge_second_rp_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_rn_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_in_zero_product))) + (((ge_first_in_zero_product) * (ge_second_ip_zero_product))))))) + ge_balance_negative_zero_productoutputreal = (((((((ge_first_rp_zero_product) * (ge_second_rn_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_rp_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_ip_zero_product))) + (((ge_first_in_zero_product) * (ge_second_in_zero_product))))))) + ge_balance_positive_zero_productoutputreal))) /\ (exists ge_balance_positive_zero_productoutputimaginary ge_balance_negative_zero_productoutputimaginary. (((((ge_representation_imaginary_code_zero_productoutput) = 2 * (ge_balance_positive_zero_productoutputimaginary) /\ (ge_balance_negative_zero_productoutputimaginary) = 0) \/ exists ge_signed_half_zero_productoutputimaginarydecode. (((ge_representation_imaginary_code_zero_productoutput) = 2 * ge_signed_half_zero_productoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_productoutputimaginary) = 0) /\ (ge_balance_negative_zero_productoutputimaginary) = S ge_signed_half_zero_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_product) * (ge_second_ip_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_in_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_rp_zero_product))) + (((ge_first_in_zero_product) * (ge_second_rn_zero_product))))))) + ge_balance_negative_zero_productoutputimaginary = (((((((ge_first_rp_zero_product) * (ge_second_in_zero_product))) + (((ge_first_rn_zero_product) * (ge_second_ip_zero_product))))) + (((((ge_first_ip_zero_product) * (ge_second_rn_zero_product))) + (((ge_first_in_zero_product) * (ge_second_rp_zero_product))))))) + ge_balance_positive_zero_productoutputimaginary))))))))) -> a=0 \/ b=0

Complete tactic proof in conservative notation

All 60 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

60 script commands · 12 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
gaussian multiply input left validgaussian multiply input right validgaussian zero normgaussian norm zero implies code zerogaussian norm value transport
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Establish hAL4–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.

  1. L4
    have hA : ∃ N. GNorm(a,N)Definitions: GNorm(a,N)Original native command in the exact edition
  2. L5
    specialize gaussian_norm_exists (a)
  3. L6
    apply gaussian_norm_exists
  4. L7
    specialize gaussian_multiply_input_left_valid (a)
  5. L8
    specialize gaussian_multiply_input_left_valid (b)
  6. L9
    specialize gaussian_multiply_input_left_valid (0)
  7. L10
    apply gaussian_multiply_input_left_valid
  8. L11
    exact h
03Separate the logical casesL12–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hA
04Establish hBL13–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.

  1. L13
    have hB : ∃ M. GNorm(b,M)Definitions: GNorm(b,M)Original native command in the exact edition
  2. L14
    specialize gaussian_norm_exists (b)
  3. L15
    apply gaussian_norm_exists
  4. L16
    specialize gaussian_multiply_input_right_valid (a)
  5. L17
    specialize gaussian_multiply_input_right_valid (b)
  6. L18
    specialize gaussian_multiply_input_right_valid (0)
  7. L19
    apply gaussian_multiply_input_right_valid
  8. L20
    exact h
05Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hB
06Establish hpL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm functional.

  1. L22
    have hp : x*x1=0
  2. L23
    specialize gaussian_norm_functional (0)
  3. L24
    specialize gaussian_norm_functional (x*x1)
  4. L25
    specialize gaussian_norm_functional (0)
  5. L26
    apply gaussian_norm_functional
  6. L27
    specialize gaussian_norm_multiply (a)
  7. L28
    specialize gaussian_norm_multiply (b)
  8. L29
    specialize gaussian_norm_multiply (0)
  9. L30
    specialize gaussian_norm_multiply (x)
  10. L31
    specialize gaussian_norm_multiply (x1)
07Use earlier factsL32–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    apply gaussian_norm_multiply
  2. L33
    exact hA_witness
  3. L34
    exact hB_witness
  4. L35
    exact h
  5. L36
    exact gaussian_zero_norm
08Establish hcasesL37–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq zero.

  1. L37
    have hcases : x=0 \/ x1=0
  2. L38
    specialize mul_eq_zero (x)
  3. L39
    specialize mul_eq_zero (x1)
  4. L40
    apply mul_eq_zero
  5. L41
    exact hp
09Separate the logical casesL42–43

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L42
    cases hcases
  2. L43
    left
10Use earlier factsL44–51

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L44
    specialize gaussian_norm_zero_implies_code_zero (a)
  2. L45
    apply gaussian_norm_zero_implies_code_zero
  3. L46
    specialize gaussian_norm_value_transport (a)
  4. L47
    specialize gaussian_norm_value_transport (x)
  5. L48
    specialize gaussian_norm_value_transport (0)
  6. L49
    apply gaussian_norm_value_transport
  7. L50
    exact hcases_left
  8. L51
    exact hA_witness
11Separate the logical casesL52–52

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L52
    right
12Use earlier factsL53–60

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    specialize gaussian_norm_zero_implies_code_zero (b)
  2. L54
    apply gaussian_norm_zero_implies_code_zero
  3. L55
    specialize gaussian_norm_value_transport (b)
  4. L56
    specialize gaussian_norm_value_transport (x1)
  5. L57
    specialize gaussian_norm_value_transport (0)
  6. L58
    apply gaussian_norm_value_transport
  7. L59
    exact hcases_right
  8. L60
    exact hB_witness

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004have hA : ∃ N. GNorm(a,N)
  5. 0005specialize gaussian_norm_exists (a)
  6. 0006apply gaussian_norm_exists
  7. 0007specialize gaussian_multiply_input_left_valid (a)
  8. 0008specialize gaussian_multiply_input_left_valid (b)
  9. 0009specialize gaussian_multiply_input_left_valid (0)
  10. 0010apply gaussian_multiply_input_left_valid
  11. 0011exact h
  12. 0012cases hA
  13. 0013have hB : ∃ M. GNorm(b,M)
  14. 0014specialize gaussian_norm_exists (b)
  15. 0015apply gaussian_norm_exists
  16. 0016specialize gaussian_multiply_input_right_valid (a)
  17. 0017specialize gaussian_multiply_input_right_valid (b)
  18. 0018specialize gaussian_multiply_input_right_valid (0)
  19. 0019apply gaussian_multiply_input_right_valid
  20. 0020exact h
  21. 0021cases hB
  22. 0022have hp : x*x1=0
  23. 0023specialize gaussian_norm_functional (0)
  24. 0024specialize gaussian_norm_functional (x*x1)
  25. 0025specialize gaussian_norm_functional (0)
  26. 0026apply gaussian_norm_functional
  27. 0027specialize gaussian_norm_multiply (a)
  28. 0028specialize gaussian_norm_multiply (b)
  29. 0029specialize gaussian_norm_multiply (0)
  30. 0030specialize gaussian_norm_multiply (x)
  31. 0031specialize gaussian_norm_multiply (x1)
  32. 0032apply gaussian_norm_multiply
  33. 0033exact hA_witness
  34. 0034exact hB_witness
  35. 0035exact h
  36. 0036exact gaussian_zero_norm
  37. 0037have hcases : x=0 \/ x1=0
  38. 0038specialize mul_eq_zero (x)
  39. 0039specialize mul_eq_zero (x1)
  40. 0040apply mul_eq_zero
  41. 0041exact hp
  42. 0042cases hcases
  43. 0043left
  44. 0044specialize gaussian_norm_zero_implies_code_zero (a)
  45. 0045apply gaussian_norm_zero_implies_code_zero
  46. 0046specialize gaussian_norm_value_transport (a)
  47. 0047specialize gaussian_norm_value_transport (x)
  48. 0048specialize gaussian_norm_value_transport (0)
  49. 0049apply gaussian_norm_value_transport
  50. 0050exact hcases_left
  51. 0051exact hA_witness
  52. 0052right
  53. 0053specialize gaussian_norm_zero_implies_code_zero (b)
  54. 0054apply gaussian_norm_zero_implies_code_zero
  55. 0055specialize gaussian_norm_value_transport (b)
  56. 0056specialize gaussian_norm_value_transport (x1)
  57. 0057specialize gaussian_norm_value_transport (0)
  58. 0058apply gaussian_norm_value_transport
  59. 0059exact hcases_right
  60. 0060exact hB_witness