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_one_divides_domain ge_real_negative_one_divides_domain ge_imaginary_positive_one_divides_domain ge_imaginary_negative_one_divides_domain. (exists ge_real_code_one_divides_domaindecode ge_imaginary_code_one_divides_domaindecode. (((z) = ((ge_real_code_one_divides_domaindecode) + (ge_imaginary_code_one_divides_domaindecode)) * S ((ge_real_code_one_divides_domaindecode) + (ge_imaginary_code_one_divides_domaindecode)) + ((ge_imaginary_code_one_divides_domaindecode) + (ge_imaginary_code_one_divides_domaindecode))) /\ (((((ge_real_code_one_divides_domaindecode) = 2 * (ge_real_positive_one_divides_domain) /\ (ge_real_negative_one_divides_domain) = 0) \/ exists ge_signed_half_ge_one_divides_domaindecode_real. (((ge_real_code_one_divides_domaindecode) = 2 * ge_signed_half_ge_one_divides_domaindecode_real + 1 /\ (ge_real_positive_one_divides_domain) = 0) /\ (ge_real_negative_one_divides_domain) = S ge_signed_half_ge_one_divides_domaindecode_real))) /\ ((((ge_imaginary_code_one_divides_domaindecode) = 2 * (ge_imaginary_positive_one_divides_domain) /\ (ge_imaginary_negative_one_divides_domain) = 0) \/ exists ge_signed_half_ge_one_divides_domaindecode_imaginary. (((ge_imaginary_code_one_divides_domaindecode) = 2 * ge_signed_half_ge_one_divides_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_one_divides_domain) = 0) /\ (ge_imaginary_negative_one_divides_domain) = S ge_signed_half_ge_one_divides_domaindecode_imaginary))))))) -> (exists gr_quotient_one_divides. (exists ge_first_rp_one_dividesproduct ge_first_rn_one_dividesproduct ge_first_ip_one_dividesproduct ge_first_in_one_dividesproduct ge_second_rp_one_dividesproduct ge_second_rn_one_dividesproduct ge_second_ip_one_dividesproduct ge_second_in_one_dividesproduct. ((exists ge_representation_real_code_one_dividesproductfirst ge_representation_imaginary_code_one_dividesproductfirst. (((6) = ((ge_representation_real_code_one_dividesproductfirst) + (ge_representation_imaginary_code_one_dividesproductfirst)) * S ((ge_representation_real_code_one_dividesproductfirst) + (ge_representation_imaginary_code_one_dividesproductfirst)) + ((ge_representation_imaginary_code_one_dividesproductfirst) + (ge_representation_imaginary_code_one_dividesproductfirst))) /\ ((exists ge_balance_positive_one_dividesproductfirstreal ge_balance_negative_one_dividesproductfirstreal. (((((ge_representation_real_code_one_dividesproductfirst) = 2 * (ge_balance_positive_one_dividesproductfirstreal) /\ (ge_balance_negative_one_dividesproductfirstreal) = 0) \/ exists ge_signed_half_one_dividesproductfirstrealdecode. (((ge_representation_real_code_one_dividesproductfirst) = 2 * ge_signed_half_one_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_one_dividesproductfirstreal) = 0) /\ (ge_balance_negative_one_dividesproductfirstreal) = S ge_signed_half_one_dividesproductfirstrealdecode))) /\ ((ge_first_rp_one_dividesproduct) + ge_balance_negative_one_dividesproductfirstreal = (ge_first_rn_one_dividesproduct) + ge_balance_positive_one_dividesproductfirstreal))) /\ (exists ge_balance_positive_one_dividesproductfirstimaginary ge_balance_negative_one_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_one_dividesproductfirst) = 2 * (ge_balance_positive_one_dividesproductfirstimaginary) /\ (ge_balance_negative_one_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_one_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_one_dividesproductfirst) = 2 * ge_signed_half_one_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_one_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_one_dividesproductfirstimaginary) = S ge_signed_half_one_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_one_dividesproduct) + ge_balance_negative_one_dividesproductfirstimaginary = (ge_first_in_one_dividesproduct) + ge_balance_positive_one_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_one_dividesproductsecond ge_representation_imaginary_code_one_dividesproductsecond. (((gr_quotient_one_divides) = ((ge_representation_real_code_one_dividesproductsecond) + (ge_representation_imaginary_code_one_dividesproductsecond)) * S ((ge_representation_real_code_one_dividesproductsecond) + (ge_representation_imaginary_code_one_dividesproductsecond)) + ((ge_representation_imaginary_code_one_dividesproductsecond) + (ge_representation_imaginary_code_one_dividesproductsecond))) /\ ((exists ge_balance_positive_one_dividesproductsecondreal ge_balance_negative_one_dividesproductsecondreal. (((((ge_representation_real_code_one_dividesproductsecond) = 2 * (ge_balance_positive_one_dividesproductsecondreal) /\ (ge_balance_negative_one_dividesproductsecondreal) = 0) \/ exists ge_signed_half_one_dividesproductsecondrealdecode. (((ge_representation_real_code_one_dividesproductsecond) = 2 * ge_signed_half_one_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_one_dividesproductsecondreal) = 0) /\ (ge_balance_negative_one_dividesproductsecondreal) = S ge_signed_half_one_dividesproductsecondrealdecode))) /\ ((ge_second_rp_one_dividesproduct) + ge_balance_negative_one_dividesproductsecondreal = (ge_second_rn_one_dividesproduct) + ge_balance_positive_one_dividesproductsecondreal))) /\ (exists ge_balance_positive_one_dividesproductsecondimaginary ge_balance_negative_one_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_one_dividesproductsecond) = 2 * (ge_balance_positive_one_dividesproductsecondimaginary) /\ (ge_balance_negative_one_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_one_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_one_dividesproductsecond) = 2 * ge_signed_half_one_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_one_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_one_dividesproductsecondimaginary) = S ge_signed_half_one_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_one_dividesproduct) + ge_balance_negative_one_dividesproductsecondimaginary = (ge_second_in_one_dividesproduct) + ge_balance_positive_one_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_one_dividesproductoutput ge_representation_imaginary_code_one_dividesproductoutput. (((z) = ((ge_representation_real_code_one_dividesproductoutput) + (ge_representation_imaginary_code_one_dividesproductoutput)) * S ((ge_representation_real_code_one_dividesproductoutput) + (ge_representation_imaginary_code_one_dividesproductoutput)) + ((ge_representation_imaginary_code_one_dividesproductoutput) + (ge_representation_imaginary_code_one_dividesproductoutput))) /\ ((exists ge_balance_positive_one_dividesproductoutputreal ge_balance_negative_one_dividesproductoutputreal. (((((ge_representation_real_code_one_dividesproductoutput) = 2 * (ge_balance_positive_one_dividesproductoutputreal) /\ (ge_balance_negative_one_dividesproductoutputreal) = 0) \/ exists ge_signed_half_one_dividesproductoutputrealdecode. (((ge_representation_real_code_one_dividesproductoutput) = 2 * ge_signed_half_one_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_one_dividesproductoutputreal) = 0) /\ (ge_balance_negative_one_dividesproductoutputreal) = S ge_signed_half_one_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_one_dividesproduct) * (ge_second_rp_one_dividesproduct))) + (((ge_first_rn_one_dividesproduct) * (ge_second_rn_one_dividesproduct))))) + (((((ge_first_ip_one_dividesproduct) * (ge_second_in_one_dividesproduct))) + (((ge_first_in_one_dividesproduct) * (ge_second_ip_one_dividesproduct))))))) + ge_balance_negative_one_dividesproductoutputreal = (((((((ge_first_rp_one_dividesproduct) * (ge_second_rn_one_dividesproduct))) + (((ge_first_rn_one_dividesproduct) * (ge_second_rp_one_dividesproduct))))) + (((((ge_first_ip_one_dividesproduct) * (ge_second_ip_one_dividesproduct))) + (((ge_first_in_one_dividesproduct) * (ge_second_in_one_dividesproduct))))))) + ge_balance_positive_one_dividesproductoutputreal))) /\ (exists ge_balance_positive_one_dividesproductoutputimaginary ge_balance_negative_one_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_one_dividesproductoutput) = 2 * (ge_balance_positive_one_dividesproductoutputimaginary) /\ (ge_balance_negative_one_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_one_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_one_dividesproductoutput) = 2 * ge_signed_half_one_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_one_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_one_dividesproductoutputimaginary) = S ge_signed_half_one_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_one_dividesproduct) * (ge_second_ip_one_dividesproduct))) + (((ge_first_rn_one_dividesproduct) * (ge_second_in_one_dividesproduct))))) + (((((ge_first_ip_one_dividesproduct) * (ge_second_rp_one_dividesproduct))) + (((ge_first_in_one_dividesproduct) * (ge_second_rn_one_dividesproduct))))))) + ge_balance_negative_one_dividesproductoutputimaginary = (((((((ge_first_rp_one_dividesproduct) * (ge_second_in_one_dividesproduct))) + (((ge_first_rn_one_dividesproduct) * (ge_second_ip_one_dividesproduct))))) + (((((ge_first_ip_one_dividesproduct) * (ge_second_rn_one_dividesproduct))) + (((ge_first_in_one_dividesproduct) * (ge_second_rp_one_dividesproduct))))))) + ge_balance_positive_one_dividesproductoutputimaginary))))))))))Constructive proof overview
Generated structural guide
The actual Gaussian identity divides every valid Gaussian integer.
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 (z)
Original exact command ledger · 6 lines
- 0001
intro z - 0002
intro h - 0003
exists (z) - 0004
specialize gaussian_multiply_one_left (z) - 0005
apply gaussian_multiply_one_left - 0006
exact h