GF003B

gaussian_multiply_cancel_left

A nonzero Gaussian factor cancels, using an actually constructed difference, distributivity and the proved absence of zero divisors.

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. ¬a = 0 → GMul(a,b,t) → GMul(a,c,t) → b = c

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

Definition DAG

ZPairAdd(a,b,c) · 2GMul(a,b,c) · 3

Actual proof prerequisites

gaussian_subtract_existsgaussian_multiply_input_left_validgaussian_multiply_input_right_validgaussian_multiply_output_validgaussian_add_input_left_validgaussian_multiply_exists · checked external prerequisitegaussian_multiply_add_distributegaussian_add_zero_leftgaussian_add_cancel_rightgaussian_multiply_output_transportgaussian_multiply_zero_implies_zero_factorgaussian_add_functional · checked external prerequisite
Original expanded first-order statement 
forall a b c t. ~(a=0) -> (exists ge_first_rp_cancel_product_first ge_first_rn_cancel_product_first ge_first_ip_cancel_product_first ge_first_in_cancel_product_first ge_second_rp_cancel_product_first ge_second_rn_cancel_product_first ge_second_ip_cancel_product_first ge_second_in_cancel_product_first. ((exists ge_representation_real_code_cancel_product_firstfirst ge_representation_imaginary_code_cancel_product_firstfirst. (((a) = ((ge_representation_real_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst)) * S ((ge_representation_real_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst)) + ((ge_representation_imaginary_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst))) /\ ((exists ge_balance_positive_cancel_product_firstfirstreal ge_balance_negative_cancel_product_firstfirstreal. (((((ge_representation_real_code_cancel_product_firstfirst) = 2 * (ge_balance_positive_cancel_product_firstfirstreal) /\ (ge_balance_negative_cancel_product_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_product_firstfirstrealdecode. (((ge_representation_real_code_cancel_product_firstfirst) = 2 * ge_signed_half_cancel_product_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_product_firstfirstreal) = S ge_signed_half_cancel_product_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_product_first) + ge_balance_negative_cancel_product_firstfirstreal = (ge_first_rn_cancel_product_first) + ge_balance_positive_cancel_product_firstfirstreal))) /\ (exists ge_balance_positive_cancel_product_firstfirstimaginary ge_balance_negative_cancel_product_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_firstfirst) = 2 * (ge_balance_positive_cancel_product_firstfirstimaginary) /\ (ge_balance_negative_cancel_product_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstfirst) = 2 * ge_signed_half_cancel_product_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstfirstimaginary) = S ge_signed_half_cancel_product_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_first) + ge_balance_negative_cancel_product_firstfirstimaginary = (ge_first_in_cancel_product_first) + ge_balance_positive_cancel_product_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_firstsecond ge_representation_imaginary_code_cancel_product_firstsecond. (((b) = ((ge_representation_real_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond)) * S ((ge_representation_real_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond)) + ((ge_representation_imaginary_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond))) /\ ((exists ge_balance_positive_cancel_product_firstsecondreal ge_balance_negative_cancel_product_firstsecondreal. (((((ge_representation_real_code_cancel_product_firstsecond) = 2 * (ge_balance_positive_cancel_product_firstsecondreal) /\ (ge_balance_negative_cancel_product_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_product_firstsecondrealdecode. (((ge_representation_real_code_cancel_product_firstsecond) = 2 * ge_signed_half_cancel_product_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_product_firstsecondreal) = S ge_signed_half_cancel_product_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_product_first) + ge_balance_negative_cancel_product_firstsecondreal = (ge_second_rn_cancel_product_first) + ge_balance_positive_cancel_product_firstsecondreal))) /\ (exists ge_balance_positive_cancel_product_firstsecondimaginary ge_balance_negative_cancel_product_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_firstsecond) = 2 * (ge_balance_positive_cancel_product_firstsecondimaginary) /\ (ge_balance_negative_cancel_product_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstsecond) = 2 * ge_signed_half_cancel_product_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstsecondimaginary) = S ge_signed_half_cancel_product_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_first) + ge_balance_negative_cancel_product_firstsecondimaginary = (ge_second_in_cancel_product_first) + ge_balance_positive_cancel_product_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_firstoutput ge_representation_imaginary_code_cancel_product_firstoutput. (((t) = ((ge_representation_real_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput)) * S ((ge_representation_real_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput)) + ((ge_representation_imaginary_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput))) /\ ((exists ge_balance_positive_cancel_product_firstoutputreal ge_balance_negative_cancel_product_firstoutputreal. (((((ge_representation_real_code_cancel_product_firstoutput) = 2 * (ge_balance_positive_cancel_product_firstoutputreal) /\ (ge_balance_negative_cancel_product_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_product_firstoutputrealdecode. (((ge_representation_real_code_cancel_product_firstoutput) = 2 * ge_signed_half_cancel_product_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_product_firstoutputreal) = S ge_signed_half_cancel_product_firstoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_product_first) * (ge_second_rp_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_rn_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_in_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_ip_cancel_product_first))))))) + ge_balance_negative_cancel_product_firstoutputreal = (((((((ge_first_rp_cancel_product_first) * (ge_second_rn_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_rp_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_ip_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_in_cancel_product_first))))))) + ge_balance_positive_cancel_product_firstoutputreal))) /\ (exists ge_balance_positive_cancel_product_firstoutputimaginary ge_balance_negative_cancel_product_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_firstoutput) = 2 * (ge_balance_positive_cancel_product_firstoutputimaginary) /\ (ge_balance_negative_cancel_product_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstoutput) = 2 * ge_signed_half_cancel_product_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstoutputimaginary) = S ge_signed_half_cancel_product_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_product_first) * (ge_second_ip_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_in_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_rp_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_rn_cancel_product_first))))))) + ge_balance_negative_cancel_product_firstoutputimaginary = (((((((ge_first_rp_cancel_product_first) * (ge_second_in_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_ip_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_rn_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_rp_cancel_product_first))))))) + ge_balance_positive_cancel_product_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_product_second ge_first_rn_cancel_product_second ge_first_ip_cancel_product_second ge_first_in_cancel_product_second ge_second_rp_cancel_product_second ge_second_rn_cancel_product_second ge_second_ip_cancel_product_second ge_second_in_cancel_product_second. ((exists ge_representation_real_code_cancel_product_secondfirst ge_representation_imaginary_code_cancel_product_secondfirst. (((a) = ((ge_representation_real_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst)) * S ((ge_representation_real_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst)) + ((ge_representation_imaginary_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst))) /\ ((exists ge_balance_positive_cancel_product_secondfirstreal ge_balance_negative_cancel_product_secondfirstreal. (((((ge_representation_real_code_cancel_product_secondfirst) = 2 * (ge_balance_positive_cancel_product_secondfirstreal) /\ (ge_balance_negative_cancel_product_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_product_secondfirstrealdecode. (((ge_representation_real_code_cancel_product_secondfirst) = 2 * ge_signed_half_cancel_product_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_product_secondfirstreal) = S ge_signed_half_cancel_product_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_product_second) + ge_balance_negative_cancel_product_secondfirstreal = (ge_first_rn_cancel_product_second) + ge_balance_positive_cancel_product_secondfirstreal))) /\ (exists ge_balance_positive_cancel_product_secondfirstimaginary ge_balance_negative_cancel_product_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_secondfirst) = 2 * (ge_balance_positive_cancel_product_secondfirstimaginary) /\ (ge_balance_negative_cancel_product_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondfirst) = 2 * ge_signed_half_cancel_product_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondfirstimaginary) = S ge_signed_half_cancel_product_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_second) + ge_balance_negative_cancel_product_secondfirstimaginary = (ge_first_in_cancel_product_second) + ge_balance_positive_cancel_product_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_secondsecond ge_representation_imaginary_code_cancel_product_secondsecond. (((c) = ((ge_representation_real_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond)) * S ((ge_representation_real_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond)) + ((ge_representation_imaginary_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond))) /\ ((exists ge_balance_positive_cancel_product_secondsecondreal ge_balance_negative_cancel_product_secondsecondreal. (((((ge_representation_real_code_cancel_product_secondsecond) = 2 * (ge_balance_positive_cancel_product_secondsecondreal) /\ (ge_balance_negative_cancel_product_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_product_secondsecondrealdecode. (((ge_representation_real_code_cancel_product_secondsecond) = 2 * ge_signed_half_cancel_product_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_product_secondsecondreal) = S ge_signed_half_cancel_product_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_product_second) + ge_balance_negative_cancel_product_secondsecondreal = (ge_second_rn_cancel_product_second) + ge_balance_positive_cancel_product_secondsecondreal))) /\ (exists ge_balance_positive_cancel_product_secondsecondimaginary ge_balance_negative_cancel_product_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_secondsecond) = 2 * (ge_balance_positive_cancel_product_secondsecondimaginary) /\ (ge_balance_negative_cancel_product_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondsecond) = 2 * ge_signed_half_cancel_product_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondsecondimaginary) = S ge_signed_half_cancel_product_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_second) + ge_balance_negative_cancel_product_secondsecondimaginary = (ge_second_in_cancel_product_second) + ge_balance_positive_cancel_product_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_secondoutput ge_representation_imaginary_code_cancel_product_secondoutput. (((t) = ((ge_representation_real_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput)) * S ((ge_representation_real_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput)) + ((ge_representation_imaginary_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput))) /\ ((exists ge_balance_positive_cancel_product_secondoutputreal ge_balance_negative_cancel_product_secondoutputreal. (((((ge_representation_real_code_cancel_product_secondoutput) = 2 * (ge_balance_positive_cancel_product_secondoutputreal) /\ (ge_balance_negative_cancel_product_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_product_secondoutputrealdecode. (((ge_representation_real_code_cancel_product_secondoutput) = 2 * ge_signed_half_cancel_product_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_product_secondoutputreal) = S ge_signed_half_cancel_product_secondoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_product_second) * (ge_second_rp_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_rn_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_in_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_ip_cancel_product_second))))))) + ge_balance_negative_cancel_product_secondoutputreal = (((((((ge_first_rp_cancel_product_second) * (ge_second_rn_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_rp_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_ip_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_in_cancel_product_second))))))) + ge_balance_positive_cancel_product_secondoutputreal))) /\ (exists ge_balance_positive_cancel_product_secondoutputimaginary ge_balance_negative_cancel_product_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_secondoutput) = 2 * (ge_balance_positive_cancel_product_secondoutputimaginary) /\ (ge_balance_negative_cancel_product_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondoutput) = 2 * ge_signed_half_cancel_product_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondoutputimaginary) = S ge_signed_half_cancel_product_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_product_second) * (ge_second_ip_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_in_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_rp_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_rn_cancel_product_second))))))) + ge_balance_negative_cancel_product_secondoutputimaginary = (((((((ge_first_rp_cancel_product_second) * (ge_second_in_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_ip_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_rn_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_rp_cancel_product_second))))))) + ge_balance_positive_cancel_product_secondoutputimaginary))))))))) -> b=c

