GF0026

gaussian_add_zero_right

The actual canonical Gaussian add zero 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) → ZPairAdd(a,0,a)

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

Definition DAG

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

Actual proof prerequisites

gaussian_valid_has_representationgaussian_add_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_zero_representation
Original expanded first-order statement 
forall a. (exists ge_real_positive_add_zero_domain ge_real_negative_add_zero_domain ge_imaginary_positive_add_zero_domain ge_imaginary_negative_add_zero_domain. (exists ge_real_code_add_zero_domaindecode ge_imaginary_code_add_zero_domaindecode. (((a) = ((ge_real_code_add_zero_domaindecode) + (ge_imaginary_code_add_zero_domaindecode)) * S ((ge_real_code_add_zero_domaindecode) + (ge_imaginary_code_add_zero_domaindecode)) + ((ge_imaginary_code_add_zero_domaindecode) + (ge_imaginary_code_add_zero_domaindecode))) /\ (((((ge_real_code_add_zero_domaindecode) = 2 * (ge_real_positive_add_zero_domain) /\ (ge_real_negative_add_zero_domain) = 0) \/ exists ge_signed_half_ge_add_zero_domaindecode_real. (((ge_real_code_add_zero_domaindecode) = 2 * ge_signed_half_ge_add_zero_domaindecode_real + 1 /\ (ge_real_positive_add_zero_domain) = 0) /\ (ge_real_negative_add_zero_domain) = S ge_signed_half_ge_add_zero_domaindecode_real))) /\ ((((ge_imaginary_code_add_zero_domaindecode) = 2 * (ge_imaginary_positive_add_zero_domain) /\ (ge_imaginary_negative_add_zero_domain) = 0) \/ exists ge_signed_half_ge_add_zero_domaindecode_imaginary. (((ge_imaginary_code_add_zero_domaindecode) = 2 * ge_signed_half_ge_add_zero_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_add_zero_domain) = 0) /\ (ge_imaginary_negative_add_zero_domain) = S ge_signed_half_ge_add_zero_domaindecode_imaginary))))))) -> (exists ge_first_rp_add_zero_right ge_first_rn_add_zero_right ge_first_ip_add_zero_right ge_first_in_add_zero_right ge_second_rp_add_zero_right ge_second_rn_add_zero_right ge_second_ip_add_zero_right ge_second_in_add_zero_right. ((exists ge_representation_real_code_add_zero_rightfirst ge_representation_imaginary_code_add_zero_rightfirst. (((a) = ((ge_representation_real_code_add_zero_rightfirst) + (ge_representation_imaginary_code_add_zero_rightfirst)) * S ((ge_representation_real_code_add_zero_rightfirst) + (ge_representation_imaginary_code_add_zero_rightfirst)) + ((ge_representation_imaginary_code_add_zero_rightfirst) + (ge_representation_imaginary_code_add_zero_rightfirst))) /\ ((exists ge_balance_positive_add_zero_rightfirstreal ge_balance_negative_add_zero_rightfirstreal. (((((ge_representation_real_code_add_zero_rightfirst) = 2 * (ge_balance_positive_add_zero_rightfirstreal) /\ (ge_balance_negative_add_zero_rightfirstreal) = 0) \/ exists ge_signed_half_add_zero_rightfirstrealdecode. (((ge_representation_real_code_add_zero_rightfirst) = 2 * ge_signed_half_add_zero_rightfirstrealdecode + 1 /\ (ge_balance_positive_add_zero_rightfirstreal) = 0) /\ (ge_balance_negative_add_zero_rightfirstreal) = S ge_signed_half_add_zero_rightfirstrealdecode))) /\ ((ge_first_rp_add_zero_right) + ge_balance_negative_add_zero_rightfirstreal = (ge_first_rn_add_zero_right) + ge_balance_positive_add_zero_rightfirstreal))) /\ (exists ge_balance_positive_add_zero_rightfirstimaginary ge_balance_negative_add_zero_rightfirstimaginary. (((((ge_representation_imaginary_code_add_zero_rightfirst) = 2 * (ge_balance_positive_add_zero_rightfirstimaginary) /\ (ge_balance_negative_add_zero_rightfirstimaginary) = 0) \/ exists ge_signed_half_add_zero_rightfirstimaginarydecode. (((ge_representation_imaginary_code_add_zero_rightfirst) = 2 * ge_signed_half_add_zero_rightfirstimaginarydecode + 1 /\ (ge_balance_positive_add_zero_rightfirstimaginary) = 0) /\ (ge_balance_negative_add_zero_rightfirstimaginary) = S ge_signed_half_add_zero_rightfirstimaginarydecode))) /\ ((ge_first_ip_add_zero_right) + ge_balance_negative_add_zero_rightfirstimaginary = (ge_first_in_add_zero_right) + ge_balance_positive_add_zero_rightfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_zero_rightsecond ge_representation_imaginary_code_add_zero_rightsecond. (((0) = ((ge_representation_real_code_add_zero_rightsecond) + (ge_representation_imaginary_code_add_zero_rightsecond)) * S ((ge_representation_real_code_add_zero_rightsecond) + (ge_representation_imaginary_code_add_zero_rightsecond)) + ((ge_representation_imaginary_code_add_zero_rightsecond) + (ge_representation_imaginary_code_add_zero_rightsecond))) /\ ((exists ge_balance_positive_add_zero_rightsecondreal ge_balance_negative_add_zero_rightsecondreal. (((((ge_representation_real_code_add_zero_rightsecond) = 2 * (ge_balance_positive_add_zero_rightsecondreal) /\ (ge_balance_negative_add_zero_rightsecondreal) = 0) \/ exists ge_signed_half_add_zero_rightsecondrealdecode. (((ge_representation_real_code_add_zero_rightsecond) = 2 * ge_signed_half_add_zero_rightsecondrealdecode + 1 /\ (ge_balance_positive_add_zero_rightsecondreal) = 0) /\ (ge_balance_negative_add_zero_rightsecondreal) = S ge_signed_half_add_zero_rightsecondrealdecode))) /\ ((ge_second_rp_add_zero_right) + ge_balance_negative_add_zero_rightsecondreal = (ge_second_rn_add_zero_right) + ge_balance_positive_add_zero_rightsecondreal))) /\ (exists ge_balance_positive_add_zero_rightsecondimaginary ge_balance_negative_add_zero_rightsecondimaginary. (((((ge_representation_imaginary_code_add_zero_rightsecond) = 2 * (ge_balance_positive_add_zero_rightsecondimaginary) /\ (ge_balance_negative_add_zero_rightsecondimaginary) = 0) \/ exists ge_signed_half_add_zero_rightsecondimaginarydecode. (((ge_representation_imaginary_code_add_zero_rightsecond) = 2 * ge_signed_half_add_zero_rightsecondimaginarydecode + 1 /\ (ge_balance_positive_add_zero_rightsecondimaginary) = 0) /\ (ge_balance_negative_add_zero_rightsecondimaginary) = S ge_signed_half_add_zero_rightsecondimaginarydecode))) /\ ((ge_second_ip_add_zero_right) + ge_balance_negative_add_zero_rightsecondimaginary = (ge_second_in_add_zero_right) + ge_balance_positive_add_zero_rightsecondimaginary)))))) /\ (exists ge_representation_real_code_add_zero_rightoutput ge_representation_imaginary_code_add_zero_rightoutput. (((a) = ((ge_representation_real_code_add_zero_rightoutput) + (ge_representation_imaginary_code_add_zero_rightoutput)) * S ((ge_representation_real_code_add_zero_rightoutput) + (ge_representation_imaginary_code_add_zero_rightoutput)) + ((ge_representation_imaginary_code_add_zero_rightoutput) + (ge_representation_imaginary_code_add_zero_rightoutput))) /\ ((exists ge_balance_positive_add_zero_rightoutputreal ge_balance_negative_add_zero_rightoutputreal. (((((ge_representation_real_code_add_zero_rightoutput) = 2 * (ge_balance_positive_add_zero_rightoutputreal) /\ (ge_balance_negative_add_zero_rightoutputreal) = 0) \/ exists ge_signed_half_add_zero_rightoutputrealdecode. (((ge_representation_real_code_add_zero_rightoutput) = 2 * ge_signed_half_add_zero_rightoutputrealdecode + 1 /\ (ge_balance_positive_add_zero_rightoutputreal) = 0) /\ (ge_balance_negative_add_zero_rightoutputreal) = S ge_signed_half_add_zero_rightoutputrealdecode))) /\ ((((ge_first_rp_add_zero_right) + (ge_second_rp_add_zero_right))) + ge_balance_negative_add_zero_rightoutputreal = (((ge_first_rn_add_zero_right) + (ge_second_rn_add_zero_right))) + ge_balance_positive_add_zero_rightoutputreal))) /\ (exists ge_balance_positive_add_zero_rightoutputimaginary ge_balance_negative_add_zero_rightoutputimaginary. (((((ge_representation_imaginary_code_add_zero_rightoutput) = 2 * (ge_balance_positive_add_zero_rightoutputimaginary) /\ (ge_balance_negative_add_zero_rightoutputimaginary) = 0) \/ exists ge_signed_half_add_zero_rightoutputimaginarydecode. (((ge_representation_imaginary_code_add_zero_rightoutput) = 2 * ge_signed_half_add_zero_rightoutputimaginarydecode + 1 /\ (ge_balance_positive_add_zero_rightoutputimaginary) = 0) /\ (ge_balance_negative_add_zero_rightoutputimaginary) = S ge_signed_half_add_zero_rightoutputimaginarydecode))) /\ ((((ge_first_ip_add_zero_right) + (ge_second_ip_add_zero_right))) + ge_balance_negative_add_zero_rightoutputimaginary = (((ge_first_in_add_zero_right) + (ge_second_in_add_zero_right))) + ge_balance_positive_add_zero_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 zero 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_add_of_representations (a)
  2. L12
    specialize gaussian_add_of_representations (0)
  3. L13
    specialize gaussian_add_of_representations (a)
  4. L14
    specialize gaussian_add_of_representations (x)
  5. L15
    specialize gaussian_add_of_representations (x1)
  6. L16
    specialize gaussian_add_of_representations (x2)
  7. L17
    specialize gaussian_add_of_representations (x3)
  8. L18
    specialize gaussian_add_of_representations (0)
  9. L19
    specialize gaussian_add_of_representations (0)
  10. L20
    specialize gaussian_add_of_representations (0)
05Use earlier factsL21–30

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

  1. L21
    specialize gaussian_add_of_representations (0)
  2. L22
    apply gaussian_add_of_representations
  3. L23
    exact hA_witness_witness_witness_witness
  4. L24
    exact gaussian_zero_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) + (0)))
06Use earlier factsL31–34

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

  1. L31
    specialize gaussian_representation_integer_transport (((x1) + (0)))
  2. L32
    specialize gaussian_representation_integer_transport (((x2) + (0)))
  3. L33
    specialize gaussian_representation_integer_transport (((x3) + (0)))
  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
  2. L37
    simp
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_add_of_representations (a)
  12. 0012specialize gaussian_add_of_representations (0)
  13. 0013specialize gaussian_add_of_representations (a)
  14. 0014specialize gaussian_add_of_representations (x)
  15. 0015specialize gaussian_add_of_representations (x1)
  16. 0016specialize gaussian_add_of_representations (x2)
  17. 0017specialize gaussian_add_of_representations (x3)
  18. 0018specialize gaussian_add_of_representations (0)
  19. 0019specialize gaussian_add_of_representations (0)
  20. 0020specialize gaussian_add_of_representations (0)
  21. 0021specialize gaussian_add_of_representations (0)
  22. 0022apply gaussian_add_of_representations
  23. 0023exact hA_witness_witness_witness_witness
  24. 0024exact gaussian_zero_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) + (0)))
  31. 0031specialize gaussian_representation_integer_transport (((x1) + (0)))
  32. 0032specialize gaussian_representation_integer_transport (((x2) + (0)))
  33. 0033specialize gaussian_representation_integer_transport (((x3) + (0)))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035split
  36. 0036simp
  37. 0037simp
  38. 0038exact hA_witness_witness_witness_witness