GF002D

gaussian_add_cancel_left

The actual canonical Gaussian additive operation is cancellative, proved in both signed coordinates.

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. ∀ c. ∀ t. ZPairAdd(a,b,t) → ZPairAdd(a,c,t) → b = c

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

Definition DAG

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

Actual proof prerequisites

gaussian_valid_has_representationgaussian_add_input_left_validgaussian_add_input_right_validgaussian_add_for_representations · checked external prerequisitegaussian_codes_equal_of_representationsgaussian_ring_raw_add_cancel_leftgaussian_representation_equal · checked external prerequisite
Original expanded first-order statement 
forall a b c t. (exists ge_first_rp_cancel_first ge_first_rn_cancel_first ge_first_ip_cancel_first ge_first_in_cancel_first ge_second_rp_cancel_first ge_second_rn_cancel_first ge_second_ip_cancel_first ge_second_in_cancel_first. ((exists ge_representation_real_code_cancel_firstfirst ge_representation_imaginary_code_cancel_firstfirst. (((a) = ((ge_representation_real_code_cancel_firstfirst) + (ge_representation_imaginary_code_cancel_firstfirst)) * S ((ge_representation_real_code_cancel_firstfirst) + (ge_representation_imaginary_code_cancel_firstfirst)) + ((ge_representation_imaginary_code_cancel_firstfirst) + (ge_representation_imaginary_code_cancel_firstfirst))) /\ ((exists ge_balance_positive_cancel_firstfirstreal ge_balance_negative_cancel_firstfirstreal. (((((ge_representation_real_code_cancel_firstfirst) = 2 * (ge_balance_positive_cancel_firstfirstreal) /\ (ge_balance_negative_cancel_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_firstfirstrealdecode. (((ge_representation_real_code_cancel_firstfirst) = 2 * ge_signed_half_cancel_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_firstfirstreal) = S ge_signed_half_cancel_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_first) + ge_balance_negative_cancel_firstfirstreal = (ge_first_rn_cancel_first) + ge_balance_positive_cancel_firstfirstreal))) /\ (exists ge_balance_positive_cancel_firstfirstimaginary ge_balance_negative_cancel_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_firstfirst) = 2 * (ge_balance_positive_cancel_firstfirstimaginary) /\ (ge_balance_negative_cancel_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_firstfirst) = 2 * ge_signed_half_cancel_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_firstfirstimaginary) = S ge_signed_half_cancel_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_first) + ge_balance_negative_cancel_firstfirstimaginary = (ge_first_in_cancel_first) + ge_balance_positive_cancel_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_firstsecond ge_representation_imaginary_code_cancel_firstsecond. (((b) = ((ge_representation_real_code_cancel_firstsecond) + (ge_representation_imaginary_code_cancel_firstsecond)) * S ((ge_representation_real_code_cancel_firstsecond) + (ge_representation_imaginary_code_cancel_firstsecond)) + ((ge_representation_imaginary_code_cancel_firstsecond) + (ge_representation_imaginary_code_cancel_firstsecond))) /\ ((exists ge_balance_positive_cancel_firstsecondreal ge_balance_negative_cancel_firstsecondreal. (((((ge_representation_real_code_cancel_firstsecond) = 2 * (ge_balance_positive_cancel_firstsecondreal) /\ (ge_balance_negative_cancel_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_firstsecondrealdecode. (((ge_representation_real_code_cancel_firstsecond) = 2 * ge_signed_half_cancel_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_firstsecondreal) = S ge_signed_half_cancel_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_first) + ge_balance_negative_cancel_firstsecondreal = (ge_second_rn_cancel_first) + ge_balance_positive_cancel_firstsecondreal))) /\ (exists ge_balance_positive_cancel_firstsecondimaginary ge_balance_negative_cancel_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_firstsecond) = 2 * (ge_balance_positive_cancel_firstsecondimaginary) /\ (ge_balance_negative_cancel_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_firstsecond) = 2 * ge_signed_half_cancel_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_firstsecondimaginary) = S ge_signed_half_cancel_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_first) + ge_balance_negative_cancel_firstsecondimaginary = (ge_second_in_cancel_first) + ge_balance_positive_cancel_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_firstoutput ge_representation_imaginary_code_cancel_firstoutput. (((t) = ((ge_representation_real_code_cancel_firstoutput) + (ge_representation_imaginary_code_cancel_firstoutput)) * S ((ge_representation_real_code_cancel_firstoutput) + (ge_representation_imaginary_code_cancel_firstoutput)) + ((ge_representation_imaginary_code_cancel_firstoutput) + (ge_representation_imaginary_code_cancel_firstoutput))) /\ ((exists ge_balance_positive_cancel_firstoutputreal ge_balance_negative_cancel_firstoutputreal. (((((ge_representation_real_code_cancel_firstoutput) = 2 * (ge_balance_positive_cancel_firstoutputreal) /\ (ge_balance_negative_cancel_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_firstoutputrealdecode. (((ge_representation_real_code_cancel_firstoutput) = 2 * ge_signed_half_cancel_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_firstoutputreal) = S ge_signed_half_cancel_firstoutputrealdecode))) /\ ((((ge_first_rp_cancel_first) + (ge_second_rp_cancel_first))) + ge_balance_negative_cancel_firstoutputreal = (((ge_first_rn_cancel_first) + (ge_second_rn_cancel_first))) + ge_balance_positive_cancel_firstoutputreal))) /\ (exists ge_balance_positive_cancel_firstoutputimaginary ge_balance_negative_cancel_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_firstoutput) = 2 * (ge_balance_positive_cancel_firstoutputimaginary) /\ (ge_balance_negative_cancel_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_firstoutput) = 2 * ge_signed_half_cancel_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_firstoutputimaginary) = S ge_signed_half_cancel_firstoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_first) + (ge_second_ip_cancel_first))) + ge_balance_negative_cancel_firstoutputimaginary = (((ge_first_in_cancel_first) + (ge_second_in_cancel_first))) + ge_balance_positive_cancel_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_second ge_first_rn_cancel_second ge_first_ip_cancel_second ge_first_in_cancel_second ge_second_rp_cancel_second ge_second_rn_cancel_second ge_second_ip_cancel_second ge_second_in_cancel_second. ((exists ge_representation_real_code_cancel_secondfirst ge_representation_imaginary_code_cancel_secondfirst. (((a) = ((ge_representation_real_code_cancel_secondfirst) + (ge_representation_imaginary_code_cancel_secondfirst)) * S ((ge_representation_real_code_cancel_secondfirst) + (ge_representation_imaginary_code_cancel_secondfirst)) + ((ge_representation_imaginary_code_cancel_secondfirst) + (ge_representation_imaginary_code_cancel_secondfirst))) /\ ((exists ge_balance_positive_cancel_secondfirstreal ge_balance_negative_cancel_secondfirstreal. (((((ge_representation_real_code_cancel_secondfirst) = 2 * (ge_balance_positive_cancel_secondfirstreal) /\ (ge_balance_negative_cancel_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_secondfirstrealdecode. (((ge_representation_real_code_cancel_secondfirst) = 2 * ge_signed_half_cancel_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_secondfirstreal) = S ge_signed_half_cancel_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_second) + ge_balance_negative_cancel_secondfirstreal = (ge_first_rn_cancel_second) + ge_balance_positive_cancel_secondfirstreal))) /\ (exists ge_balance_positive_cancel_secondfirstimaginary ge_balance_negative_cancel_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_secondfirst) = 2 * (ge_balance_positive_cancel_secondfirstimaginary) /\ (ge_balance_negative_cancel_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_secondfirst) = 2 * ge_signed_half_cancel_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_secondfirstimaginary) = S ge_signed_half_cancel_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_second) + ge_balance_negative_cancel_secondfirstimaginary = (ge_first_in_cancel_second) + ge_balance_positive_cancel_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_secondsecond ge_representation_imaginary_code_cancel_secondsecond. (((c) = ((ge_representation_real_code_cancel_secondsecond) + (ge_representation_imaginary_code_cancel_secondsecond)) * S ((ge_representation_real_code_cancel_secondsecond) + (ge_representation_imaginary_code_cancel_secondsecond)) + ((ge_representation_imaginary_code_cancel_secondsecond) + (ge_representation_imaginary_code_cancel_secondsecond))) /\ ((exists ge_balance_positive_cancel_secondsecondreal ge_balance_negative_cancel_secondsecondreal. (((((ge_representation_real_code_cancel_secondsecond) = 2 * (ge_balance_positive_cancel_secondsecondreal) /\ (ge_balance_negative_cancel_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_secondsecondrealdecode. (((ge_representation_real_code_cancel_secondsecond) = 2 * ge_signed_half_cancel_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_secondsecondreal) = S ge_signed_half_cancel_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_second) + ge_balance_negative_cancel_secondsecondreal = (ge_second_rn_cancel_second) + ge_balance_positive_cancel_secondsecondreal))) /\ (exists ge_balance_positive_cancel_secondsecondimaginary ge_balance_negative_cancel_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_secondsecond) = 2 * (ge_balance_positive_cancel_secondsecondimaginary) /\ (ge_balance_negative_cancel_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_secondsecond) = 2 * ge_signed_half_cancel_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_secondsecondimaginary) = S ge_signed_half_cancel_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_second) + ge_balance_negative_cancel_secondsecondimaginary = (ge_second_in_cancel_second) + ge_balance_positive_cancel_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_secondoutput ge_representation_imaginary_code_cancel_secondoutput. (((t) = ((ge_representation_real_code_cancel_secondoutput) + (ge_representation_imaginary_code_cancel_secondoutput)) * S ((ge_representation_real_code_cancel_secondoutput) + (ge_representation_imaginary_code_cancel_secondoutput)) + ((ge_representation_imaginary_code_cancel_secondoutput) + (ge_representation_imaginary_code_cancel_secondoutput))) /\ ((exists ge_balance_positive_cancel_secondoutputreal ge_balance_negative_cancel_secondoutputreal. (((((ge_representation_real_code_cancel_secondoutput) = 2 * (ge_balance_positive_cancel_secondoutputreal) /\ (ge_balance_negative_cancel_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_secondoutputrealdecode. (((ge_representation_real_code_cancel_secondoutput) = 2 * ge_signed_half_cancel_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_secondoutputreal) = S ge_signed_half_cancel_secondoutputrealdecode))) /\ ((((ge_first_rp_cancel_second) + (ge_second_rp_cancel_second))) + ge_balance_negative_cancel_secondoutputreal = (((ge_first_rn_cancel_second) + (ge_second_rn_cancel_second))) + ge_balance_positive_cancel_secondoutputreal))) /\ (exists ge_balance_positive_cancel_secondoutputimaginary ge_balance_negative_cancel_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_secondoutput) = 2 * (ge_balance_positive_cancel_secondoutputimaginary) /\ (ge_balance_negative_cancel_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_secondoutput) = 2 * ge_signed_half_cancel_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_secondoutputimaginary) = S ge_signed_half_cancel_secondoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_second) + (ge_second_ip_cancel_second))) + ge_balance_negative_cancel_secondoutputimaginary = (((ge_first_in_cancel_second) + (ge_second_in_cancel_second))) + ge_balance_positive_cancel_secondoutputimaginary))))))))) -> b=c

Complete tactic proof in conservative notation

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

112 script commands · 15 reading checkpoints · 5 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 (5)
gaussian valid has representationgaussian add input left validgaussian add input right validgaussian codes equal of representationsgaussian ring raw add cancel left
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro hAB
  6. L6
    intro hAC
02Establish hAL7–14

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

  1. L7
    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. L8
    specialize gaussian_valid_has_representation (a)
  3. L9
    apply gaussian_valid_has_representation
  4. L10
    specialize gaussian_add_input_left_valid (a)
  5. L11
    specialize gaussian_add_input_left_valid (b)
  6. L12
    specialize gaussian_add_input_left_valid (t)
  7. L13
    apply gaussian_add_input_left_valid
  8. L14
    exact hAB
03Separate the logical casesL15–18

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

  1. L15
    cases hA
  2. L16
    cases hA_witness
  3. L17
    cases hA_witness_witness
  4. L18
    cases hA_witness_witness_witness
04Establish hBL19–26

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

  1. L19
    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. L20
    specialize gaussian_valid_has_representation (b)
  3. L21
    apply gaussian_valid_has_representation
  4. L22
    specialize gaussian_add_input_right_valid (a)
  5. L23
    specialize gaussian_add_input_right_valid (b)
  6. L24
    specialize gaussian_add_input_right_valid (t)
  7. L25
    apply gaussian_add_input_right_valid
  8. L26
    exact hAB
05Separate the logical casesL27–30

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

  1. L27
    cases hB
  2. L28
    cases hB_witness
  3. L29
    cases hB_witness_witness
  4. L30
    cases hB_witness_witness_witness
06Establish hCL31–38

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

  1. L31
    have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)Definitions: ZPairRep(c,rp,rn,ip,inn)Original native command in the exact edition
  2. L32
    specialize gaussian_valid_has_representation (c)
  3. L33
    apply gaussian_valid_has_representation
  4. L34
    specialize gaussian_add_input_right_valid (a)
  5. L35
    specialize gaussian_add_input_right_valid (c)
  6. L36
    specialize gaussian_add_input_right_valid (t)
  7. L37
    apply gaussian_add_input_right_valid
  8. L38
    exact hAC
07Separate the logical casesL39–42

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

  1. L39
    cases hC
  2. L40
    cases hC_witness
  3. L41
    cases hC_witness_witness
  4. L42
    cases hC_witness_witness_witness
08Establish hleftL43–52

Establish this local claim before using it. It is not an additional assumption.

  1. L43
    have hleft : ZPairRep(t,x + x4,x1 + x5,x2 + x6,x3 + x7)Definitions: ZPairRep(t,x + x4,x1 + x5,x2 + x6,x3 + x7)Original native command in the exact edition
  2. L44
    specialize gaussian_add_for_representations (a)
  3. L45
    specialize gaussian_add_for_representations (b)
  4. L46
    specialize gaussian_add_for_representations (t)
  5. L47
    specialize gaussian_add_for_representations (x)
  6. L48
    specialize gaussian_add_for_representations (x1)
  7. L49
    specialize gaussian_add_for_representations (x2)
  8. L50
    specialize gaussian_add_for_representations (x3)
  9. L51
    specialize gaussian_add_for_representations (x4)
  10. L52
    specialize gaussian_add_for_representations (x5)
09Use earlier factsL53–58

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

  1. L53
    specialize gaussian_add_for_representations (x6)
  2. L54
    specialize gaussian_add_for_representations (x7)
  3. L55
    apply gaussian_add_for_representations
  4. L56
    exact hA_witness_witness_witness_witness
  5. L57
    exact hB_witness_witness_witness_witness
  6. L58
    exact hAB
10Establish hrightL59–68

Establish this local claim before using it. It is not an additional assumption.

  1. L59
    have hright : ZPairRep(t,x + x8,x1 + x9,x2 + x10,x3 + x11)Definitions: ZPairRep(t,x + x8,x1 + x9,x2 + x10,x3 + x11)Original native command in the exact edition
  2. L60
    specialize gaussian_add_for_representations (a)
  3. L61
    specialize gaussian_add_for_representations (c)
  4. L62
    specialize gaussian_add_for_representations (t)
  5. L63
    specialize gaussian_add_for_representations (x)
  6. L64
    specialize gaussian_add_for_representations (x1)
  7. L65
    specialize gaussian_add_for_representations (x2)
  8. L66
    specialize gaussian_add_for_representations (x3)
  9. L67
    specialize gaussian_add_for_representations (x8)
  10. L68
    specialize gaussian_add_for_representations (x9)
11Use earlier factsL69–78

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

  1. L69
    specialize gaussian_add_for_representations (x10)
  2. L70
    specialize gaussian_add_for_representations (x11)
  3. L71
    apply gaussian_add_for_representations
  4. L72
    exact hA_witness_witness_witness_witness
  5. L73
    exact hC_witness_witness_witness_witness
  6. L74
    exact hAC
  7. L75
    specialize gaussian_codes_equal_of_representations (b)
  8. L76
    specialize gaussian_codes_equal_of_representations (c)
  9. L77
    specialize gaussian_codes_equal_of_representations (x4)
  10. L78
    specialize gaussian_codes_equal_of_representations (x5)
12Use earlier factsL79–88

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

  1. L79
    specialize gaussian_codes_equal_of_representations (x6)
  2. L80
    specialize gaussian_codes_equal_of_representations (x7)
  3. L81
    specialize gaussian_codes_equal_of_representations (x8)
  4. L82
    specialize gaussian_codes_equal_of_representations (x9)
  5. L83
    specialize gaussian_codes_equal_of_representations (x10)
  6. L84
    specialize gaussian_codes_equal_of_representations (x11)
  7. L85
    apply gaussian_codes_equal_of_representations
  8. L86
    exact hB_witness_witness_witness_witness
  9. L87
    exact hC_witness_witness_witness_witness
  10. L88
    specialize gaussian_ring_raw_add_cancel_left (x)
13Use earlier factsL89–98

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

  1. L89
    specialize gaussian_ring_raw_add_cancel_left (x1)
  2. L90
    specialize gaussian_ring_raw_add_cancel_left (x2)
  3. L91
    specialize gaussian_ring_raw_add_cancel_left (x3)
  4. L92
    specialize gaussian_ring_raw_add_cancel_left (x4)
  5. L93
    specialize gaussian_ring_raw_add_cancel_left (x5)
  6. L94
    specialize gaussian_ring_raw_add_cancel_left (x6)
  7. L95
    specialize gaussian_ring_raw_add_cancel_left (x7)
  8. L96
    specialize gaussian_ring_raw_add_cancel_left (x8)
  9. L97
    specialize gaussian_ring_raw_add_cancel_left (x9)
  10. L98
    specialize gaussian_ring_raw_add_cancel_left (x10)
14Use earlier factsL99–108

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

  1. L99
    specialize gaussian_ring_raw_add_cancel_left (x11)
  2. L100
    apply gaussian_ring_raw_add_cancel_left
  3. L101
    specialize gaussian_representation_equal (t)
  4. L102
    specialize gaussian_representation_equal (((x) + (x4)))
  5. L103
    specialize gaussian_representation_equal (((x1) + (x5)))
  6. L104
    specialize gaussian_representation_equal (((x2) + (x6)))
  7. L105
    specialize gaussian_representation_equal (((x3) + (x7)))
  8. L106
    specialize gaussian_representation_equal (((x) + (x8)))
  9. L107
    specialize gaussian_representation_equal (((x1) + (x9)))
  10. L108
    specialize gaussian_representation_equal (((x2) + (x10)))
15Use earlier factsL109–112

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

  1. L109
    specialize gaussian_representation_equal (((x3) + (x11)))
  2. L110
    apply gaussian_representation_equal
  3. L111
    exact hleft
  4. L112
    exact hright

Library-wide reading audit

Original defined command ledger · 112 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro hAB
  6. 0006intro hAC
  7. 0007have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  8. 0008specialize gaussian_valid_has_representation (a)
  9. 0009apply gaussian_valid_has_representation
  10. 0010specialize gaussian_add_input_left_valid (a)
  11. 0011specialize gaussian_add_input_left_valid (b)
  12. 0012specialize gaussian_add_input_left_valid (t)
  13. 0013apply gaussian_add_input_left_valid
  14. 0014exact hAB
  15. 0015cases hA
  16. 0016cases hA_witness
  17. 0017cases hA_witness_witness
  18. 0018cases hA_witness_witness_witness
  19. 0019have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)
  20. 0020specialize gaussian_valid_has_representation (b)
  21. 0021apply gaussian_valid_has_representation
  22. 0022specialize gaussian_add_input_right_valid (a)
  23. 0023specialize gaussian_add_input_right_valid (b)
  24. 0024specialize gaussian_add_input_right_valid (t)
  25. 0025apply gaussian_add_input_right_valid
  26. 0026exact hAB
  27. 0027cases hB
  28. 0028cases hB_witness
  29. 0029cases hB_witness_witness
  30. 0030cases hB_witness_witness_witness
  31. 0031have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)
  32. 0032specialize gaussian_valid_has_representation (c)
  33. 0033apply gaussian_valid_has_representation
  34. 0034specialize gaussian_add_input_right_valid (a)
  35. 0035specialize gaussian_add_input_right_valid (c)
  36. 0036specialize gaussian_add_input_right_valid (t)
  37. 0037apply gaussian_add_input_right_valid
  38. 0038exact hAC
  39. 0039cases hC
  40. 0040cases hC_witness
  41. 0041cases hC_witness_witness
  42. 0042cases hC_witness_witness_witness
  43. 0043have hleft : ZPairRep(t,x + x4,x1 + x5,x2 + x6,x3 + x7)
  44. 0044specialize gaussian_add_for_representations (a)
  45. 0045specialize gaussian_add_for_representations (b)
  46. 0046specialize gaussian_add_for_representations (t)
  47. 0047specialize gaussian_add_for_representations (x)
  48. 0048specialize gaussian_add_for_representations (x1)
  49. 0049specialize gaussian_add_for_representations (x2)
  50. 0050specialize gaussian_add_for_representations (x3)
  51. 0051specialize gaussian_add_for_representations (x4)
  52. 0052specialize gaussian_add_for_representations (x5)
  53. 0053specialize gaussian_add_for_representations (x6)
  54. 0054specialize gaussian_add_for_representations (x7)
  55. 0055apply gaussian_add_for_representations
  56. 0056exact hA_witness_witness_witness_witness
  57. 0057exact hB_witness_witness_witness_witness
  58. 0058exact hAB
  59. 0059have hright : ZPairRep(t,x + x8,x1 + x9,x2 + x10,x3 + x11)
  60. 0060specialize gaussian_add_for_representations (a)
  61. 0061specialize gaussian_add_for_representations (c)
  62. 0062specialize gaussian_add_for_representations (t)
  63. 0063specialize gaussian_add_for_representations (x)
  64. 0064specialize gaussian_add_for_representations (x1)
  65. 0065specialize gaussian_add_for_representations (x2)
  66. 0066specialize gaussian_add_for_representations (x3)
  67. 0067specialize gaussian_add_for_representations (x8)
  68. 0068specialize gaussian_add_for_representations (x9)
  69. 0069specialize gaussian_add_for_representations (x10)
  70. 0070specialize gaussian_add_for_representations (x11)
  71. 0071apply gaussian_add_for_representations
  72. 0072exact hA_witness_witness_witness_witness
  73. 0073exact hC_witness_witness_witness_witness
  74. 0074exact hAC
  75. 0075specialize gaussian_codes_equal_of_representations (b)
  76. 0076specialize gaussian_codes_equal_of_representations (c)
  77. 0077specialize gaussian_codes_equal_of_representations (x4)
  78. 0078specialize gaussian_codes_equal_of_representations (x5)
  79. 0079specialize gaussian_codes_equal_of_representations (x6)
  80. 0080specialize gaussian_codes_equal_of_representations (x7)
  81. 0081specialize gaussian_codes_equal_of_representations (x8)
  82. 0082specialize gaussian_codes_equal_of_representations (x9)
  83. 0083specialize gaussian_codes_equal_of_representations (x10)
  84. 0084specialize gaussian_codes_equal_of_representations (x11)
  85. 0085apply gaussian_codes_equal_of_representations
  86. 0086exact hB_witness_witness_witness_witness
  87. 0087exact hC_witness_witness_witness_witness
  88. 0088specialize gaussian_ring_raw_add_cancel_left (x)
  89. 0089specialize gaussian_ring_raw_add_cancel_left (x1)
  90. 0090specialize gaussian_ring_raw_add_cancel_left (x2)
  91. 0091specialize gaussian_ring_raw_add_cancel_left (x3)
  92. 0092specialize gaussian_ring_raw_add_cancel_left (x4)
  93. 0093specialize gaussian_ring_raw_add_cancel_left (x5)
  94. 0094specialize gaussian_ring_raw_add_cancel_left (x6)
  95. 0095specialize gaussian_ring_raw_add_cancel_left (x7)
  96. 0096specialize gaussian_ring_raw_add_cancel_left (x8)
  97. 0097specialize gaussian_ring_raw_add_cancel_left (x9)
  98. 0098specialize gaussian_ring_raw_add_cancel_left (x10)
  99. 0099specialize gaussian_ring_raw_add_cancel_left (x11)
  100. 0100apply gaussian_ring_raw_add_cancel_left
  101. 0101specialize gaussian_representation_equal (t)
  102. 0102specialize gaussian_representation_equal (((x) + (x4)))
  103. 0103specialize gaussian_representation_equal (((x1) + (x5)))
  104. 0104specialize gaussian_representation_equal (((x2) + (x6)))
  105. 0105specialize gaussian_representation_equal (((x3) + (x7)))
  106. 0106specialize gaussian_representation_equal (((x) + (x8)))
  107. 0107specialize gaussian_representation_equal (((x1) + (x9)))
  108. 0108specialize gaussian_representation_equal (((x2) + (x10)))
  109. 0109specialize gaussian_representation_equal (((x3) + (x11)))
  110. 0110apply gaussian_representation_equal
  111. 0111exact hleft
  112. 0112exact hright