GF0045

gaussian_divides_zero

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

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

∀ z. ZPairValid(z) → GDvd(z,0)

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

Definition DAG

ZPairValid(z) · 1GDvd(d,z) · 1

Actual proof prerequisites

gaussian_multiply_zero_right
Original expanded first-order statement 
forall z. (exists ge_real_positive_divides_zero_domain ge_real_negative_divides_zero_domain ge_imaginary_positive_divides_zero_domain ge_imaginary_negative_divides_zero_domain. (exists ge_real_code_divides_zero_domaindecode ge_imaginary_code_divides_zero_domaindecode. (((z) = ((ge_real_code_divides_zero_domaindecode) + (ge_imaginary_code_divides_zero_domaindecode)) * S ((ge_real_code_divides_zero_domaindecode) + (ge_imaginary_code_divides_zero_domaindecode)) + ((ge_imaginary_code_divides_zero_domaindecode) + (ge_imaginary_code_divides_zero_domaindecode))) /\ (((((ge_real_code_divides_zero_domaindecode) = 2 * (ge_real_positive_divides_zero_domain) /\ (ge_real_negative_divides_zero_domain) = 0) \/ exists ge_signed_half_ge_divides_zero_domaindecode_real. (((ge_real_code_divides_zero_domaindecode) = 2 * ge_signed_half_ge_divides_zero_domaindecode_real + 1 /\ (ge_real_positive_divides_zero_domain) = 0) /\ (ge_real_negative_divides_zero_domain) = S ge_signed_half_ge_divides_zero_domaindecode_real))) /\ ((((ge_imaginary_code_divides_zero_domaindecode) = 2 * (ge_imaginary_positive_divides_zero_domain) /\ (ge_imaginary_negative_divides_zero_domain) = 0) \/ exists ge_signed_half_ge_divides_zero_domaindecode_imaginary. (((ge_imaginary_code_divides_zero_domaindecode) = 2 * ge_signed_half_ge_divides_zero_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_divides_zero_domain) = 0) /\ (ge_imaginary_negative_divides_zero_domain) = S ge_signed_half_ge_divides_zero_domaindecode_imaginary))))))) -> (exists gr_quotient_divides_zero. (exists ge_first_rp_divides_zeroproduct ge_first_rn_divides_zeroproduct ge_first_ip_divides_zeroproduct ge_first_in_divides_zeroproduct ge_second_rp_divides_zeroproduct ge_second_rn_divides_zeroproduct ge_second_ip_divides_zeroproduct ge_second_in_divides_zeroproduct. ((exists ge_representation_real_code_divides_zeroproductfirst ge_representation_imaginary_code_divides_zeroproductfirst. (((z) = ((ge_representation_real_code_divides_zeroproductfirst) + (ge_representation_imaginary_code_divides_zeroproductfirst)) * S ((ge_representation_real_code_divides_zeroproductfirst) + (ge_representation_imaginary_code_divides_zeroproductfirst)) + ((ge_representation_imaginary_code_divides_zeroproductfirst) + (ge_representation_imaginary_code_divides_zeroproductfirst))) /\ ((exists ge_balance_positive_divides_zeroproductfirstreal ge_balance_negative_divides_zeroproductfirstreal. (((((ge_representation_real_code_divides_zeroproductfirst) = 2 * (ge_balance_positive_divides_zeroproductfirstreal) /\ (ge_balance_negative_divides_zeroproductfirstreal) = 0) \/ exists ge_signed_half_divides_zeroproductfirstrealdecode. (((ge_representation_real_code_divides_zeroproductfirst) = 2 * ge_signed_half_divides_zeroproductfirstrealdecode + 1 /\ (ge_balance_positive_divides_zeroproductfirstreal) = 0) /\ (ge_balance_negative_divides_zeroproductfirstreal) = S ge_signed_half_divides_zeroproductfirstrealdecode))) /\ ((ge_first_rp_divides_zeroproduct) + ge_balance_negative_divides_zeroproductfirstreal = (ge_first_rn_divides_zeroproduct) + ge_balance_positive_divides_zeroproductfirstreal))) /\ (exists ge_balance_positive_divides_zeroproductfirstimaginary ge_balance_negative_divides_zeroproductfirstimaginary. (((((ge_representation_imaginary_code_divides_zeroproductfirst) = 2 * (ge_balance_positive_divides_zeroproductfirstimaginary) /\ (ge_balance_negative_divides_zeroproductfirstimaginary) = 0) \/ exists ge_signed_half_divides_zeroproductfirstimaginarydecode. (((ge_representation_imaginary_code_divides_zeroproductfirst) = 2 * ge_signed_half_divides_zeroproductfirstimaginarydecode + 1 /\ (ge_balance_positive_divides_zeroproductfirstimaginary) = 0) /\ (ge_balance_negative_divides_zeroproductfirstimaginary) = S ge_signed_half_divides_zeroproductfirstimaginarydecode))) /\ ((ge_first_ip_divides_zeroproduct) + ge_balance_negative_divides_zeroproductfirstimaginary = (ge_first_in_divides_zeroproduct) + ge_balance_positive_divides_zeroproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_divides_zeroproductsecond ge_representation_imaginary_code_divides_zeroproductsecond. (((gr_quotient_divides_zero) = ((ge_representation_real_code_divides_zeroproductsecond) + (ge_representation_imaginary_code_divides_zeroproductsecond)) * S ((ge_representation_real_code_divides_zeroproductsecond) + (ge_representation_imaginary_code_divides_zeroproductsecond)) + ((ge_representation_imaginary_code_divides_zeroproductsecond) + (ge_representation_imaginary_code_divides_zeroproductsecond))) /\ ((exists ge_balance_positive_divides_zeroproductsecondreal ge_balance_negative_divides_zeroproductsecondreal. (((((ge_representation_real_code_divides_zeroproductsecond) = 2 * (ge_balance_positive_divides_zeroproductsecondreal) /\ (ge_balance_negative_divides_zeroproductsecondreal) = 0) \/ exists ge_signed_half_divides_zeroproductsecondrealdecode. (((ge_representation_real_code_divides_zeroproductsecond) = 2 * ge_signed_half_divides_zeroproductsecondrealdecode + 1 /\ (ge_balance_positive_divides_zeroproductsecondreal) = 0) /\ (ge_balance_negative_divides_zeroproductsecondreal) = S ge_signed_half_divides_zeroproductsecondrealdecode))) /\ ((ge_second_rp_divides_zeroproduct) + ge_balance_negative_divides_zeroproductsecondreal = (ge_second_rn_divides_zeroproduct) + ge_balance_positive_divides_zeroproductsecondreal))) /\ (exists ge_balance_positive_divides_zeroproductsecondimaginary ge_balance_negative_divides_zeroproductsecondimaginary. (((((ge_representation_imaginary_code_divides_zeroproductsecond) = 2 * (ge_balance_positive_divides_zeroproductsecondimaginary) /\ (ge_balance_negative_divides_zeroproductsecondimaginary) = 0) \/ exists ge_signed_half_divides_zeroproductsecondimaginarydecode. (((ge_representation_imaginary_code_divides_zeroproductsecond) = 2 * ge_signed_half_divides_zeroproductsecondimaginarydecode + 1 /\ (ge_balance_positive_divides_zeroproductsecondimaginary) = 0) /\ (ge_balance_negative_divides_zeroproductsecondimaginary) = S ge_signed_half_divides_zeroproductsecondimaginarydecode))) /\ ((ge_second_ip_divides_zeroproduct) + ge_balance_negative_divides_zeroproductsecondimaginary = (ge_second_in_divides_zeroproduct) + ge_balance_positive_divides_zeroproductsecondimaginary)))))) /\ (exists ge_representation_real_code_divides_zeroproductoutput ge_representation_imaginary_code_divides_zeroproductoutput. (((0) = ((ge_representation_real_code_divides_zeroproductoutput) + (ge_representation_imaginary_code_divides_zeroproductoutput)) * S ((ge_representation_real_code_divides_zeroproductoutput) + (ge_representation_imaginary_code_divides_zeroproductoutput)) + ((ge_representation_imaginary_code_divides_zeroproductoutput) + (ge_representation_imaginary_code_divides_zeroproductoutput))) /\ ((exists ge_balance_positive_divides_zeroproductoutputreal ge_balance_negative_divides_zeroproductoutputreal. (((((ge_representation_real_code_divides_zeroproductoutput) = 2 * (ge_balance_positive_divides_zeroproductoutputreal) /\ (ge_balance_negative_divides_zeroproductoutputreal) = 0) \/ exists ge_signed_half_divides_zeroproductoutputrealdecode. (((ge_representation_real_code_divides_zeroproductoutput) = 2 * ge_signed_half_divides_zeroproductoutputrealdecode + 1 /\ (ge_balance_positive_divides_zeroproductoutputreal) = 0) /\ (ge_balance_negative_divides_zeroproductoutputreal) = S ge_signed_half_divides_zeroproductoutputrealdecode))) /\ ((((((((ge_first_rp_divides_zeroproduct) * (ge_second_rp_divides_zeroproduct))) + (((ge_first_rn_divides_zeroproduct) * (ge_second_rn_divides_zeroproduct))))) + (((((ge_first_ip_divides_zeroproduct) * (ge_second_in_divides_zeroproduct))) + (((ge_first_in_divides_zeroproduct) * (ge_second_ip_divides_zeroproduct))))))) + ge_balance_negative_divides_zeroproductoutputreal = (((((((ge_first_rp_divides_zeroproduct) * (ge_second_rn_divides_zeroproduct))) + (((ge_first_rn_divides_zeroproduct) * (ge_second_rp_divides_zeroproduct))))) + (((((ge_first_ip_divides_zeroproduct) * (ge_second_ip_divides_zeroproduct))) + (((ge_first_in_divides_zeroproduct) * (ge_second_in_divides_zeroproduct))))))) + ge_balance_positive_divides_zeroproductoutputreal))) /\ (exists ge_balance_positive_divides_zeroproductoutputimaginary ge_balance_negative_divides_zeroproductoutputimaginary. (((((ge_representation_imaginary_code_divides_zeroproductoutput) = 2 * (ge_balance_positive_divides_zeroproductoutputimaginary) /\ (ge_balance_negative_divides_zeroproductoutputimaginary) = 0) \/ exists ge_signed_half_divides_zeroproductoutputimaginarydecode. (((ge_representation_imaginary_code_divides_zeroproductoutput) = 2 * ge_signed_half_divides_zeroproductoutputimaginarydecode + 1 /\ (ge_balance_positive_divides_zeroproductoutputimaginary) = 0) /\ (ge_balance_negative_divides_zeroproductoutputimaginary) = S ge_signed_half_divides_zeroproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_divides_zeroproduct) * (ge_second_ip_divides_zeroproduct))) + (((ge_first_rn_divides_zeroproduct) * (ge_second_in_divides_zeroproduct))))) + (((((ge_first_ip_divides_zeroproduct) * (ge_second_rp_divides_zeroproduct))) + (((ge_first_in_divides_zeroproduct) * (ge_second_rn_divides_zeroproduct))))))) + ge_balance_negative_divides_zeroproductoutputimaginary = (((((((ge_first_rp_divides_zeroproduct) * (ge_second_in_divides_zeroproduct))) + (((ge_first_rn_divides_zeroproduct) * (ge_second_ip_divides_zeroproduct))))) + (((((ge_first_ip_divides_zeroproduct) * (ge_second_rn_divides_zeroproduct))) + (((ge_first_in_divides_zeroproduct) * (ge_second_rp_divides_zeroproduct))))))) + ge_balance_positive_divides_zeroproductoutputimaginary))))))))))

Complete tactic proof in conservative notation

All 6 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

6 script commands · 3 reading checkpoints · 0 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 (1)
gaussian multiply zero right
01Fix variables and assumptionsL1–2

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

  1. L1
    intro z
  2. L2
    intro h
02Construct an explicit witnessL3–3

Supply the displayed value, then prove that it has the required property.

  1. L3
    exists (0)
03Use earlier factsL4–6

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

  1. L4
    specialize gaussian_multiply_zero_right (z)
  2. L5
    apply gaussian_multiply_zero_right
  3. L6
    exact h

Library-wide reading audit

Original defined command ledger · 6 lines
  1. 0001intro z
  2. 0002intro h
  3. 0003exists (0)
  4. 0004specialize gaussian_multiply_zero_right (z)
  5. 0005apply gaussian_multiply_zero_right
  6. 0006exact h