GF0028

gaussian_multiply_one_right

The actual canonical Gaussian multiply one identity holds on the entire valid carrier.

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

∀ a. ZPairValid(a) → GMul(a,6,a)

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

Definition DAG

ZPairValid(z) · 1ZPairRep(z,ap,an,bp,bn) · 1GMul(a,b,c) · 1

Actual proof prerequisites

gaussian_valid_has_representationgaussian_multiply_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_one_representationzero_add · checked external prerequisite
Original expanded first-order statement 
forall a. (exists ge_real_positive_multiply_one_domain ge_real_negative_multiply_one_domain ge_imaginary_positive_multiply_one_domain ge_imaginary_negative_multiply_one_domain. (exists ge_real_code_multiply_one_domaindecode ge_imaginary_code_multiply_one_domaindecode. (((a) = ((ge_real_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode)) * S ((ge_real_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode)) + ((ge_imaginary_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode))) /\ (((((ge_real_code_multiply_one_domaindecode) = 2 * (ge_real_positive_multiply_one_domain) /\ (ge_real_negative_multiply_one_domain) = 0) \/ exists ge_signed_half_ge_multiply_one_domaindecode_real. (((ge_real_code_multiply_one_domaindecode) = 2 * ge_signed_half_ge_multiply_one_domaindecode_real + 1 /\ (ge_real_positive_multiply_one_domain) = 0) /\ (ge_real_negative_multiply_one_domain) = S ge_signed_half_ge_multiply_one_domaindecode_real))) /\ ((((ge_imaginary_code_multiply_one_domaindecode) = 2 * (ge_imaginary_positive_multiply_one_domain) /\ (ge_imaginary_negative_multiply_one_domain) = 0) \/ exists ge_signed_half_ge_multiply_one_domaindecode_imaginary. (((ge_imaginary_code_multiply_one_domaindecode) = 2 * ge_signed_half_ge_multiply_one_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_multiply_one_domain) = 0) /\ (ge_imaginary_negative_multiply_one_domain) = S ge_signed_half_ge_multiply_one_domaindecode_imaginary))))))) -> (exists ge_first_rp_multiply_one_right ge_first_rn_multiply_one_right ge_first_ip_multiply_one_right ge_first_in_multiply_one_right ge_second_rp_multiply_one_right ge_second_rn_multiply_one_right ge_second_ip_multiply_one_right ge_second_in_multiply_one_right. ((exists ge_representation_real_code_multiply_one_rightfirst ge_representation_imaginary_code_multiply_one_rightfirst. (((a) = ((ge_representation_real_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst)) * S ((ge_representation_real_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst)) + ((ge_representation_imaginary_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst))) /\ ((exists ge_balance_positive_multiply_one_rightfirstreal ge_balance_negative_multiply_one_rightfirstreal. (((((ge_representation_real_code_multiply_one_rightfirst) = 2 * (ge_balance_positive_multiply_one_rightfirstreal) /\ (ge_balance_negative_multiply_one_rightfirstreal) = 0) \/ exists ge_signed_half_multiply_one_rightfirstrealdecode. (((ge_representation_real_code_multiply_one_rightfirst) = 2 * ge_signed_half_multiply_one_rightfirstrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightfirstreal) = 0) /\ (ge_balance_negative_multiply_one_rightfirstreal) = S ge_signed_half_multiply_one_rightfirstrealdecode))) /\ ((ge_first_rp_multiply_one_right) + ge_balance_negative_multiply_one_rightfirstreal = (ge_first_rn_multiply_one_right) + ge_balance_positive_multiply_one_rightfirstreal))) /\ (exists ge_balance_positive_multiply_one_rightfirstimaginary ge_balance_negative_multiply_one_rightfirstimaginary. (((((ge_representation_imaginary_code_multiply_one_rightfirst) = 2 * (ge_balance_positive_multiply_one_rightfirstimaginary) /\ (ge_balance_negative_multiply_one_rightfirstimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightfirst) = 2 * ge_signed_half_multiply_one_rightfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightfirstimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightfirstimaginary) = S ge_signed_half_multiply_one_rightfirstimaginarydecode))) /\ ((ge_first_ip_multiply_one_right) + ge_balance_negative_multiply_one_rightfirstimaginary = (ge_first_in_multiply_one_right) + ge_balance_positive_multiply_one_rightfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_one_rightsecond ge_representation_imaginary_code_multiply_one_rightsecond. (((6) = ((ge_representation_real_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond)) * S ((ge_representation_real_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond)) + ((ge_representation_imaginary_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond))) /\ ((exists ge_balance_positive_multiply_one_rightsecondreal ge_balance_negative_multiply_one_rightsecondreal. (((((ge_representation_real_code_multiply_one_rightsecond) = 2 * (ge_balance_positive_multiply_one_rightsecondreal) /\ (ge_balance_negative_multiply_one_rightsecondreal) = 0) \/ exists ge_signed_half_multiply_one_rightsecondrealdecode. (((ge_representation_real_code_multiply_one_rightsecond) = 2 * ge_signed_half_multiply_one_rightsecondrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightsecondreal) = 0) /\ (ge_balance_negative_multiply_one_rightsecondreal) = S ge_signed_half_multiply_one_rightsecondrealdecode))) /\ ((ge_second_rp_multiply_one_right) + ge_balance_negative_multiply_one_rightsecondreal = (ge_second_rn_multiply_one_right) + ge_balance_positive_multiply_one_rightsecondreal))) /\ (exists ge_balance_positive_multiply_one_rightsecondimaginary ge_balance_negative_multiply_one_rightsecondimaginary. (((((ge_representation_imaginary_code_multiply_one_rightsecond) = 2 * (ge_balance_positive_multiply_one_rightsecondimaginary) /\ (ge_balance_negative_multiply_one_rightsecondimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightsecond) = 2 * ge_signed_half_multiply_one_rightsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightsecondimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightsecondimaginary) = S ge_signed_half_multiply_one_rightsecondimaginarydecode))) /\ ((ge_second_ip_multiply_one_right) + ge_balance_negative_multiply_one_rightsecondimaginary = (ge_second_in_multiply_one_right) + ge_balance_positive_multiply_one_rightsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_one_rightoutput ge_representation_imaginary_code_multiply_one_rightoutput. (((a) = ((ge_representation_real_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput)) * S ((ge_representation_real_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput)) + ((ge_representation_imaginary_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput))) /\ ((exists ge_balance_positive_multiply_one_rightoutputreal ge_balance_negative_multiply_one_rightoutputreal. (((((ge_representation_real_code_multiply_one_rightoutput) = 2 * (ge_balance_positive_multiply_one_rightoutputreal) /\ (ge_balance_negative_multiply_one_rightoutputreal) = 0) \/ exists ge_signed_half_multiply_one_rightoutputrealdecode. (((ge_representation_real_code_multiply_one_rightoutput) = 2 * ge_signed_half_multiply_one_rightoutputrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightoutputreal) = 0) /\ (ge_balance_negative_multiply_one_rightoutputreal) = S ge_signed_half_multiply_one_rightoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_one_right) * (ge_second_rp_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_rn_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_in_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_ip_multiply_one_right))))))) + ge_balance_negative_multiply_one_rightoutputreal = (((((((ge_first_rp_multiply_one_right) * (ge_second_rn_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_rp_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_ip_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_in_multiply_one_right))))))) + ge_balance_positive_multiply_one_rightoutputreal))) /\ (exists ge_balance_positive_multiply_one_rightoutputimaginary ge_balance_negative_multiply_one_rightoutputimaginary. (((((ge_representation_imaginary_code_multiply_one_rightoutput) = 2 * (ge_balance_positive_multiply_one_rightoutputimaginary) /\ (ge_balance_negative_multiply_one_rightoutputimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightoutput) = 2 * ge_signed_half_multiply_one_rightoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightoutputimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightoutputimaginary) = S ge_signed_half_multiply_one_rightoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_one_right) * (ge_second_ip_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_in_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_rp_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_rn_multiply_one_right))))))) + ge_balance_negative_multiply_one_rightoutputimaginary = (((((((ge_first_rp_multiply_one_right) * (ge_second_in_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_ip_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_rn_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_rp_multiply_one_right))))))) + ge_balance_positive_multiply_one_rightoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

38 script commands · 9 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 valid has representationgaussian one representation
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro hv
02Establish hAL3–6

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

  1. L3
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep(a,rp,rn,ip,inn)Original native command in the exact edition
  2. L4
    specialize gaussian_valid_has_representation (a)
  3. L5
    apply gaussian_valid_has_representation
  4. L6
    exact hv
03Separate the logical casesL7–10

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

  1. L7
    cases hA
  2. L8
    cases hA_witness
  3. L9
    cases hA_witness_witness
  4. L10
    cases hA_witness_witness_witness
04Use earlier factsL11–20

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

  1. L11
    specialize gaussian_multiply_of_representations (a)
  2. L12
    specialize gaussian_multiply_of_representations (6)
  3. L13
    specialize gaussian_multiply_of_representations (a)
  4. L14
    specialize gaussian_multiply_of_representations (x)
  5. L15
    specialize gaussian_multiply_of_representations (x1)
  6. L16
    specialize gaussian_multiply_of_representations (x2)
  7. L17
    specialize gaussian_multiply_of_representations (x3)
  8. L18
    specialize gaussian_multiply_of_representations (1)
  9. L19
    specialize gaussian_multiply_of_representations (0)
  10. L20
    specialize gaussian_multiply_of_representations (0)
05Use earlier factsL21–30

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

  1. L21
    specialize gaussian_multiply_of_representations (0)
  2. L22
    apply gaussian_multiply_of_representations
  3. L23
    exact hA_witness_witness_witness_witness
  4. L24
    exact gaussian_one_representation
  5. L25
    specialize gaussian_representation_integer_transport (a)
  6. L26
    specialize gaussian_representation_integer_transport (x)
  7. L27
    specialize gaussian_representation_integer_transport (x1)
  8. L28
    specialize gaussian_representation_integer_transport (x2)
  9. L29
    specialize gaussian_representation_integer_transport (x3)
  10. L30
    specialize gaussian_representation_integer_transport (((((((x) * (1))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
06Use earlier factsL31–34

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

  1. L31
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (1))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  2. L32
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (1))) + (((x3) * (0)))))))
  3. L33
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (1)))))))
  4. L34
    apply gaussian_representation_integer_transport