Complete tactic proof in conservative notation

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

93 script commands · 18 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 (10)
gaussian subtract existsgaussian multiply input right validgaussian multiply input left validgaussian add input left validgaussian multiply add distributegaussian add cancel rightgaussian add zero leftgaussian multiply output validgaussian multiply zero implies zero factorgaussian multiply output transport
01Fix variables and assumptionsL1–7

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 hn
  6. L6
    intro hB
  7. L7
    intro hC
02Establish hdL8–17

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

  1. L8
    have hd : ∃ d. ZPairAdd(d,c,b)Definitions: ZPairAdd(d,c,b)Original native command in the exact edition
  2. L9
    specialize gaussian_subtract_exists (b)
  3. L10
    specialize gaussian_subtract_exists (c)
  4. L11
    apply gaussian_subtract_exists
  5. L12
    specialize gaussian_multiply_input_right_valid (a)
  6. L13
    specialize gaussian_multiply_input_right_valid (b)
  7. L14
    specialize gaussian_multiply_input_right_valid (t)
  8. L15
    apply gaussian_multiply_input_right_valid
  9. L16
    exact hB
  10. L17
    specialize gaussian_multiply_input_right_valid (a)
03Use earlier factsL18–21

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

  1. L18
    specialize gaussian_multiply_input_right_valid (c)
  2. L19
    specialize gaussian_multiply_input_right_valid (t)
  3. L20
    apply gaussian_multiply_input_right_valid
  4. L21
    exact hC
