GI0055

gaussian_add_exists

Construct an actual canonical Gaussian add output for every pair of valid canonical Gaussian inputs.

Alpha v34 checked-use · first admitted v28 · 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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ZPairValid(ac) → ZPairValid(bc) → ∃ x. ZPairAdd(ac,bc,x)

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

Definition DAG

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

Actual proof prerequisites

gaussian_representation_existsgaussian_add_of_representationsgaussian_decode_representation
Original expanded first-order statement 
forall ac bc. (exists ge_real_positive_add_total_first ge_real_negative_add_total_first ge_imaginary_positive_add_total_first ge_imaginary_negative_add_total_first. (exists ge_real_code_add_total_firstdecode ge_imaginary_code_add_total_firstdecode. (((ac) = ((ge_real_code_add_total_firstdecode) + (ge_imaginary_code_add_total_firstdecode)) * S ((ge_real_code_add_total_firstdecode) + (ge_imaginary_code_add_total_firstdecode)) + ((ge_imaginary_code_add_total_firstdecode) + (ge_imaginary_code_add_total_firstdecode))) /\ (((((ge_real_code_add_total_firstdecode) = 2 * (ge_real_positive_add_total_first) /\ (ge_real_negative_add_total_first) = 0) \/ exists ge_signed_half_ge_add_total_firstdecode_real. (((ge_real_code_add_total_firstdecode) = 2 * ge_signed_half_ge_add_total_firstdecode_real + 1 /\ (ge_real_positive_add_total_first) = 0) /\ (ge_real_negative_add_total_first) = S ge_signed_half_ge_add_total_firstdecode_real))) /\ ((((ge_imaginary_code_add_total_firstdecode) = 2 * (ge_imaginary_positive_add_total_first) /\ (ge_imaginary_negative_add_total_first) = 0) \/ exists ge_signed_half_ge_add_total_firstdecode_imaginary. (((ge_imaginary_code_add_total_firstdecode) = 2 * ge_signed_half_ge_add_total_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_add_total_first) = 0) /\ (ge_imaginary_negative_add_total_first) = S ge_signed_half_ge_add_total_firstdecode_imaginary))))))) -> (exists ge_real_positive_add_total_second ge_real_negative_add_total_second ge_imaginary_positive_add_total_second ge_imaginary_negative_add_total_second. (exists ge_real_code_add_total_seconddecode ge_imaginary_code_add_total_seconddecode. (((bc) = ((ge_real_code_add_total_seconddecode) + (ge_imaginary_code_add_total_seconddecode)) * S ((ge_real_code_add_total_seconddecode) + (ge_imaginary_code_add_total_seconddecode)) + ((ge_imaginary_code_add_total_seconddecode) + (ge_imaginary_code_add_total_seconddecode))) /\ (((((ge_real_code_add_total_seconddecode) = 2 * (ge_real_positive_add_total_second) /\ (ge_real_negative_add_total_second) = 0) \/ exists ge_signed_half_ge_add_total_seconddecode_real. (((ge_real_code_add_total_seconddecode) = 2 * ge_signed_half_ge_add_total_seconddecode_real + 1 /\ (ge_real_positive_add_total_second) = 0) /\ (ge_real_negative_add_total_second) = S ge_signed_half_ge_add_total_seconddecode_real))) /\ ((((ge_imaginary_code_add_total_seconddecode) = 2 * (ge_imaginary_positive_add_total_second) /\ (ge_imaginary_negative_add_total_second) = 0) \/ exists ge_signed_half_ge_add_total_seconddecode_imaginary. (((ge_imaginary_code_add_total_seconddecode) = 2 * ge_signed_half_ge_add_total_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_add_total_second) = 0) /\ (ge_imaginary_negative_add_total_second) = S ge_signed_half_ge_add_total_seconddecode_imaginary))))))) -> exists cc. (exists ge_first_rp_add_total_output ge_first_rn_add_total_output ge_first_ip_add_total_output ge_first_in_add_total_output ge_second_rp_add_total_output ge_second_rn_add_total_output ge_second_ip_add_total_output ge_second_in_add_total_output. ((exists ge_representation_real_code_add_total_outputfirst ge_representation_imaginary_code_add_total_outputfirst. (((ac) = ((ge_representation_real_code_add_total_outputfirst) + (ge_representation_imaginary_code_add_total_outputfirst)) * S ((ge_representation_real_code_add_total_outputfirst) + (ge_representation_imaginary_code_add_total_outputfirst)) + ((ge_representation_imaginary_code_add_total_outputfirst) + (ge_representation_imaginary_code_add_total_outputfirst))) /\ ((exists ge_balance_positive_add_total_outputfirstreal ge_balance_negative_add_total_outputfirstreal. (((((ge_representation_real_code_add_total_outputfirst) = 2 * (ge_balance_positive_add_total_outputfirstreal) /\ (ge_balance_negative_add_total_outputfirstreal) = 0) \/ exists ge_signed_half_add_total_outputfirstrealdecode. (((ge_representation_real_code_add_total_outputfirst) = 2 * ge_signed_half_add_total_outputfirstrealdecode + 1 /\ (ge_balance_positive_add_total_outputfirstreal) = 0) /\ (ge_balance_negative_add_total_outputfirstreal) = S ge_signed_half_add_total_outputfirstrealdecode))) /\ ((ge_first_rp_add_total_output) + ge_balance_negative_add_total_outputfirstreal = (ge_first_rn_add_total_output) + ge_balance_positive_add_total_outputfirstreal))) /\ (exists ge_balance_positive_add_total_outputfirstimaginary ge_balance_negative_add_total_outputfirstimaginary. (((((ge_representation_imaginary_code_add_total_outputfirst) = 2 * (ge_balance_positive_add_total_outputfirstimaginary) /\ (ge_balance_negative_add_total_outputfirstimaginary) = 0) \/ exists ge_signed_half_add_total_outputfirstimaginarydecode. (((ge_representation_imaginary_code_add_total_outputfirst) = 2 * ge_signed_half_add_total_outputfirstimaginarydecode + 1 /\ (ge_balance_positive_add_total_outputfirstimaginary) = 0) /\ (ge_balance_negative_add_total_outputfirstimaginary) = S ge_signed_half_add_total_outputfirstimaginarydecode))) /\ ((ge_first_ip_add_total_output) + ge_balance_negative_add_total_outputfirstimaginary = (ge_first_in_add_total_output) + ge_balance_positive_add_total_outputfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_total_outputsecond ge_representation_imaginary_code_add_total_outputsecond. (((bc) = ((ge_representation_real_code_add_total_outputsecond) + (ge_representation_imaginary_code_add_total_outputsecond)) * S ((ge_representation_real_code_add_total_outputsecond) + (ge_representation_imaginary_code_add_total_outputsecond)) + ((ge_representation_imaginary_code_add_total_outputsecond) + (ge_representation_imaginary_code_add_total_outputsecond))) /\ ((exists ge_balance_positive_add_total_outputsecondreal ge_balance_negative_add_total_outputsecondreal. (((((ge_representation_real_code_add_total_outputsecond) = 2 * (ge_balance_positive_add_total_outputsecondreal) /\ (ge_balance_negative_add_total_outputsecondreal) = 0) \/ exists ge_signed_half_add_total_outputsecondrealdecode. (((ge_representation_real_code_add_total_outputsecond) = 2 * ge_signed_half_add_total_outputsecondrealdecode + 1 /\ (ge_balance_positive_add_total_outputsecondreal) = 0) /\ (ge_balance_negative_add_total_outputsecondreal) = S ge_signed_half_add_total_outputsecondrealdecode))) /\ ((ge_second_rp_add_total_output) + ge_balance_negative_add_total_outputsecondreal = (ge_second_rn_add_total_output) + ge_balance_positive_add_total_outputsecondreal))) /\ (exists ge_balance_positive_add_total_outputsecondimaginary ge_balance_negative_add_total_outputsecondimaginary. (((((ge_representation_imaginary_code_add_total_outputsecond) = 2 * (ge_balance_positive_add_total_outputsecondimaginary) /\ (ge_balance_negative_add_total_outputsecondimaginary) = 0) \/ exists ge_signed_half_add_total_outputsecondimaginarydecode. (((ge_representation_imaginary_code_add_total_outputsecond) = 2 * ge_signed_half_add_total_outputsecondimaginarydecode + 1 /\ (ge_balance_positive_add_total_outputsecondimaginary) = 0) /\ (ge_balance_negative_add_total_outputsecondimaginary) = S ge_signed_half_add_total_outputsecondimaginarydecode))) /\ ((ge_second_ip_add_total_output) + ge_balance_negative_add_total_outputsecondimaginary = (ge_second_in_add_total_output) + ge_balance_positive_add_total_outputsecondimaginary)))))) /\ (exists ge_representation_real_code_add_total_outputoutput ge_representation_imaginary_code_add_total_outputoutput. (((cc) = ((ge_representation_real_code_add_total_outputoutput) + (ge_representation_imaginary_code_add_total_outputoutput)) * S ((ge_representation_real_code_add_total_outputoutput) + (ge_representation_imaginary_code_add_total_outputoutput)) + ((ge_representation_imaginary_code_add_total_outputoutput) + (ge_representation_imaginary_code_add_total_outputoutput))) /\ ((exists ge_balance_positive_add_total_outputoutputreal ge_balance_negative_add_total_outputoutputreal. (((((ge_representation_real_code_add_total_outputoutput) = 2 * (ge_balance_positive_add_total_outputoutputreal) /\ (ge_balance_negative_add_total_outputoutputreal) = 0) \/ exists ge_signed_half_add_total_outputoutputrealdecode. (((ge_representation_real_code_add_total_outputoutput) = 2 * ge_signed_half_add_total_outputoutputrealdecode + 1 /\ (ge_balance_positive_add_total_outputoutputreal) = 0) /\ (ge_balance_negative_add_total_outputoutputreal) = S ge_signed_half_add_total_outputoutputrealdecode))) /\ ((((ge_first_rp_add_total_output) + (ge_second_rp_add_total_output))) + ge_balance_negative_add_total_outputoutputreal = (((ge_first_rn_add_total_output) + (ge_second_rn_add_total_output))) + ge_balance_positive_add_total_outputoutputreal))) /\ (exists ge_balance_positive_add_total_outputoutputimaginary ge_balance_negative_add_total_outputoutputimaginary. (((((ge_representation_imaginary_code_add_total_outputoutput) = 2 * (ge_balance_positive_add_total_outputoutputimaginary) /\ (ge_balance_negative_add_total_outputoutputimaginary) = 0) \/ exists ge_signed_half_add_total_outputoutputimaginarydecode. (((ge_representation_imaginary_code_add_total_outputoutput) = 2 * ge_signed_half_add_total_outputoutputimaginarydecode + 1 /\ (ge_balance_positive_add_total_outputoutputimaginary) = 0) /\ (ge_balance_negative_add_total_outputoutputimaginary) = S ge_signed_half_add_total_outputoutputimaginarydecode))) /\ ((((ge_first_ip_add_total_output) + (ge_second_ip_add_total_output))) + ge_balance_negative_add_total_outputoutputimaginary = (((ge_first_in_add_total_output) + (ge_second_in_add_total_output))) + ge_balance_positive_add_total_outputoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

47 script commands · 8 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 (3)
gaussian representation existsgaussian add of representationsgaussian decode representation
01Fix variables and assumptionsL1–4

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro hfirst
  4. L4
    intro hsecond
02Separate the logical casesL5–12

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

  1. L5
    cases hfirst
  2. L6
    cases hfirst_witness
  3. L7
    cases hfirst_witness_witness
  4. L8
    cases hfirst_witness_witness_witness
  5. L9
    cases hsecond
  6. L10
    cases hsecond_witness
  7. L11
    cases hsecond_witness_witness
  8. L12
    cases hsecond_witness_witness_witness
03Establish houtputL13–18

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

  1. L13
    have houtput : ∃ cc. ZPairRep(cc,x + x4,x1 + x5,x2 + x6,x3 + x7)Definitions: ZPairRep(cc,x + x4,x1 + x5,x2 + x6,x3 + x7)Original native command in the exact edition
  2. L14
    specialize gaussian_representation_exists ((x) + (x4))
  3. L15
    specialize gaussian_representation_exists ((x1) + (x5))
  4. L16
    specialize gaussian_representation_exists ((x2) + (x6))
  5. L17
    specialize gaussian_representation_exists ((x3) + (x7))
  6. L18
    apply gaussian_representation_exists
04Separate the logical casesL19–19

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

  1. L19
    cases houtput
05Construct an explicit witnessL20–20

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

  1. L20
    exists x8
06Use earlier factsL21–30

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

  1. L21
    specialize gaussian_add_of_representations ac
  2. L22
    specialize gaussian_add_of_representations bc
  3. L23
    specialize gaussian_add_of_representations x8
  4. L24
    specialize gaussian_add_of_representations x
  5. L25
    specialize gaussian_add_of_representations x1
  6. L26
    specialize gaussian_add_of_representations x2
  7. L27
    specialize gaussian_add_of_representations x3
  8. L28
    specialize gaussian_add_of_representations x4
  9. L29
    specialize gaussian_add_of_representations x5
  10. L30
    specialize gaussian_add_of_representations x6
07Use earlier factsL31–40

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

  1. L31
    specialize gaussian_add_of_representations x7
  2. L32
    apply gaussian_add_of_representations
  3. L33
    specialize gaussian_decode_representation ac
  4. L34
    specialize gaussian_decode_representation x
  5. L35
    specialize gaussian_decode_representation x1
  6. L36
    specialize gaussian_decode_representation x2
  7. L37
    specialize gaussian_decode_representation x3
  8. L38
    apply gaussian_decode_representation
  9. L39
    exact hfirst_witness_witness_witness_witness
  10. L40
    specialize gaussian_decode_representation bc
08Use earlier factsL41–47

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

  1. L41
    specialize gaussian_decode_representation x4
  2. L42
    specialize gaussian_decode_representation x5
  3. L43
    specialize gaussian_decode_representation x6
  4. L44
    specialize gaussian_decode_representation x7
  5. L45
    apply gaussian_decode_representation
  6. L46
    exact hsecond_witness_witness_witness_witness
  7. L47
    exact houtput_witness

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro hfirst
  4. 0004intro hsecond
  5. 0005cases hfirst
  6. 0006cases hfirst_witness
  7. 0007cases hfirst_witness_witness
  8. 0008cases hfirst_witness_witness_witness
  9. 0009cases hsecond
  10. 0010cases hsecond_witness
  11. 0011cases hsecond_witness_witness
  12. 0012cases hsecond_witness_witness_witness
  13. 0013have houtput : ∃ cc. ZPairRep(cc,x + x4,x1 + x5,x2 + x6,x3 + x7)
  14. 0014specialize gaussian_representation_exists ((x) + (x4))
  15. 0015specialize gaussian_representation_exists ((x1) + (x5))
  16. 0016specialize gaussian_representation_exists ((x2) + (x6))
  17. 0017specialize gaussian_representation_exists ((x3) + (x7))
  18. 0018apply gaussian_representation_exists
  19. 0019cases houtput
  20. 0020exists x8
  21. 0021specialize gaussian_add_of_representations ac
  22. 0022specialize gaussian_add_of_representations bc
  23. 0023specialize gaussian_add_of_representations x8
  24. 0024specialize gaussian_add_of_representations x
  25. 0025specialize gaussian_add_of_representations x1
  26. 0026specialize gaussian_add_of_representations x2
  27. 0027specialize gaussian_add_of_representations x3
  28. 0028specialize gaussian_add_of_representations x4
  29. 0029specialize gaussian_add_of_representations x5
  30. 0030specialize gaussian_add_of_representations x6
  31. 0031specialize gaussian_add_of_representations x7
  32. 0032apply gaussian_add_of_representations
  33. 0033specialize gaussian_decode_representation ac
  34. 0034specialize gaussian_decode_representation x
  35. 0035specialize gaussian_decode_representation x1
  36. 0036specialize gaussian_decode_representation x2
  37. 0037specialize gaussian_decode_representation x3
  38. 0038apply gaussian_decode_representation
  39. 0039exact hfirst_witness_witness_witness_witness
  40. 0040specialize gaussian_decode_representation bc
  41. 0041specialize gaussian_decode_representation x4
  42. 0042specialize gaussian_decode_representation x5
  43. 0043specialize gaussian_decode_representation x6
  44. 0044specialize gaussian_decode_representation x7
  45. 0045apply gaussian_decode_representation
  46. 0046exact hsecond_witness_witness_witness_witness
  47. 0047exact houtput_witness