07Separate the logical casesL35–35

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

  1. L35
    split
08Calculate and transport equalitiesL36–37

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

  1. L36
    simp [zero_add]
  2. L37
    simp [zero_add]
09Use earlier factsL38–38

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

  1. L38
    exact hA_witness_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro a
  2. 0002intro hv
  3. 0003have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  4. 0004specialize gaussian_valid_has_representation (a)
  5. 0005apply gaussian_valid_has_representation
  6. 0006exact hv
  7. 0007cases hA
  8. 0008cases hA_witness
  9. 0009cases hA_witness_witness
  10. 0010cases hA_witness_witness_witness
  11. 0011specialize gaussian_multiply_of_representations (a)
  12. 0012specialize gaussian_multiply_of_representations (6)
  13. 0013specialize gaussian_multiply_of_representations (a)
  14. 0014specialize gaussian_multiply_of_representations (x)
  15. 0015specialize gaussian_multiply_of_representations (x1)
  16. 0016specialize gaussian_multiply_of_representations (x2)
  17. 0017specialize gaussian_multiply_of_representations (x3)
  18. 0018specialize gaussian_multiply_of_representations (1)
  19. 0019specialize gaussian_multiply_of_representations (0)
  20. 0020specialize gaussian_multiply_of_representations (0)
  21. 0021specialize gaussian_multiply_of_representations (0)
  22. 0022apply gaussian_multiply_of_representations
  23. 0023exact hA_witness_witness_witness_witness
  24. 0024exact gaussian_one_representation
  25. 0025specialize gaussian_representation_integer_transport (a)
  26. 0026specialize gaussian_representation_integer_transport (x)
  27. 0027specialize gaussian_representation_integer_transport (x1)
  28. 0028specialize gaussian_representation_integer_transport (x2)
  29. 0029specialize gaussian_representation_integer_transport (x3)
  30. 0030specialize gaussian_representation_integer_transport (((((((x) * (1))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  31. 0031specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (1))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  32. 0032specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (1))) + (((x3) * (0)))))))
  33. 0033specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (1)))))))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035split
  36. 0036simp [zero_add]
  37. 0037simp [zero_add]
  38. 0038exact hA_witness_witness_witness_witness