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 gr_inverse_unit_nonzero. (exists ge_first_rp_unit_nonzeroidentity ge_first_rn_unit_nonzeroidentity ge_first_ip_unit_nonzeroidentity ge_first_in_unit_nonzeroidentity ge_second_rp_unit_nonzeroidentity ge_second_rn_unit_nonzeroidentity ge_second_ip_unit_nonzeroidentity ge_second_in_unit_nonzeroidentity. ((exists ge_representation_real_code_unit_nonzeroidentityfirst ge_representation_imaginary_code_unit_nonzeroidentityfirst. (((z) = ((ge_representation_real_code_unit_nonzeroidentityfirst) + (ge_representation_imaginary_code_unit_nonzeroidentityfirst)) * S ((ge_representation_real_code_unit_nonzeroidentityfirst) + (ge_representation_imaginary_code_unit_nonzeroidentityfirst)) + ((ge_representation_imaginary_code_unit_nonzeroidentityfirst) + (ge_representation_imaginary_code_unit_nonzeroidentityfirst))) /\ ((exists ge_balance_positive_unit_nonzeroidentityfirstreal ge_balance_negative_unit_nonzeroidentityfirstreal. (((((ge_representation_real_code_unit_nonzeroidentityfirst) = 2 * (ge_balance_positive_unit_nonzeroidentityfirstreal) /\ (ge_balance_negative_unit_nonzeroidentityfirstreal) = 0) \/ exists ge_signed_half_unit_nonzeroidentityfirstrealdecode. (((ge_representation_real_code_unit_nonzeroidentityfirst) = 2 * ge_signed_half_unit_nonzeroidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_nonzeroidentityfirstreal) = 0) /\ (ge_balance_negative_unit_nonzeroidentityfirstreal) = S ge_signed_half_unit_nonzeroidentityfirstrealdecode))) /\ ((ge_first_rp_unit_nonzeroidentity) + ge_balance_negative_unit_nonzeroidentityfirstreal = (ge_first_rn_unit_nonzeroidentity) + ge_balance_positive_unit_nonzeroidentityfirstreal))) /\ (exists ge_balance_positive_unit_nonzeroidentityfirstimaginary ge_balance_negative_unit_nonzeroidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_nonzeroidentityfirst) = 2 * (ge_balance_positive_unit_nonzeroidentityfirstimaginary) /\ (ge_balance_negative_unit_nonzeroidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_nonzeroidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_nonzeroidentityfirst) = 2 * ge_signed_half_unit_nonzeroidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_nonzeroidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_nonzeroidentityfirstimaginary) = S ge_signed_half_unit_nonzeroidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_nonzeroidentity) + ge_balance_negative_unit_nonzeroidentityfirstimaginary = (ge_first_in_unit_nonzeroidentity) + ge_balance_positive_unit_nonzeroidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_nonzeroidentitysecond ge_representation_imaginary_code_unit_nonzeroidentitysecond. (((gr_inverse_unit_nonzero) = ((ge_representation_real_code_unit_nonzeroidentitysecond) + (ge_representation_imaginary_code_unit_nonzeroidentitysecond)) * S ((ge_representation_real_code_unit_nonzeroidentitysecond) + (ge_representation_imaginary_code_unit_nonzeroidentitysecond)) + ((ge_representation_imaginary_code_unit_nonzeroidentitysecond) + (ge_representation_imaginary_code_unit_nonzeroidentitysecond))) /\ ((exists ge_balance_positive_unit_nonzeroidentitysecondreal ge_balance_negative_unit_nonzeroidentitysecondreal. (((((ge_representation_real_code_unit_nonzeroidentitysecond) = 2 * (ge_balance_positive_unit_nonzeroidentitysecondreal) /\ (ge_balance_negative_unit_nonzeroidentitysecondreal) = 0) \/ exists ge_signed_half_unit_nonzeroidentitysecondrealdecode. (((ge_representation_real_code_unit_nonzeroidentitysecond) = 2 * ge_signed_half_unit_nonzeroidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_nonzeroidentitysecondreal) = 0) /\ (ge_balance_negative_unit_nonzeroidentitysecondreal) = S ge_signed_half_unit_nonzeroidentitysecondrealdecode))) /\ ((ge_second_rp_unit_nonzeroidentity) + ge_balance_negative_unit_nonzeroidentitysecondreal = (ge_second_rn_unit_nonzeroidentity) + ge_balance_positive_unit_nonzeroidentitysecondreal))) /\ (exists ge_balance_positive_unit_nonzeroidentitysecondimaginary ge_balance_negative_unit_nonzeroidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_nonzeroidentitysecond) = 2 * (ge_balance_positive_unit_nonzeroidentitysecondimaginary) /\ (ge_balance_negative_unit_nonzeroidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_nonzeroidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_nonzeroidentitysecond) = 2 * ge_signed_half_unit_nonzeroidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_nonzeroidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_nonzeroidentitysecondimaginary) = S ge_signed_half_unit_nonzeroidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_nonzeroidentity) + ge_balance_negative_unit_nonzeroidentitysecondimaginary = (ge_second_in_unit_nonzeroidentity) + ge_balance_positive_unit_nonzeroidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_nonzeroidentityoutput ge_representation_imaginary_code_unit_nonzeroidentityoutput. (((6) = ((ge_representation_real_code_unit_nonzeroidentityoutput) + (ge_representation_imaginary_code_unit_nonzeroidentityoutput)) * S ((ge_representation_real_code_unit_nonzeroidentityoutput) + (ge_representation_imaginary_code_unit_nonzeroidentityoutput)) + ((ge_representation_imaginary_code_unit_nonzeroidentityoutput) + (ge_representation_imaginary_code_unit_nonzeroidentityoutput))) /\ ((exists ge_balance_positive_unit_nonzeroidentityoutputreal ge_balance_negative_unit_nonzeroidentityoutputreal. (((((ge_representation_real_code_unit_nonzeroidentityoutput) = 2 * (ge_balance_positive_unit_nonzeroidentityoutputreal) /\ (ge_balance_negative_unit_nonzeroidentityoutputreal) = 0) \/ exists ge_signed_half_unit_nonzeroidentityoutputrealdecode. (((ge_representation_real_code_unit_nonzeroidentityoutput) = 2 * ge_signed_half_unit_nonzeroidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_nonzeroidentityoutputreal) = 0) /\ (ge_balance_negative_unit_nonzeroidentityoutputreal) = S ge_signed_half_unit_nonzeroidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_nonzeroidentity) * (ge_second_rp_unit_nonzeroidentity))) + (((ge_first_rn_unit_nonzeroidentity) * (ge_second_rn_unit_nonzeroidentity))))) + (((((ge_first_ip_unit_nonzeroidentity) * (ge_second_in_unit_nonzeroidentity))) + (((ge_first_in_unit_nonzeroidentity) * (ge_second_ip_unit_nonzeroidentity))))))) + ge_balance_negative_unit_nonzeroidentityoutputreal = (((((((ge_first_rp_unit_nonzeroidentity) * (ge_second_rn_unit_nonzeroidentity))) + (((ge_first_rn_unit_nonzeroidentity) * (ge_second_rp_unit_nonzeroidentity))))) + (((((ge_first_ip_unit_nonzeroidentity) * (ge_second_ip_unit_nonzeroidentity))) + (((ge_first_in_unit_nonzeroidentity) * (ge_second_in_unit_nonzeroidentity))))))) + ge_balance_positive_unit_nonzeroidentityoutputreal))) /\ (exists ge_balance_positive_unit_nonzeroidentityoutputimaginary ge_balance_negative_unit_nonzeroidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_nonzeroidentityoutput) = 2 * (ge_balance_positive_unit_nonzeroidentityoutputimaginary) /\ (ge_balance_negative_unit_nonzeroidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_nonzeroidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_nonzeroidentityoutput) = 2 * ge_signed_half_unit_nonzeroidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_nonzeroidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_nonzeroidentityoutputimaginary) = S ge_signed_half_unit_nonzeroidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_nonzeroidentity) * (ge_second_ip_unit_nonzeroidentity))) + (((ge_first_rn_unit_nonzeroidentity) * (ge_second_in_unit_nonzeroidentity))))) + (((((ge_first_ip_unit_nonzeroidentity) * (ge_second_rp_unit_nonzeroidentity))) + (((ge_first_in_unit_nonzeroidentity) * (ge_second_rn_unit_nonzeroidentity))))))) + ge_balance_negative_unit_nonzeroidentityoutputimaginary = (((((((ge_first_rp_unit_nonzeroidentity) * (ge_second_in_unit_nonzeroidentity))) + (((ge_first_rn_unit_nonzeroidentity) * (ge_second_ip_unit_nonzeroidentity))))) + (((((ge_first_ip_unit_nonzeroidentity) * (ge_second_rn_unit_nonzeroidentity))) + (((ge_first_in_unit_nonzeroidentity) * (ge_second_rp_unit_nonzeroidentity))))))) + ge_balance_positive_unit_nonzeroidentityoutputimaginary)))))))))) -> ~(z=0)Constructive proof overview
Generated structural guide
A Gaussian multiplicative unit cannot have zero canonical code.
The unchanged tactic script uses 2 declared prerequisites and contains 13 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 (2)
01Fix variables and assumptionsL1–3
02Establish hbadL4–13
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian code zero implies norm zero.
Original exact command ledger · 13 lines
- 0001
intro z - 0002
intro hu - 0003
intro hz - 0004
have hbad : 1=0 - 0005
specialize gaussian_code_zero_implies_norm_zero (z) - 0006
specialize gaussian_code_zero_implies_norm_zero (1) - 0007
apply gaussian_code_zero_implies_norm_zero - 0008
specialize gaussian_unit_has_norm_one (z) - 0009
apply gaussian_unit_has_norm_one - 0010
exact hu - 0011
exact hz - 0012
apply PA1 - 0013
exact hbad