04Separate the logical casesL22–22

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

  1. L22
    cases hd
05Establish hproductL23–32

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

  1. L23
    have hproduct : ∃ u. GMul(a,x,u)Definitions: GMul(a,x,u)Original native command in the exact edition
  2. L24
    specialize gaussian_multiply_exists (a)
  3. L25
    specialize gaussian_multiply_exists (x)
  4. L26
    apply gaussian_multiply_exists
  5. L27
    specialize gaussian_multiply_input_left_valid (a)
  6. L28
    specialize gaussian_multiply_input_left_valid (b)
  7. L29
    specialize gaussian_multiply_input_left_valid (t)
  8. L30
    apply gaussian_multiply_input_left_valid
  9. L31
    exact hB
  10. L32
    specialize gaussian_add_input_left_valid (x)
06Use earlier factsL33–36

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

  1. L33
    specialize gaussian_add_input_left_valid (c)
  2. L34
    specialize gaussian_add_input_left_valid (b)
  3. L35
    apply gaussian_add_input_left_valid
  4. L36
    exact hd_witness
07Separate the logical casesL37–37

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

  1. L37
    cases hproduct
08Establish hsumL38–47

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

  1. L38
    have hsum : ZPairAdd(x1,t,t)Definitions: ZPairAdd(x1,t,t)Original native command in the exact edition
  2. L39
    specialize gaussian_multiply_add_distribute (a)
  3. L40
    specialize gaussian_multiply_add_distribute (x)
  4. L41
    specialize gaussian_multiply_add_distribute (c)
  5. L42
    specialize gaussian_multiply_add_distribute (b)
  6. L43
    specialize gaussian_multiply_add_distribute (x1)
  7. L44
    specialize gaussian_multiply_add_distribute (t)
  8. L45
    specialize gaussian_multiply_add_distribute (t)
  9. L46
    apply gaussian_multiply_add_distribute
  10. L47
    exact hd_witness
