GF0019

gaussian_unit_has_norm_one

An actual inverse multiplies norms to one, forcing the unit norm to equal one.

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) → GNorm(z,1)

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

Definition DAG

GNorm(z,n) · 3GUnit(z) · 1

Actual proof prerequisites

gaussian_norm_exists · checked external prerequisitegaussian_multiply_input_left_validgaussian_multiply_input_right_validgaussian_norm_multiply · checked external prerequisitegaussian_norm_functional · checked external prerequisitegaussian_one_normdivisor_one · checked external prerequisitegaussian_norm_value_transport
Original expanded first-order statement 
forall z. (exists gr_inverse_unit_norm_given. (exists ge_first_rp_unit_norm_givenidentity ge_first_rn_unit_norm_givenidentity ge_first_ip_unit_norm_givenidentity ge_first_in_unit_norm_givenidentity ge_second_rp_unit_norm_givenidentity ge_second_rn_unit_norm_givenidentity ge_second_ip_unit_norm_givenidentity ge_second_in_unit_norm_givenidentity. ((exists ge_representation_real_code_unit_norm_givenidentityfirst ge_representation_imaginary_code_unit_norm_givenidentityfirst. (((z) = ((ge_representation_real_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst)) * S ((ge_representation_real_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst)) + ((ge_representation_imaginary_code_unit_norm_givenidentityfirst) + (ge_representation_imaginary_code_unit_norm_givenidentityfirst))) /\ ((exists ge_balance_positive_unit_norm_givenidentityfirstreal ge_balance_negative_unit_norm_givenidentityfirstreal. (((((ge_representation_real_code_unit_norm_givenidentityfirst) = 2 * (ge_balance_positive_unit_norm_givenidentityfirstreal) /\ (ge_balance_negative_unit_norm_givenidentityfirstreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentityfirstrealdecode. (((ge_representation_real_code_unit_norm_givenidentityfirst) = 2 * ge_signed_half_unit_norm_givenidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityfirstreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentityfirstreal) = S ge_signed_half_unit_norm_givenidentityfirstrealdecode))) /\ ((ge_first_rp_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentityfirstreal = (ge_first_rn_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentityfirstreal))) /\ (exists ge_balance_positive_unit_norm_givenidentityfirstimaginary ge_balance_negative_unit_norm_givenidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentityfirst) = 2 * (ge_balance_positive_unit_norm_givenidentityfirstimaginary) /\ (ge_balance_negative_unit_norm_givenidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentityfirst) = 2 * ge_signed_half_unit_norm_givenidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentityfirstimaginary) = S ge_signed_half_unit_norm_givenidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentityfirstimaginary = (ge_first_in_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_norm_givenidentitysecond ge_representation_imaginary_code_unit_norm_givenidentitysecond. (((gr_inverse_unit_norm_given) = ((ge_representation_real_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond)) * S ((ge_representation_real_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond)) + ((ge_representation_imaginary_code_unit_norm_givenidentitysecond) + (ge_representation_imaginary_code_unit_norm_givenidentitysecond))) /\ ((exists ge_balance_positive_unit_norm_givenidentitysecondreal ge_balance_negative_unit_norm_givenidentitysecondreal. (((((ge_representation_real_code_unit_norm_givenidentitysecond) = 2 * (ge_balance_positive_unit_norm_givenidentitysecondreal) /\ (ge_balance_negative_unit_norm_givenidentitysecondreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentitysecondrealdecode. (((ge_representation_real_code_unit_norm_givenidentitysecond) = 2 * ge_signed_half_unit_norm_givenidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentitysecondreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentitysecondreal) = S ge_signed_half_unit_norm_givenidentitysecondrealdecode))) /\ ((ge_second_rp_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentitysecondreal = (ge_second_rn_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentitysecondreal))) /\ (exists ge_balance_positive_unit_norm_givenidentitysecondimaginary ge_balance_negative_unit_norm_givenidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentitysecond) = 2 * (ge_balance_positive_unit_norm_givenidentitysecondimaginary) /\ (ge_balance_negative_unit_norm_givenidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentitysecond) = 2 * ge_signed_half_unit_norm_givenidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentitysecondimaginary) = S ge_signed_half_unit_norm_givenidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_norm_givenidentity) + ge_balance_negative_unit_norm_givenidentitysecondimaginary = (ge_second_in_unit_norm_givenidentity) + ge_balance_positive_unit_norm_givenidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_norm_givenidentityoutput ge_representation_imaginary_code_unit_norm_givenidentityoutput. (((6) = ((ge_representation_real_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput)) * S ((ge_representation_real_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput)) + ((ge_representation_imaginary_code_unit_norm_givenidentityoutput) + (ge_representation_imaginary_code_unit_norm_givenidentityoutput))) /\ ((exists ge_balance_positive_unit_norm_givenidentityoutputreal ge_balance_negative_unit_norm_givenidentityoutputreal. (((((ge_representation_real_code_unit_norm_givenidentityoutput) = 2 * (ge_balance_positive_unit_norm_givenidentityoutputreal) /\ (ge_balance_negative_unit_norm_givenidentityoutputreal) = 0) \/ exists ge_signed_half_unit_norm_givenidentityoutputrealdecode. (((ge_representation_real_code_unit_norm_givenidentityoutput) = 2 * ge_signed_half_unit_norm_givenidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityoutputreal) = 0) /\ (ge_balance_negative_unit_norm_givenidentityoutputreal) = S ge_signed_half_unit_norm_givenidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))))))) + ge_balance_negative_unit_norm_givenidentityoutputreal = (((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))))))) + ge_balance_positive_unit_norm_givenidentityoutputreal))) /\ (exists ge_balance_positive_unit_norm_givenidentityoutputimaginary ge_balance_negative_unit_norm_givenidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_norm_givenidentityoutput) = 2 * (ge_balance_positive_unit_norm_givenidentityoutputimaginary) /\ (ge_balance_negative_unit_norm_givenidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_norm_givenidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_norm_givenidentityoutput) = 2 * ge_signed_half_unit_norm_givenidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_givenidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_norm_givenidentityoutputimaginary) = S ge_signed_half_unit_norm_givenidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))))))) + ge_balance_negative_unit_norm_givenidentityoutputimaginary = (((((((ge_first_rp_unit_norm_givenidentity) * (ge_second_in_unit_norm_givenidentity))) + (((ge_first_rn_unit_norm_givenidentity) * (ge_second_ip_unit_norm_givenidentity))))) + (((((ge_first_ip_unit_norm_givenidentity) * (ge_second_rn_unit_norm_givenidentity))) + (((ge_first_in_unit_norm_givenidentity) * (ge_second_rp_unit_norm_givenidentity))))))) + ge_balance_positive_unit_norm_givenidentityoutputimaginary)))))))))) -> (exists ge_norm_rp_unit_norm_value ge_norm_rn_unit_norm_value ge_norm_ip_unit_norm_value ge_norm_in_unit_norm_value. ((exists ge_representation_real_code_unit_norm_valuerepresentation ge_representation_imaginary_code_unit_norm_valuerepresentation. (((z) = ((ge_representation_real_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation)) * S ((ge_representation_real_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation)) + ((ge_representation_imaginary_code_unit_norm_valuerepresentation) + (ge_representation_imaginary_code_unit_norm_valuerepresentation))) /\ ((exists ge_balance_positive_unit_norm_valuerepresentationreal ge_balance_negative_unit_norm_valuerepresentationreal. (((((ge_representation_real_code_unit_norm_valuerepresentation) = 2 * (ge_balance_positive_unit_norm_valuerepresentationreal) /\ (ge_balance_negative_unit_norm_valuerepresentationreal) = 0) \/ exists ge_signed_half_unit_norm_valuerepresentationrealdecode. (((ge_representation_real_code_unit_norm_valuerepresentation) = 2 * ge_signed_half_unit_norm_valuerepresentationrealdecode + 1 /\ (ge_balance_positive_unit_norm_valuerepresentationreal) = 0) /\ (ge_balance_negative_unit_norm_valuerepresentationreal) = S ge_signed_half_unit_norm_valuerepresentationrealdecode))) /\ ((ge_norm_rp_unit_norm_value) + ge_balance_negative_unit_norm_valuerepresentationreal = (ge_norm_rn_unit_norm_value) + ge_balance_positive_unit_norm_valuerepresentationreal))) /\ (exists ge_balance_positive_unit_norm_valuerepresentationimaginary ge_balance_negative_unit_norm_valuerepresentationimaginary. (((((ge_representation_imaginary_code_unit_norm_valuerepresentation) = 2 * (ge_balance_positive_unit_norm_valuerepresentationimaginary) /\ (ge_balance_negative_unit_norm_valuerepresentationimaginary) = 0) \/ exists ge_signed_half_unit_norm_valuerepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_norm_valuerepresentation) = 2 * ge_signed_half_unit_norm_valuerepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_norm_valuerepresentationimaginary) = 0) /\ (ge_balance_negative_unit_norm_valuerepresentationimaginary) = S ge_signed_half_unit_norm_valuerepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_norm_value) + ge_balance_negative_unit_norm_valuerepresentationimaginary = (ge_norm_in_unit_norm_value) + ge_balance_positive_unit_norm_valuerepresentationimaginary)))))) /\ (exists ge_real_square_unit_norm_valuesquare ge_imaginary_square_unit_norm_valuesquare. ((((((ge_norm_rp_unit_norm_value) * (ge_norm_rp_unit_norm_value))) + (((ge_norm_rn_unit_norm_value) * (ge_norm_rn_unit_norm_value)))) = ((ge_real_square_unit_norm_valuesquare) + (((((ge_norm_rp_unit_norm_value) * (ge_norm_rn_unit_norm_value))) + (((ge_norm_rn_unit_norm_value) * (ge_norm_rp_unit_norm_value))))))) /\ ((((((ge_norm_ip_unit_norm_value) * (ge_norm_ip_unit_norm_value))) + (((ge_norm_in_unit_norm_value) * (ge_norm_in_unit_norm_value)))) = ((ge_imaginary_square_unit_norm_valuesquare) + (((((ge_norm_ip_unit_norm_value) * (ge_norm_in_unit_norm_value))) + (((ge_norm_in_unit_norm_value) * (ge_norm_ip_unit_norm_value))))))) /\ ((1) = ge_real_square_unit_norm_valuesquare + ge_imaginary_square_unit_norm_valuesquare))))))

