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_reflexive_domain ge_real_negative_reflexive_domain ge_imaginary_positive_reflexive_domain ge_imaginary_negative_reflexive_domain. (exists ge_real_code_reflexive_domaindecode ge_imaginary_code_reflexive_domaindecode. (((z) = ((ge_real_code_reflexive_domaindecode) + (ge_imaginary_code_reflexive_domaindecode)) * S ((ge_real_code_reflexive_domaindecode) + (ge_imaginary_code_reflexive_domaindecode)) + ((ge_imaginary_code_reflexive_domaindecode) + (ge_imaginary_code_reflexive_domaindecode))) /\ (((((ge_real_code_reflexive_domaindecode) = 2 * (ge_real_positive_reflexive_domain) /\ (ge_real_negative_reflexive_domain) = 0) \/ exists ge_signed_half_ge_reflexive_domaindecode_real. (((ge_real_code_reflexive_domaindecode) = 2 * ge_signed_half_ge_reflexive_domaindecode_real + 1 /\ (ge_real_positive_reflexive_domain) = 0) /\ (ge_real_negative_reflexive_domain) = S ge_signed_half_ge_reflexive_domaindecode_real))) /\ ((((ge_imaginary_code_reflexive_domaindecode) = 2 * (ge_imaginary_positive_reflexive_domain) /\ (ge_imaginary_negative_reflexive_domain) = 0) \/ exists ge_signed_half_ge_reflexive_domaindecode_imaginary. (((ge_imaginary_code_reflexive_domaindecode) = 2 * ge_signed_half_ge_reflexive_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_reflexive_domain) = 0) /\ (ge_imaginary_negative_reflexive_domain) = S ge_signed_half_ge_reflexive_domaindecode_imaginary))))))) -> (exists gr_quotient_reflexive_division. (exists ge_first_rp_reflexive_divisionproduct ge_first_rn_reflexive_divisionproduct ge_first_ip_reflexive_divisionproduct ge_first_in_reflexive_divisionproduct ge_second_rp_reflexive_divisionproduct ge_second_rn_reflexive_divisionproduct ge_second_ip_reflexive_divisionproduct ge_second_in_reflexive_divisionproduct. ((exists ge_representation_real_code_reflexive_divisionproductfirst ge_representation_imaginary_code_reflexive_divisionproductfirst. (((z) = ((ge_representation_real_code_reflexive_divisionproductfirst) + (ge_representation_imaginary_code_reflexive_divisionproductfirst)) * S ((ge_representation_real_code_reflexive_divisionproductfirst) + (ge_representation_imaginary_code_reflexive_divisionproductfirst)) + ((ge_representation_imaginary_code_reflexive_divisionproductfirst) + (ge_representation_imaginary_code_reflexive_divisionproductfirst))) /\ ((exists ge_balance_positive_reflexive_divisionproductfirstreal ge_balance_negative_reflexive_divisionproductfirstreal. (((((ge_representation_real_code_reflexive_divisionproductfirst) = 2 * (ge_balance_positive_reflexive_divisionproductfirstreal) /\ (ge_balance_negative_reflexive_divisionproductfirstreal) = 0) \/ exists ge_signed_half_reflexive_divisionproductfirstrealdecode. (((ge_representation_real_code_reflexive_divisionproductfirst) = 2 * ge_signed_half_reflexive_divisionproductfirstrealdecode + 1 /\ (ge_balance_positive_reflexive_divisionproductfirstreal) = 0) /\ (ge_balance_negative_reflexive_divisionproductfirstreal) = S ge_signed_half_reflexive_divisionproductfirstrealdecode))) /\ ((ge_first_rp_reflexive_divisionproduct) + ge_balance_negative_reflexive_divisionproductfirstreal = (ge_first_rn_reflexive_divisionproduct) + ge_balance_positive_reflexive_divisionproductfirstreal))) /\ (exists ge_balance_positive_reflexive_divisionproductfirstimaginary ge_balance_negative_reflexive_divisionproductfirstimaginary. (((((ge_representation_imaginary_code_reflexive_divisionproductfirst) = 2 * (ge_balance_positive_reflexive_divisionproductfirstimaginary) /\ (ge_balance_negative_reflexive_divisionproductfirstimaginary) = 0) \/ exists ge_signed_half_reflexive_divisionproductfirstimaginarydecode. (((ge_representation_imaginary_code_reflexive_divisionproductfirst) = 2 * ge_signed_half_reflexive_divisionproductfirstimaginarydecode + 1 /\ (ge_balance_positive_reflexive_divisionproductfirstimaginary) = 0) /\ (ge_balance_negative_reflexive_divisionproductfirstimaginary) = S ge_signed_half_reflexive_divisionproductfirstimaginarydecode))) /\ ((ge_first_ip_reflexive_divisionproduct) + ge_balance_negative_reflexive_divisionproductfirstimaginary = (ge_first_in_reflexive_divisionproduct) + ge_balance_positive_reflexive_divisionproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_reflexive_divisionproductsecond ge_representation_imaginary_code_reflexive_divisionproductsecond. (((gr_quotient_reflexive_division) = ((ge_representation_real_code_reflexive_divisionproductsecond) + (ge_representation_imaginary_code_reflexive_divisionproductsecond)) * S ((ge_representation_real_code_reflexive_divisionproductsecond) + (ge_representation_imaginary_code_reflexive_divisionproductsecond)) + ((ge_representation_imaginary_code_reflexive_divisionproductsecond) + (ge_representation_imaginary_code_reflexive_divisionproductsecond))) /\ ((exists ge_balance_positive_reflexive_divisionproductsecondreal ge_balance_negative_reflexive_divisionproductsecondreal. (((((ge_representation_real_code_reflexive_divisionproductsecond) = 2 * (ge_balance_positive_reflexive_divisionproductsecondreal) /\ (ge_balance_negative_reflexive_divisionproductsecondreal) = 0) \/ exists ge_signed_half_reflexive_divisionproductsecondrealdecode. (((ge_representation_real_code_reflexive_divisionproductsecond) = 2 * ge_signed_half_reflexive_divisionproductsecondrealdecode + 1 /\ (ge_balance_positive_reflexive_divisionproductsecondreal) = 0) /\ (ge_balance_negative_reflexive_divisionproductsecondreal) = S ge_signed_half_reflexive_divisionproductsecondrealdecode))) /\ ((ge_second_rp_reflexive_divisionproduct) + ge_balance_negative_reflexive_divisionproductsecondreal = (ge_second_rn_reflexive_divisionproduct) + ge_balance_positive_reflexive_divisionproductsecondreal))) /\ (exists ge_balance_positive_reflexive_divisionproductsecondimaginary ge_balance_negative_reflexive_divisionproductsecondimaginary. (((((ge_representation_imaginary_code_reflexive_divisionproductsecond) = 2 * (ge_balance_positive_reflexive_divisionproductsecondimaginary) /\ (ge_balance_negative_reflexive_divisionproductsecondimaginary) = 0) \/ exists ge_signed_half_reflexive_divisionproductsecondimaginarydecode. (((ge_representation_imaginary_code_reflexive_divisionproductsecond) = 2 * ge_signed_half_reflexive_divisionproductsecondimaginarydecode + 1 /\ (ge_balance_positive_reflexive_divisionproductsecondimaginary) = 0) /\ (ge_balance_negative_reflexive_divisionproductsecondimaginary) = S ge_signed_half_reflexive_divisionproductsecondimaginarydecode))) /\ ((ge_second_ip_reflexive_divisionproduct) + ge_balance_negative_reflexive_divisionproductsecondimaginary = (ge_second_in_reflexive_divisionproduct) + ge_balance_positive_reflexive_divisionproductsecondimaginary)))))) /\ (exists ge_representation_real_code_reflexive_divisionproductoutput ge_representation_imaginary_code_reflexive_divisionproductoutput. (((z) = ((ge_representation_real_code_reflexive_divisionproductoutput) + (ge_representation_imaginary_code_reflexive_divisionproductoutput)) * S ((ge_representation_real_code_reflexive_divisionproductoutput) + (ge_representation_imaginary_code_reflexive_divisionproductoutput)) + ((ge_representation_imaginary_code_reflexive_divisionproductoutput) + (ge_representation_imaginary_code_reflexive_divisionproductoutput))) /\ ((exists ge_balance_positive_reflexive_divisionproductoutputreal ge_balance_negative_reflexive_divisionproductoutputreal. (((((ge_representation_real_code_reflexive_divisionproductoutput) = 2 * (ge_balance_positive_reflexive_divisionproductoutputreal) /\ (ge_balance_negative_reflexive_divisionproductoutputreal) = 0) \/ exists ge_signed_half_reflexive_divisionproductoutputrealdecode. (((ge_representation_real_code_reflexive_divisionproductoutput) = 2 * ge_signed_half_reflexive_divisionproductoutputrealdecode + 1 /\ (ge_balance_positive_reflexive_divisionproductoutputreal) = 0) /\ (ge_balance_negative_reflexive_divisionproductoutputreal) = S ge_signed_half_reflexive_divisionproductoutputrealdecode))) /\ ((((((((ge_first_rp_reflexive_divisionproduct) * (ge_second_rp_reflexive_divisionproduct))) + (((ge_first_rn_reflexive_divisionproduct) * (ge_second_rn_reflexive_divisionproduct))))) + (((((ge_first_ip_reflexive_divisionproduct) * (ge_second_in_reflexive_divisionproduct))) + (((ge_first_in_reflexive_divisionproduct) * (ge_second_ip_reflexive_divisionproduct))))))) + ge_balance_negative_reflexive_divisionproductoutputreal = (((((((ge_first_rp_reflexive_divisionproduct) * (ge_second_rn_reflexive_divisionproduct))) + (((ge_first_rn_reflexive_divisionproduct) * (ge_second_rp_reflexive_divisionproduct))))) + (((((ge_first_ip_reflexive_divisionproduct) * (ge_second_ip_reflexive_divisionproduct))) + (((ge_first_in_reflexive_divisionproduct) * (ge_second_in_reflexive_divisionproduct))))))) + ge_balance_positive_reflexive_divisionproductoutputreal))) /\ (exists ge_balance_positive_reflexive_divisionproductoutputimaginary ge_balance_negative_reflexive_divisionproductoutputimaginary. (((((ge_representation_imaginary_code_reflexive_divisionproductoutput) = 2 * (ge_balance_positive_reflexive_divisionproductoutputimaginary) /\ (ge_balance_negative_reflexive_divisionproductoutputimaginary) = 0) \/ exists ge_signed_half_reflexive_divisionproductoutputimaginarydecode. (((ge_representation_imaginary_code_reflexive_divisionproductoutput) = 2 * ge_signed_half_reflexive_divisionproductoutputimaginarydecode + 1 /\ (ge_balance_positive_reflexive_divisionproductoutputimaginary) = 0) /\ (ge_balance_negative_reflexive_divisionproductoutputimaginary) = S ge_signed_half_reflexive_divisionproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_reflexive_divisionproduct) * (ge_second_ip_reflexive_divisionproduct))) + (((ge_first_rn_reflexive_divisionproduct) * (ge_second_in_reflexive_divisionproduct))))) + (((((ge_first_ip_reflexive_divisionproduct) * (ge_second_rp_reflexive_divisionproduct))) + (((ge_first_in_reflexive_divisionproduct) * (ge_second_rn_reflexive_divisionproduct))))))) + ge_balance_negative_reflexive_divisionproductoutputimaginary = (((((((ge_first_rp_reflexive_divisionproduct) * (ge_second_in_reflexive_divisionproduct))) + (((ge_first_rn_reflexive_divisionproduct) * (ge_second_ip_reflexive_divisionproduct))))) + (((((ge_first_ip_reflexive_divisionproduct) * (ge_second_rn_reflexive_divisionproduct))) + (((ge_first_in_reflexive_divisionproduct) * (ge_second_rp_reflexive_divisionproduct))))))) + ge_balance_positive_reflexive_divisionproductoutputimaginary))))))))))Constructive proof overview
Generated structural guide
Each actual Gaussian integer divides itself with canonical quotient six, the Gaussian identity.
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 (6)
Original exact command ledger · 6 lines
- 0001
intro z - 0002
intro h - 0003
exists (6) - 0004
specialize gaussian_multiply_one_right (z) - 0005
apply gaussian_multiply_one_right - 0006
exact h