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 expanded first-order arithmetic 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))))))))))Constructive proof overview
Generated structural guide
Each actual Gaussian integer divides zero with its actual zero quotient.
The unchanged tactic script uses 1 declared prerequisite and contains 6 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.
Named ingredients (1)
01Fix variables and assumptionsL1–2
02Construct an explicit witnessL3–3
Supply the displayed value, then prove that it has the required property.
- L3
exists (0)
Original exact command ledger · 6 lines
- 0001
intro z - 0002
intro h - 0003
exists (0) - 0004
specialize gaussian_multiply_zero_right (z) - 0005
apply gaussian_multiply_zero_right - 0006
exact h