Complete tactic proof in conservative notation

All 48 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

48 script commands · 12 reading checkpoints · 4 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 (4)
gaussian multiply input left validgaussian multiply input right validgaussian one normgaussian norm value transport
01Fix variables and assumptionsL1–2

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

  1. L1
    intro z
  2. L2
    intro hu
02Separate the logical casesL3–3

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L3
    cases hu
03Establish hNL4–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.

  1. L4
    have hN : ∃ N. GNorm(z,N)Definitions: GNorm(z,N)Original native command in the exact edition
  2. L5
    specialize gaussian_norm_exists (z)
  3. L6
    apply gaussian_norm_exists
  4. L7
    specialize gaussian_multiply_input_left_valid (z)
  5. L8
    specialize gaussian_multiply_input_left_valid (x)
  6. L9
    specialize gaussian_multiply_input_left_valid (6)
  7. L10
    apply gaussian_multiply_input_left_valid
  8. L11
    exact hu_witness
04Separate the logical casesL12–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hN
05Establish hML13–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.

  1. L13
    have hM : ∃ M. GNorm(x,M)Definitions: GNorm(x,M)Original native command in the exact edition
  2. L14
    specialize gaussian_norm_exists (x)
  3. L15
    apply gaussian_norm_exists
  4. L16
    specialize gaussian_multiply_input_right_valid (z)
  5. L17
    specialize gaussian_multiply_input_right_valid (x)
  6. L18
    specialize gaussian_multiply_input_right_valid (6)
  7. L19
    apply gaussian_multiply_input_right_valid
  8. L20
    exact hu_witness
06Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hM
07Establish hproductL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm functional.

  1. L22
    have hproduct : x1*x2=1
  2. L23
    specialize gaussian_norm_functional (6)
  3. L24
    specialize gaussian_norm_functional (x1*x2)
  4. L25
    specialize gaussian_norm_functional (1)
  5. L26
    apply gaussian_norm_functional
  6. L27
    specialize gaussian_norm_multiply (z)
  7. L28
    specialize gaussian_norm_multiply (x)
  8. L29
    specialize gaussian_norm_multiply (6)
  9. L30
    specialize gaussian_norm_multiply (x1)
  10. L31
    specialize gaussian_norm_multiply (x2)
08Use earlier factsL32–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    apply gaussian_norm_multiply
  2. L33
    exact hN_witness
  3. L34
    exact hM_witness
  4. L35
    exact hu_witness
  5. L36
    exact gaussian_one_norm
09Establish honeL37–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor one.

  1. L37
    have hone : x1=1
  2. L38
    specialize divisor_one (x1)
  3. L39
    apply divisor_one
10Construct an explicit witnessL40–40

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists (x2)
11Calculate and transport equalitiesL41–41

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L41
    symm
12Use earlier factsL42–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L42
    exact hproduct
  2. L43
    specialize gaussian_norm_value_transport (z)
  3. L44
    specialize gaussian_norm_value_transport (x1)
  4. L45
    specialize gaussian_norm_value_transport (1)
  5. L46
    apply gaussian_norm_value_transport
  6. L47
    exact hone
  7. L48
    exact hN_witness

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro z
  2. 0002intro hu
  3. 0003cases hu
  4. 0004have hN : ∃ N. GNorm(z,N)
  5. 0005specialize gaussian_norm_exists (z)
  6. 0006apply gaussian_norm_exists
  7. 0007specialize gaussian_multiply_input_left_valid (z)
  8. 0008specialize gaussian_multiply_input_left_valid (x)
  9. 0009specialize gaussian_multiply_input_left_valid (6)
  10. 0010apply gaussian_multiply_input_left_valid
  11. 0011exact hu_witness
  12. 0012cases hN
  13. 0013have hM : ∃ M. GNorm(x,M)
  14. 0014specialize gaussian_norm_exists (x)
  15. 0015apply gaussian_norm_exists
  16. 0016specialize gaussian_multiply_input_right_valid (z)
  17. 0017specialize gaussian_multiply_input_right_valid (x)
  18. 0018specialize gaussian_multiply_input_right_valid (6)
  19. 0019apply gaussian_multiply_input_right_valid
  20. 0020exact hu_witness
  21. 0021cases hM
  22. 0022have hproduct : x1*x2=1
  23. 0023specialize gaussian_norm_functional (6)
  24. 0024specialize gaussian_norm_functional (x1*x2)
  25. 0025specialize gaussian_norm_functional (1)
  26. 0026apply gaussian_norm_functional
  27. 0027specialize gaussian_norm_multiply (z)
  28. 0028specialize gaussian_norm_multiply (x)
  29. 0029specialize gaussian_norm_multiply (6)
  30. 0030specialize gaussian_norm_multiply (x1)
  31. 0031specialize gaussian_norm_multiply (x2)
  32. 0032apply gaussian_norm_multiply
  33. 0033exact hN_witness
  34. 0034exact hM_witness
  35. 0035exact hu_witness
  36. 0036exact gaussian_one_norm
  37. 0037have hone : x1=1
  38. 0038specialize divisor_one (x1)
  39. 0039apply divisor_one
  40. 0040exists (x2)
  41. 0041symm
  42. 0042exact hproduct
  43. 0043specialize gaussian_norm_value_transport (z)
  44. 0044specialize gaussian_norm_value_transport (x1)
  45. 0045specialize gaussian_norm_value_transport (1)
  46. 0046apply gaussian_norm_value_transport
  47. 0047exact hone
  48. 0048exact hN_witness