GF001D

gaussian_unit_nonzero

A Gaussian multiplicative unit cannot have zero canonical code.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ z. GUnit(z) → ¬z = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GUnit(z) · 1

Actual proof prerequisites

gaussian_unit_has_norm_onegaussian_code_zero_implies_norm_zero
Original expanded first-order 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)

Complete tactic proof in conservative notation

All 13 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

13 script commands · 2 reading checkpoints · 1 local claims

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
gaussian code zero implies norm zerogaussian unit has norm one
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro z
  2. L2
    intro hu
  3. L3
    intro hz
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.

  1. L4
    have hbad : 1=0
  2. L5
    specialize gaussian_code_zero_implies_norm_zero (z)
  3. L6
    specialize gaussian_code_zero_implies_norm_zero (1)
  4. L7
    apply gaussian_code_zero_implies_norm_zero
  5. L8
    specialize gaussian_unit_has_norm_one (z)
  6. L9
    apply gaussian_unit_has_norm_one
  7. L10
    exact hu
  8. L11
    exact hz
  9. L12
    apply PA1
  10. L13
    exact hbad

Library-wide reading audit

Original defined command ledger · 13 lines
  1. 0001intro z
  2. 0002intro hu
  3. 0003intro hz
  4. 0004have hbad : 1=0
  5. 0005specialize gaussian_code_zero_implies_norm_zero (z)
  6. 0006specialize gaussian_code_zero_implies_norm_zero (1)
  7. 0007apply gaussian_code_zero_implies_norm_zero
  8. 0008specialize gaussian_unit_has_norm_one (z)
  9. 0009apply gaussian_unit_has_norm_one
  10. 0010exact hu
  11. 0011exact hz
  12. 0012apply PA1
  13. 0013exact hbad