09Use earlier factsL48–50

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

  1. L48
    exact hproduct_witness
  2. L49
    exact hC
  3. L50
    exact hB
10Establish hzeroL51–60

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

  1. L51
    have hzero : x1=0
  2. L52
    specialize gaussian_add_cancel_right (x1)
  3. L53
    specialize gaussian_add_cancel_right (0)
  4. L54
    specialize gaussian_add_cancel_right (t)
  5. L55
    specialize gaussian_add_cancel_right (t)
  6. L56
    apply gaussian_add_cancel_right
  7. L57
    exact hsum
  8. L58
    specialize gaussian_add_zero_left (t)
  9. L59
    apply gaussian_add_zero_left
  10. L60
    specialize gaussian_multiply_output_valid (a)
11Use earlier factsL61–64

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

  1. L61
    specialize gaussian_multiply_output_valid (b)
  2. L62
    specialize gaussian_multiply_output_valid (t)
  3. L63
    apply gaussian_multiply_output_valid
  4. L64
    exact hB
12Establish hcasesL65–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply zero implies zero factor.

  1. L65
    have hcases : a=0 \/ x=0
  2. L66
    specialize gaussian_multiply_zero_implies_zero_factor (a)
  3. L67
    specialize gaussian_multiply_zero_implies_zero_factor (x)
  4. L68
    apply gaussian_multiply_zero_implies_zero_factor
  5. L69
    specialize gaussian_multiply_output_transport (a)
  6. L70
    specialize gaussian_multiply_output_transport (x)
  7. L71
    specialize gaussian_multiply_output_transport (x1)
  8. L72
    specialize gaussian_multiply_output_transport (0)
  9. L73
    apply gaussian_multiply_output_transport
  10. L74
    exact hzero
13Use earlier factsL75–75

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

  1. L75
    exact hproduct_witness
14Separate the logical casesL76–77

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

  1. L76
    cases hcases
  2. L77
    exfalso
15Use earlier factsL78–79

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

  1. L78
    apply hn
  2. L79
    exact hcases_left
16Calculate and transport equalitiesL80–80

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

  1. L80
    rewrite hcases_right at hd_witness
17Use earlier factsL81–90

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

  1. L81
    specialize gaussian_add_functional (0)
  2. L82
    specialize gaussian_add_functional (c)
  3. L83
    specialize gaussian_add_functional (b)
  4. L84
    specialize gaussian_add_functional (c)
  5. L85
    apply gaussian_add_functional
  6. L86
    exact hd_witness
  7. L87
    specialize gaussian_add_zero_left (c)
  8. L88
    apply gaussian_add_zero_left
  9. L89
    specialize gaussian_multiply_input_right_valid (a)
  10. L90
    specialize gaussian_multiply_input_right_valid (c)
18Use earlier factsL91–93

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

  1. L91
    specialize gaussian_multiply_input_right_valid (t)
  2. L92
    apply gaussian_multiply_input_right_valid
  3. L93
    exact hC

Library-wide reading audit

