GF002C

gaussian_subtract_exists

Every actual Gaussian difference has a constructed canonical code solving c+b=a, without assuming a subtraction oracle.

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. ∀ b. ZPairValid(a) → ZPairValid(b) → ∃ x. ZPairAdd(x,b,a)

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

Definition DAG

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

Actual proof prerequisites

gaussian_valid_has_representationgaussian_representation_exists · checked external prerequisitegaussian_add_commutativegaussian_add_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_equal_symmetric · checked external prerequisitegaussian_difference_reconstructs_dividend · checked external prerequisite
Original expanded first-order statement 
forall a b. (exists ge_real_positive_subtract_first ge_real_negative_subtract_first ge_imaginary_positive_subtract_first ge_imaginary_negative_subtract_first. (exists ge_real_code_subtract_firstdecode ge_imaginary_code_subtract_firstdecode. (((a) = ((ge_real_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode)) * S ((ge_real_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode)) + ((ge_imaginary_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode))) /\ (((((ge_real_code_subtract_firstdecode) = 2 * (ge_real_positive_subtract_first) /\ (ge_real_negative_subtract_first) = 0) \/ exists ge_signed_half_ge_subtract_firstdecode_real. (((ge_real_code_subtract_firstdecode) = 2 * ge_signed_half_ge_subtract_firstdecode_real + 1 /\ (ge_real_positive_subtract_first) = 0) /\ (ge_real_negative_subtract_first) = S ge_signed_half_ge_subtract_firstdecode_real))) /\ ((((ge_imaginary_code_subtract_firstdecode) = 2 * (ge_imaginary_positive_subtract_first) /\ (ge_imaginary_negative_subtract_first) = 0) \/ exists ge_signed_half_ge_subtract_firstdecode_imaginary. (((ge_imaginary_code_subtract_firstdecode) = 2 * ge_signed_half_ge_subtract_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_subtract_first) = 0) /\ (ge_imaginary_negative_subtract_first) = S ge_signed_half_ge_subtract_firstdecode_imaginary))))))) -> (exists ge_real_positive_subtract_second ge_real_negative_subtract_second ge_imaginary_positive_subtract_second ge_imaginary_negative_subtract_second. (exists ge_real_code_subtract_seconddecode ge_imaginary_code_subtract_seconddecode. (((b) = ((ge_real_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode)) * S ((ge_real_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode)) + ((ge_imaginary_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode))) /\ (((((ge_real_code_subtract_seconddecode) = 2 * (ge_real_positive_subtract_second) /\ (ge_real_negative_subtract_second) = 0) \/ exists ge_signed_half_ge_subtract_seconddecode_real. (((ge_real_code_subtract_seconddecode) = 2 * ge_signed_half_ge_subtract_seconddecode_real + 1 /\ (ge_real_positive_subtract_second) = 0) /\ (ge_real_negative_subtract_second) = S ge_signed_half_ge_subtract_seconddecode_real))) /\ ((((ge_imaginary_code_subtract_seconddecode) = 2 * (ge_imaginary_positive_subtract_second) /\ (ge_imaginary_negative_subtract_second) = 0) \/ exists ge_signed_half_ge_subtract_seconddecode_imaginary. (((ge_imaginary_code_subtract_seconddecode) = 2 * ge_signed_half_ge_subtract_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_subtract_second) = 0) /\ (ge_imaginary_negative_subtract_second) = S ge_signed_half_ge_subtract_seconddecode_imaginary))))))) -> exists c. (exists ge_first_rp_subtract_equation ge_first_rn_subtract_equation ge_first_ip_subtract_equation ge_first_in_subtract_equation ge_second_rp_subtract_equation ge_second_rn_subtract_equation ge_second_ip_subtract_equation ge_second_in_subtract_equation. ((exists ge_representation_real_code_subtract_equationfirst ge_representation_imaginary_code_subtract_equationfirst. (((c) = ((ge_representation_real_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst)) * S ((ge_representation_real_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst)) + ((ge_representation_imaginary_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst))) /\ ((exists ge_balance_positive_subtract_equationfirstreal ge_balance_negative_subtract_equationfirstreal. (((((ge_representation_real_code_subtract_equationfirst) = 2 * (ge_balance_positive_subtract_equationfirstreal) /\ (ge_balance_negative_subtract_equationfirstreal) = 0) \/ exists ge_signed_half_subtract_equationfirstrealdecode. (((ge_representation_real_code_subtract_equationfirst) = 2 * ge_signed_half_subtract_equationfirstrealdecode + 1 /\ (ge_balance_positive_subtract_equationfirstreal) = 0) /\ (ge_balance_negative_subtract_equationfirstreal) = S ge_signed_half_subtract_equationfirstrealdecode))) /\ ((ge_first_rp_subtract_equation) + ge_balance_negative_subtract_equationfirstreal = (ge_first_rn_subtract_equation) + ge_balance_positive_subtract_equationfirstreal))) /\ (exists ge_balance_positive_subtract_equationfirstimaginary ge_balance_negative_subtract_equationfirstimaginary. (((((ge_representation_imaginary_code_subtract_equationfirst) = 2 * (ge_balance_positive_subtract_equationfirstimaginary) /\ (ge_balance_negative_subtract_equationfirstimaginary) = 0) \/ exists ge_signed_half_subtract_equationfirstimaginarydecode. (((ge_representation_imaginary_code_subtract_equationfirst) = 2 * ge_signed_half_subtract_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationfirstimaginary) = 0) /\ (ge_balance_negative_subtract_equationfirstimaginary) = S ge_signed_half_subtract_equationfirstimaginarydecode))) /\ ((ge_first_ip_subtract_equation) + ge_balance_negative_subtract_equationfirstimaginary = (ge_first_in_subtract_equation) + ge_balance_positive_subtract_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_subtract_equationsecond ge_representation_imaginary_code_subtract_equationsecond. (((b) = ((ge_representation_real_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond)) * S ((ge_representation_real_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond)) + ((ge_representation_imaginary_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond))) /\ ((exists ge_balance_positive_subtract_equationsecondreal ge_balance_negative_subtract_equationsecondreal. (((((ge_representation_real_code_subtract_equationsecond) = 2 * (ge_balance_positive_subtract_equationsecondreal) /\ (ge_balance_negative_subtract_equationsecondreal) = 0) \/ exists ge_signed_half_subtract_equationsecondrealdecode. (((ge_representation_real_code_subtract_equationsecond) = 2 * ge_signed_half_subtract_equationsecondrealdecode + 1 /\ (ge_balance_positive_subtract_equationsecondreal) = 0) /\ (ge_balance_negative_subtract_equationsecondreal) = S ge_signed_half_subtract_equationsecondrealdecode))) /\ ((ge_second_rp_subtract_equation) + ge_balance_negative_subtract_equationsecondreal = (ge_second_rn_subtract_equation) + ge_balance_positive_subtract_equationsecondreal))) /\ (exists ge_balance_positive_subtract_equationsecondimaginary ge_balance_negative_subtract_equationsecondimaginary. (((((ge_representation_imaginary_code_subtract_equationsecond) = 2 * (ge_balance_positive_subtract_equationsecondimaginary) /\ (ge_balance_negative_subtract_equationsecondimaginary) = 0) \/ exists ge_signed_half_subtract_equationsecondimaginarydecode. (((ge_representation_imaginary_code_subtract_equationsecond) = 2 * ge_signed_half_subtract_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationsecondimaginary) = 0) /\ (ge_balance_negative_subtract_equationsecondimaginary) = S ge_signed_half_subtract_equationsecondimaginarydecode))) /\ ((ge_second_ip_subtract_equation) + ge_balance_negative_subtract_equationsecondimaginary = (ge_second_in_subtract_equation) + ge_balance_positive_subtract_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_subtract_equationoutput ge_representation_imaginary_code_subtract_equationoutput. (((a) = ((ge_representation_real_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput)) * S ((ge_representation_real_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput)) + ((ge_representation_imaginary_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput))) /\ ((exists ge_balance_positive_subtract_equationoutputreal ge_balance_negative_subtract_equationoutputreal. (((((ge_representation_real_code_subtract_equationoutput) = 2 * (ge_balance_positive_subtract_equationoutputreal) /\ (ge_balance_negative_subtract_equationoutputreal) = 0) \/ exists ge_signed_half_subtract_equationoutputrealdecode. (((ge_representation_real_code_subtract_equationoutput) = 2 * ge_signed_half_subtract_equationoutputrealdecode + 1 /\ (ge_balance_positive_subtract_equationoutputreal) = 0) /\ (ge_balance_negative_subtract_equationoutputreal) = S ge_signed_half_subtract_equationoutputrealdecode))) /\ ((((ge_first_rp_subtract_equation) + (ge_second_rp_subtract_equation))) + ge_balance_negative_subtract_equationoutputreal = (((ge_first_rn_subtract_equation) + (ge_second_rn_subtract_equation))) + ge_balance_positive_subtract_equationoutputreal))) /\ (exists ge_balance_positive_subtract_equationoutputimaginary ge_balance_negative_subtract_equationoutputimaginary. (((((ge_representation_imaginary_code_subtract_equationoutput) = 2 * (ge_balance_positive_subtract_equationoutputimaginary) /\ (ge_balance_negative_subtract_equationoutputimaginary) = 0) \/ exists ge_signed_half_subtract_equationoutputimaginarydecode. (((ge_representation_imaginary_code_subtract_equationoutput) = 2 * ge_signed_half_subtract_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationoutputimaginary) = 0) /\ (ge_balance_negative_subtract_equationoutputimaginary) = S ge_signed_half_subtract_equationoutputimaginarydecode))) /\ ((((ge_first_ip_subtract_equation) + (ge_second_ip_subtract_equation))) + ge_balance_negative_subtract_equationoutputimaginary = (((ge_first_in_subtract_equation) + (ge_second_in_subtract_equation))) + ge_balance_positive_subtract_equationoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

75 script commands · 13 reading checkpoints · 3 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 add commutative
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro ha
  4. L4
    intro hb
02Establish hAL5–8

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

  1. L5
    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. L6
    specialize gaussian_valid_has_representation (a)
  3. L7
    apply gaussian_valid_has_representation
  4. L8
    exact ha
03Separate the logical casesL9–12

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

  1. L9
    cases hA
  2. L10
    cases hA_witness
  3. L11
    cases hA_witness_witness
  4. L12
    cases hA_witness_witness_witness
04Establish hBL13–16

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

  1. L13
    have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)Definitions: ZPairRep(b,rp,rn,ip,inn)Original native command in the exact edition
  2. L14
    specialize gaussian_valid_has_representation (b)
  3. L15
    apply gaussian_valid_has_representation
  4. L16
    exact hb
05Separate the logical casesL17–20

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

  1. L17
    cases hB
  2. L18
    cases hB_witness
  3. L19
    cases hB_witness_witness
  4. L20
    cases hB_witness_witness_witness
06Establish hCL21–26

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

  1. L21
    have hC : ∃ c. ZPairRep(c,x + x5,x1 + x4,x2 + x7,x3 + x6)Definitions: ZPairRep(c,x + x5,x1 + x4,x2 + x7,x3 + x6)Original native command in the exact edition
  2. L22
    specialize gaussian_representation_exists (((x) + (x5)))
  3. L23
    specialize gaussian_representation_exists (((x1) + (x4)))
  4. L24
    specialize gaussian_representation_exists (((x2) + (x7)))
  5. L25
    specialize gaussian_representation_exists (((x3) + (x6)))
  6. L26
    apply gaussian_representation_exists
07Separate the logical casesL27–27

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

  1. L27
    cases hC
08Construct an explicit witnessL28–28

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

  1. L28
    exists (x8)
09Use earlier factsL29–38

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

  1. L29
    specialize gaussian_add_commutative (b)
  2. L30
    specialize gaussian_add_commutative (x8)
  3. L31
    specialize gaussian_add_commutative (a)
  4. L32
    apply gaussian_add_commutative
  5. L33
    specialize gaussian_add_of_representations (b)
  6. L34
    specialize gaussian_add_of_representations (x8)
  7. L35
    specialize gaussian_add_of_representations (a)
  8. L36
    specialize gaussian_add_of_representations (x4)
  9. L37
    specialize gaussian_add_of_representations (x5)
  10. L38
    specialize gaussian_add_of_representations (x6)
10Use earlier factsL39–48

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

  1. L39
    specialize gaussian_add_of_representations (x7)
  2. L40
    specialize gaussian_add_of_representations (((x) + (x5)))
  3. L41
    specialize gaussian_add_of_representations (((x1) + (x4)))
  4. L42
    specialize gaussian_add_of_representations (((x2) + (x7)))
  5. L43
    specialize gaussian_add_of_representations (((x3) + (x6)))
  6. L44
    apply gaussian_add_of_representations
  7. L45
    exact hB_witness_witness_witness_witness
  8. L46
    exact hC_witness
  9. L47
    specialize gaussian_representation_integer_transport (a)
  10. L48
    specialize gaussian_representation_integer_transport (x)
11Use earlier factsL49–58

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

  1. L49
    specialize gaussian_representation_integer_transport (x1)
  2. L50
    specialize gaussian_representation_integer_transport (x2)
  3. L51
    specialize gaussian_representation_integer_transport (x3)
  4. L52
    specialize gaussian_representation_integer_transport (((x4) + (((x) + (x5)))))
  5. L53
    specialize gaussian_representation_integer_transport (((x5) + (((x1) + (x4)))))
  6. L54
    specialize gaussian_representation_integer_transport (((x6) + (((x2) + (x7)))))
  7. L55
    specialize gaussian_representation_integer_transport (((x7) + (((x3) + (x6)))))
  8. L56
    apply gaussian_representation_integer_transport
  9. L57
    specialize gaussian_equal_symmetric (((x4) + (((x) + (x5)))))
  10. L58
    specialize gaussian_equal_symmetric (((x5) + (((x1) + (x4)))))
12Use earlier factsL59–68

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

  1. L59
    specialize gaussian_equal_symmetric (((x6) + (((x2) + (x7)))))
  2. L60
    specialize gaussian_equal_symmetric (((x7) + (((x3) + (x6)))))
  3. L61
    specialize gaussian_equal_symmetric (x)
  4. L62
    specialize gaussian_equal_symmetric (x1)
  5. L63
    specialize gaussian_equal_symmetric (x2)
  6. L64
    specialize gaussian_equal_symmetric (x3)
  7. L65
    apply gaussian_equal_symmetric
  8. L66
    specialize gaussian_difference_reconstructs_dividend (x)
  9. L67
    specialize gaussian_difference_reconstructs_dividend (x1)
  10. L68
    specialize gaussian_difference_reconstructs_dividend (x2)
13Use earlier factsL69–75

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

  1. L69
    specialize gaussian_difference_reconstructs_dividend (x3)
  2. L70
    specialize gaussian_difference_reconstructs_dividend (x4)
  3. L71
    specialize gaussian_difference_reconstructs_dividend (x5)
  4. L72
    specialize gaussian_difference_reconstructs_dividend (x6)
  5. L73
    specialize gaussian_difference_reconstructs_dividend (x7)
  6. L74
    apply gaussian_difference_reconstructs_dividend
  7. L75
    exact hA_witness_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro ha
  4. 0004intro hb
  5. 0005have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  6. 0006specialize gaussian_valid_has_representation (a)
  7. 0007apply gaussian_valid_has_representation
  8. 0008exact ha
  9. 0009cases hA
  10. 0010cases hA_witness
  11. 0011cases hA_witness_witness
  12. 0012cases hA_witness_witness_witness
  13. 0013have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)
  14. 0014specialize gaussian_valid_has_representation (b)
  15. 0015apply gaussian_valid_has_representation
  16. 0016exact hb
  17. 0017cases hB
  18. 0018cases hB_witness
  19. 0019cases hB_witness_witness
  20. 0020cases hB_witness_witness_witness
  21. 0021have hC : ∃ c. ZPairRep(c,x + x5,x1 + x4,x2 + x7,x3 + x6)
  22. 0022specialize gaussian_representation_exists (((x) + (x5)))
  23. 0023specialize gaussian_representation_exists (((x1) + (x4)))
  24. 0024specialize gaussian_representation_exists (((x2) + (x7)))
  25. 0025specialize gaussian_representation_exists (((x3) + (x6)))
  26. 0026apply gaussian_representation_exists
  27. 0027cases hC
  28. 0028exists (x8)
  29. 0029specialize gaussian_add_commutative (b)
  30. 0030specialize gaussian_add_commutative (x8)
  31. 0031specialize gaussian_add_commutative (a)
  32. 0032apply gaussian_add_commutative
  33. 0033specialize gaussian_add_of_representations (b)
  34. 0034specialize gaussian_add_of_representations (x8)
  35. 0035specialize gaussian_add_of_representations (a)
  36. 0036specialize gaussian_add_of_representations (x4)
  37. 0037specialize gaussian_add_of_representations (x5)
  38. 0038specialize gaussian_add_of_representations (x6)
  39. 0039specialize gaussian_add_of_representations (x7)
  40. 0040specialize gaussian_add_of_representations (((x) + (x5)))
  41. 0041specialize gaussian_add_of_representations (((x1) + (x4)))
  42. 0042specialize gaussian_add_of_representations (((x2) + (x7)))
  43. 0043specialize gaussian_add_of_representations (((x3) + (x6)))
  44. 0044apply gaussian_add_of_representations
  45. 0045exact hB_witness_witness_witness_witness
  46. 0046exact hC_witness
  47. 0047specialize gaussian_representation_integer_transport (a)
  48. 0048specialize gaussian_representation_integer_transport (x)
  49. 0049specialize gaussian_representation_integer_transport (x1)
  50. 0050specialize gaussian_representation_integer_transport (x2)
  51. 0051specialize gaussian_representation_integer_transport (x3)
  52. 0052specialize gaussian_representation_integer_transport (((x4) + (((x) + (x5)))))
  53. 0053specialize gaussian_representation_integer_transport (((x5) + (((x1) + (x4)))))
  54. 0054specialize gaussian_representation_integer_transport (((x6) + (((x2) + (x7)))))
  55. 0055specialize gaussian_representation_integer_transport (((x7) + (((x3) + (x6)))))
  56. 0056apply gaussian_representation_integer_transport
  57. 0057specialize gaussian_equal_symmetric (((x4) + (((x) + (x5)))))
  58. 0058specialize gaussian_equal_symmetric (((x5) + (((x1) + (x4)))))
  59. 0059specialize gaussian_equal_symmetric (((x6) + (((x2) + (x7)))))
  60. 0060specialize gaussian_equal_symmetric (((x7) + (((x3) + (x6)))))
  61. 0061specialize gaussian_equal_symmetric (x)
  62. 0062specialize gaussian_equal_symmetric (x1)
  63. 0063specialize gaussian_equal_symmetric (x2)
  64. 0064specialize gaussian_equal_symmetric (x3)
  65. 0065apply gaussian_equal_symmetric
  66. 0066specialize gaussian_difference_reconstructs_dividend (x)
  67. 0067specialize gaussian_difference_reconstructs_dividend (x1)
  68. 0068specialize gaussian_difference_reconstructs_dividend (x2)
  69. 0069specialize gaussian_difference_reconstructs_dividend (x3)
  70. 0070specialize gaussian_difference_reconstructs_dividend (x4)
  71. 0071specialize gaussian_difference_reconstructs_dividend (x5)
  72. 0072specialize gaussian_difference_reconstructs_dividend (x6)
  73. 0073specialize gaussian_difference_reconstructs_dividend (x7)
  74. 0074apply gaussian_difference_reconstructs_dividend
  75. 0075exact hA_witness_witness_witness_witness