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_norm_unique_input ge_real_negative_norm_unique_input ge_imaginary_positive_norm_unique_input ge_imaginary_negative_norm_unique_input. (exists ge_real_code_norm_unique_inputdecode ge_imaginary_code_norm_unique_inputdecode. (((z) = ((ge_real_code_norm_unique_inputdecode) + (ge_imaginary_code_norm_unique_inputdecode)) * S ((ge_real_code_norm_unique_inputdecode) + (ge_imaginary_code_norm_unique_inputdecode)) + ((ge_imaginary_code_norm_unique_inputdecode) + (ge_imaginary_code_norm_unique_inputdecode))) /\ (((((ge_real_code_norm_unique_inputdecode) = 2 * (ge_real_positive_norm_unique_input) /\ (ge_real_negative_norm_unique_input) = 0) \/ exists ge_signed_half_ge_norm_unique_inputdecode_real. (((ge_real_code_norm_unique_inputdecode) = 2 * ge_signed_half_ge_norm_unique_inputdecode_real + 1 /\ (ge_real_positive_norm_unique_input) = 0) /\ (ge_real_negative_norm_unique_input) = S ge_signed_half_ge_norm_unique_inputdecode_real))) /\ ((((ge_imaginary_code_norm_unique_inputdecode) = 2 * (ge_imaginary_positive_norm_unique_input) /\ (ge_imaginary_negative_norm_unique_input) = 0) \/ exists ge_signed_half_ge_norm_unique_inputdecode_imaginary. (((ge_imaginary_code_norm_unique_inputdecode) = 2 * ge_signed_half_ge_norm_unique_inputdecode_imaginary + 1 /\ (ge_imaginary_positive_norm_unique_input) = 0) /\ (ge_imaginary_negative_norm_unique_input) = S ge_signed_half_ge_norm_unique_inputdecode_imaginary))))))) -> exists N. (((exists ee_norm_rp_unique_witness ee_norm_rn_unique_witness ee_norm_ip_unique_witness ee_norm_in_unique_witness. ((exists ge_representation_real_code_unique_witnessrepresentation ge_representation_imaginary_code_unique_witnessrepresentation. (((z) = ((ge_representation_real_code_unique_witnessrepresentation) + (ge_representation_imaginary_code_unique_witnessrepresentation)) * S ((ge_representation_real_code_unique_witnessrepresentation) + (ge_representation_imaginary_code_unique_witnessrepresentation)) + ((ge_representation_imaginary_code_unique_witnessrepresentation) + (ge_representation_imaginary_code_unique_witnessrepresentation))) /\ ((exists ge_balance_positive_unique_witnessrepresentationreal ge_balance_negative_unique_witnessrepresentationreal. (((((ge_representation_real_code_unique_witnessrepresentation) = 2 * (ge_balance_positive_unique_witnessrepresentationreal) /\ (ge_balance_negative_unique_witnessrepresentationreal) = 0) \/ exists ge_signed_half_unique_witnessrepresentationrealdecode. (((ge_representation_real_code_unique_witnessrepresentation) = 2 * ge_signed_half_unique_witnessrepresentationrealdecode + 1 /\ (ge_balance_positive_unique_witnessrepresentationreal) = 0) /\ (ge_balance_negative_unique_witnessrepresentationreal) = S ge_signed_half_unique_witnessrepresentationrealdecode))) /\ ((ee_norm_rp_unique_witness) + ge_balance_negative_unique_witnessrepresentationreal = (ee_norm_rn_unique_witness) + ge_balance_positive_unique_witnessrepresentationreal))) /\ (exists ge_balance_positive_unique_witnessrepresentationimaginary ge_balance_negative_unique_witnessrepresentationimaginary. (((((ge_representation_imaginary_code_unique_witnessrepresentation) = 2 * (ge_balance_positive_unique_witnessrepresentationimaginary) /\ (ge_balance_negative_unique_witnessrepresentationimaginary) = 0) \/ exists ge_signed_half_unique_witnessrepresentationimaginarydecode. (((ge_representation_imaginary_code_unique_witnessrepresentation) = 2 * ge_signed_half_unique_witnessrepresentationimaginarydecode + 1 /\ (ge_balance_positive_unique_witnessrepresentationimaginary) = 0) /\ (ge_balance_negative_unique_witnessrepresentationimaginary) = S ge_signed_half_unique_witnessrepresentationimaginarydecode))) /\ ((ee_norm_ip_unique_witness) + ge_balance_negative_unique_witnessrepresentationimaginary = (ee_norm_in_unique_witness) + ge_balance_positive_unique_witnessrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_unique_witness) * (ee_norm_rp_unique_witness))) + (((ee_norm_rn_unique_witness) * (ee_norm_rn_unique_witness))))) + (((((ee_norm_ip_unique_witness) * (ee_norm_ip_unique_witness))) + (((ee_norm_in_unique_witness) * (ee_norm_in_unique_witness))))))) + (((((ee_norm_rp_unique_witness) * (ee_norm_in_unique_witness))) + (((ee_norm_rn_unique_witness) * (ee_norm_ip_unique_witness)))))) = ((((((((((ee_norm_rp_unique_witness) * (ee_norm_rn_unique_witness))) + (((ee_norm_rn_unique_witness) * (ee_norm_rp_unique_witness))))) + (((((ee_norm_ip_unique_witness) * (ee_norm_in_unique_witness))) + (((ee_norm_in_unique_witness) * (ee_norm_ip_unique_witness))))))) + (((((ee_norm_rp_unique_witness) * (ee_norm_ip_unique_witness))) + (((ee_norm_rn_unique_witness) * (ee_norm_in_unique_witness))))))) + (N))))) /\ (forall M. (exists ee_norm_rp_unique_compare ee_norm_rn_unique_compare ee_norm_ip_unique_compare ee_norm_in_unique_compare. ((exists ge_representation_real_code_unique_comparerepresentation ge_representation_imaginary_code_unique_comparerepresentation. (((z) = ((ge_representation_real_code_unique_comparerepresentation) + (ge_representation_imaginary_code_unique_comparerepresentation)) * S ((ge_representation_real_code_unique_comparerepresentation) + (ge_representation_imaginary_code_unique_comparerepresentation)) + ((ge_representation_imaginary_code_unique_comparerepresentation) + (ge_representation_imaginary_code_unique_comparerepresentation))) /\ ((exists ge_balance_positive_unique_comparerepresentationreal ge_balance_negative_unique_comparerepresentationreal. (((((ge_representation_real_code_unique_comparerepresentation) = 2 * (ge_balance_positive_unique_comparerepresentationreal) /\ (ge_balance_negative_unique_comparerepresentationreal) = 0) \/ exists ge_signed_half_unique_comparerepresentationrealdecode. (((ge_representation_real_code_unique_comparerepresentation) = 2 * ge_signed_half_unique_comparerepresentationrealdecode + 1 /\ (ge_balance_positive_unique_comparerepresentationreal) = 0) /\ (ge_balance_negative_unique_comparerepresentationreal) = S ge_signed_half_unique_comparerepresentationrealdecode))) /\ ((ee_norm_rp_unique_compare) + ge_balance_negative_unique_comparerepresentationreal = (ee_norm_rn_unique_compare) + ge_balance_positive_unique_comparerepresentationreal))) /\ (exists ge_balance_positive_unique_comparerepresentationimaginary ge_balance_negative_unique_comparerepresentationimaginary. (((((ge_representation_imaginary_code_unique_comparerepresentation) = 2 * (ge_balance_positive_unique_comparerepresentationimaginary) /\ (ge_balance_negative_unique_comparerepresentationimaginary) = 0) \/ exists ge_signed_half_unique_comparerepresentationimaginarydecode. (((ge_representation_imaginary_code_unique_comparerepresentation) = 2 * ge_signed_half_unique_comparerepresentationimaginarydecode + 1 /\ (ge_balance_positive_unique_comparerepresentationimaginary) = 0) /\ (ge_balance_negative_unique_comparerepresentationimaginary) = S ge_signed_half_unique_comparerepresentationimaginarydecode))) /\ ((ee_norm_ip_unique_compare) + ge_balance_negative_unique_comparerepresentationimaginary = (ee_norm_in_unique_compare) + ge_balance_positive_unique_comparerepresentationimaginary)))))) /\ (((((((((ee_norm_rp_unique_compare) * (ee_norm_rp_unique_compare))) + (((ee_norm_rn_unique_compare) * (ee_norm_rn_unique_compare))))) + (((((ee_norm_ip_unique_compare) * (ee_norm_ip_unique_compare))) + (((ee_norm_in_unique_compare) * (ee_norm_in_unique_compare))))))) + (((((ee_norm_rp_unique_compare) * (ee_norm_in_unique_compare))) + (((ee_norm_rn_unique_compare) * (ee_norm_ip_unique_compare)))))) = ((((((((((ee_norm_rp_unique_compare) * (ee_norm_rn_unique_compare))) + (((ee_norm_rn_unique_compare) * (ee_norm_rp_unique_compare))))) + (((((ee_norm_ip_unique_compare) * (ee_norm_in_unique_compare))) + (((ee_norm_in_unique_compare) * (ee_norm_ip_unique_compare))))))) + (((((ee_norm_rp_unique_compare) * (ee_norm_ip_unique_compare))) + (((ee_norm_rn_unique_compare) * (ee_norm_in_unique_compare))))))) + (M))))) -> M = N)))Constructive proof overview
Generated structural guide
Every valid canonical Eisenstein code has one actually computed and uniquely determined natural norm.
The unchanged tactic script uses 2 declared prerequisites and contains 18 exact native proof lines.
Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
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–2
02Establish hnormL3–6
03Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
cases hnorm
04Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- L8
exists x
05Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
split
06Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact hnorm_witness
07Fix variables and assumptionsL11–12
08Use earlier factsL13–18
Original exact command ledger · 18 lines
- 0001
intro z - 0002
intro hvalid - 0003
have hnorm : exists N. (exists ee_norm_rp_norm_unique_construct ee_norm_rn_norm_unique_construct ee_norm_ip_norm_unique_construct ee_norm_in_norm_unique_construct. ((exists ge_representation_real_code_norm_unique_constructrepresentation ge_representation_imaginary_code_norm_unique_constructrepresentation. (((z) = ((ge_representation_real_code_norm_unique_constructrepresentation) + (ge_representation_imaginary_code_norm_unique_constructrepresentation)) * S ((ge_representation_real_code_norm_unique_constructrepresentation) + (ge_representation_imaginary_code_norm_unique_constructrepresentation)) + ((ge_representation_imaginary_code_norm_unique_constructrepresentation) + (ge_representation_imaginary_code_norm_unique_constructrepresentation))) /\ ((exists ge_balance_positive_norm_unique_constructrepresentationreal ge_balance_negative_norm_unique_constructrepresentationreal. (((((ge_representation_real_code_norm_unique_constructrepresentation) = 2 * (ge_balance_positive_norm_unique_constructrepresentationreal) /\ (ge_balance_negative_norm_unique_constructrepresentationreal) = 0) \/ exists ge_signed_half_norm_unique_constructrepresentationrealdecode. (((ge_representation_real_code_norm_unique_constructrepresentation) = 2 * ge_signed_half_norm_unique_constructrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_unique_constructrepresentationreal) = 0) /\ (ge_balance_negative_norm_unique_constructrepresentationreal) = S ge_signed_half_norm_unique_constructrepresentationrealdecode))) /\ ((ee_norm_rp_norm_unique_construct) + ge_balance_negative_norm_unique_constructrepresentationreal = (ee_norm_rn_norm_unique_construct) + ge_balance_positive_norm_unique_constructrepresentationreal))) /\ (exists ge_balance_positive_norm_unique_constructrepresentationimaginary ge_balance_negative_norm_unique_constructrepresentationimaginary. (((((ge_representation_imaginary_code_norm_unique_constructrepresentation) = 2 * (ge_balance_positive_norm_unique_constructrepresentationimaginary) /\ (ge_balance_negative_norm_unique_constructrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_unique_constructrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_unique_constructrepresentation) = 2 * ge_signed_half_norm_unique_constructrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_unique_constructrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_unique_constructrepresentationimaginary) = S ge_signed_half_norm_unique_constructrepresentationimaginarydecode))) /\ ((ee_norm_ip_norm_unique_construct) + ge_balance_negative_norm_unique_constructrepresentationimaginary = (ee_norm_in_norm_unique_construct) + ge_balance_positive_norm_unique_constructrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_norm_unique_construct) * (ee_norm_rp_norm_unique_construct))) + (((ee_norm_rn_norm_unique_construct) * (ee_norm_rn_norm_unique_construct))))) + (((((ee_norm_ip_norm_unique_construct) * (ee_norm_ip_norm_unique_construct))) + (((ee_norm_in_norm_unique_construct) * (ee_norm_in_norm_unique_construct))))))) + (((((ee_norm_rp_norm_unique_construct) * (ee_norm_in_norm_unique_construct))) + (((ee_norm_rn_norm_unique_construct) * (ee_norm_ip_norm_unique_construct)))))) = ((((((((((ee_norm_rp_norm_unique_construct) * (ee_norm_rn_norm_unique_construct))) + (((ee_norm_rn_norm_unique_construct) * (ee_norm_rp_norm_unique_construct))))) + (((((ee_norm_ip_norm_unique_construct) * (ee_norm_in_norm_unique_construct))) + (((ee_norm_in_norm_unique_construct) * (ee_norm_ip_norm_unique_construct))))))) + (((((ee_norm_rp_norm_unique_construct) * (ee_norm_ip_norm_unique_construct))) + (((ee_norm_rn_norm_unique_construct) * (ee_norm_in_norm_unique_construct))))))) + (N))))) - 0004
specialize eisenstein_norm_exists z - 0005
apply eisenstein_norm_exists - 0006
exact hvalid - 0007
cases hnorm - 0008
exists x - 0009
split - 0010
exact hnorm_witness - 0011
intro M - 0012
intro hother - 0013
specialize eisenstein_norm_functional z - 0014
specialize eisenstein_norm_functional M - 0015
specialize eisenstein_norm_functional x - 0016
apply eisenstein_norm_functional - 0017
exact hother - 0018
exact hnorm_witness