Original defined command ledger · 93 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro hn
  6. 0006intro hB
  7. 0007intro hC
  8. 0008have hd : ∃ d. ZPairAdd(d,c,b)
  9. 0009specialize gaussian_subtract_exists (b)
  10. 0010specialize gaussian_subtract_exists (c)
  11. 0011apply gaussian_subtract_exists
  12. 0012specialize gaussian_multiply_input_right_valid (a)
  13. 0013specialize gaussian_multiply_input_right_valid (b)
  14. 0014specialize gaussian_multiply_input_right_valid (t)
  15. 0015apply gaussian_multiply_input_right_valid
  16. 0016exact hB
  17. 0017specialize gaussian_multiply_input_right_valid (a)
  18. 0018specialize gaussian_multiply_input_right_valid (c)
  19. 0019specialize gaussian_multiply_input_right_valid (t)
  20. 0020apply gaussian_multiply_input_right_valid
  21. 0021exact hC
  22. 0022cases hd
  23. 0023have hproduct : ∃ u. GMul(a,x,u)
  24. 0024specialize gaussian_multiply_exists (a)
  25. 0025specialize gaussian_multiply_exists (x)
  26. 0026apply gaussian_multiply_exists
  27. 0027specialize gaussian_multiply_input_left_valid (a)
  28. 0028specialize gaussian_multiply_input_left_valid (b)
  29. 0029specialize gaussian_multiply_input_left_valid (t)
  30. 0030apply gaussian_multiply_input_left_valid
  31. 0031exact hB
  32. 0032specialize gaussian_add_input_left_valid (x)
  33. 0033specialize gaussian_add_input_left_valid (c)
  34. 0034specialize gaussian_add_input_left_valid (b)
  35. 0035apply gaussian_add_input_left_valid
  36. 0036exact hd_witness
  37. 0037cases hproduct
  38. 0038have hsum : ZPairAdd(x1,t,t)
  39. 0039specialize gaussian_multiply_add_distribute (a)
  40. 0040specialize gaussian_multiply_add_distribute (x)
  41. 0041specialize gaussian_multiply_add_distribute (c)
  42. 0042specialize gaussian_multiply_add_distribute (b)
  43. 0043specialize gaussian_multiply_add_distribute (x1)
  44. 0044specialize gaussian_multiply_add_distribute (t)
  45. 0045specialize gaussian_multiply_add_distribute (t)
  46. 0046apply gaussian_multiply_add_distribute
  47. 0047exact hd_witness
  48. 0048exact hproduct_witness
  49. 0049exact hC
  50. 0050exact hB
  51. 0051have hzero : x1=0
  52. 0052specialize gaussian_add_cancel_right (x1)
  53. 0053specialize gaussian_add_cancel_right (0)
  54. 0054specialize gaussian_add_cancel_right (t)
  55. 0055specialize gaussian_add_cancel_right (t)
  56. 0056apply gaussian_add_cancel_right
  57. 0057exact hsum
  58. 0058specialize gaussian_add_zero_left (t)
  59. 0059apply gaussian_add_zero_left
  60. 0060specialize gaussian_multiply_output_valid (a)
  61. 0061specialize gaussian_multiply_output_valid (b)
  62. 0062specialize gaussian_multiply_output_valid (t)
  63. 0063apply gaussian_multiply_output_valid
  64. 0064exact hB
  65. 0065have hcases : a=0 \/ x=0
  66. 0066specialize gaussian_multiply_zero_implies_zero_factor (a)
  67. 0067specialize gaussian_multiply_zero_implies_zero_factor (x)
  68. 0068apply gaussian_multiply_zero_implies_zero_factor
  69. 0069specialize gaussian_multiply_output_transport (a)
  70. 0070specialize gaussian_multiply_output_transport (x)
  71. 0071specialize gaussian_multiply_output_transport (x1)
  72. 0072specialize gaussian_multiply_output_transport (0)
  73. 0073apply gaussian_multiply_output_transport
  74. 0074exact hzero
  75. 0075exact hproduct_witness
  76. 0076cases hcases
  77. 0077exfalso
  78. 0078apply hn
  79. 0079exact hcases_left
  80. 0080rewrite hcases_right at hd_witness
  81. 0081specialize gaussian_add_functional (0)
  82. 0082specialize gaussian_add_functional (c)
  83. 0083specialize gaussian_add_functional (b)
  84. 0084specialize gaussian_add_functional (c)
  85. 0085apply gaussian_add_functional
  86. 0086exact hd_witness
  87. 0087specialize gaussian_add_zero_left (c)
  88. 0088apply gaussian_add_zero_left
  89. 0089specialize gaussian_multiply_input_right_valid (a)
  90. 0090specialize gaussian_multiply_input_right_valid (c)
  91. 0091specialize gaussian_multiply_input_right_valid (t)
  92. 0092apply gaussian_multiply_input_right_valid
  93. 0093exact hC