GF002A

gaussian_multiply_zero_right

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The actual canonical Gaussian multiply zero identity holds on the entire valid carrier.

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.

Exact expanded first-order arithmetic statement

forall a. (exists ge_real_positive_multiply_zero_domain ge_real_negative_multiply_zero_domain ge_imaginary_positive_multiply_zero_domain ge_imaginary_negative_multiply_zero_domain. (exists ge_real_code_multiply_zero_domaindecode ge_imaginary_code_multiply_zero_domaindecode. (((a) = ((ge_real_code_multiply_zero_domaindecode) + (ge_imaginary_code_multiply_zero_domaindecode)) * S ((ge_real_code_multiply_zero_domaindecode) + (ge_imaginary_code_multiply_zero_domaindecode)) + ((ge_imaginary_code_multiply_zero_domaindecode) + (ge_imaginary_code_multiply_zero_domaindecode))) /\ (((((ge_real_code_multiply_zero_domaindecode) = 2 * (ge_real_positive_multiply_zero_domain) /\ (ge_real_negative_multiply_zero_domain) = 0) \/ exists ge_signed_half_ge_multiply_zero_domaindecode_real. (((ge_real_code_multiply_zero_domaindecode) = 2 * ge_signed_half_ge_multiply_zero_domaindecode_real + 1 /\ (ge_real_positive_multiply_zero_domain) = 0) /\ (ge_real_negative_multiply_zero_domain) = S ge_signed_half_ge_multiply_zero_domaindecode_real))) /\ ((((ge_imaginary_code_multiply_zero_domaindecode) = 2 * (ge_imaginary_positive_multiply_zero_domain) /\ (ge_imaginary_negative_multiply_zero_domain) = 0) \/ exists ge_signed_half_ge_multiply_zero_domaindecode_imaginary. (((ge_imaginary_code_multiply_zero_domaindecode) = 2 * ge_signed_half_ge_multiply_zero_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_multiply_zero_domain) = 0) /\ (ge_imaginary_negative_multiply_zero_domain) = S ge_signed_half_ge_multiply_zero_domaindecode_imaginary))))))) -> (exists ge_first_rp_multiply_zero_right ge_first_rn_multiply_zero_right ge_first_ip_multiply_zero_right ge_first_in_multiply_zero_right ge_second_rp_multiply_zero_right ge_second_rn_multiply_zero_right ge_second_ip_multiply_zero_right ge_second_in_multiply_zero_right. ((exists ge_representation_real_code_multiply_zero_rightfirst ge_representation_imaginary_code_multiply_zero_rightfirst. (((a) = ((ge_representation_real_code_multiply_zero_rightfirst) + (ge_representation_imaginary_code_multiply_zero_rightfirst)) * S ((ge_representation_real_code_multiply_zero_rightfirst) + (ge_representation_imaginary_code_multiply_zero_rightfirst)) + ((ge_representation_imaginary_code_multiply_zero_rightfirst) + (ge_representation_imaginary_code_multiply_zero_rightfirst))) /\ ((exists ge_balance_positive_multiply_zero_rightfirstreal ge_balance_negative_multiply_zero_rightfirstreal. (((((ge_representation_real_code_multiply_zero_rightfirst) = 2 * (ge_balance_positive_multiply_zero_rightfirstreal) /\ (ge_balance_negative_multiply_zero_rightfirstreal) = 0) \/ exists ge_signed_half_multiply_zero_rightfirstrealdecode. (((ge_representation_real_code_multiply_zero_rightfirst) = 2 * ge_signed_half_multiply_zero_rightfirstrealdecode + 1 /\ (ge_balance_positive_multiply_zero_rightfirstreal) = 0) /\ (ge_balance_negative_multiply_zero_rightfirstreal) = S ge_signed_half_multiply_zero_rightfirstrealdecode))) /\ ((ge_first_rp_multiply_zero_right) + ge_balance_negative_multiply_zero_rightfirstreal = (ge_first_rn_multiply_zero_right) + ge_balance_positive_multiply_zero_rightfirstreal))) /\ (exists ge_balance_positive_multiply_zero_rightfirstimaginary ge_balance_negative_multiply_zero_rightfirstimaginary. (((((ge_representation_imaginary_code_multiply_zero_rightfirst) = 2 * (ge_balance_positive_multiply_zero_rightfirstimaginary) /\ (ge_balance_negative_multiply_zero_rightfirstimaginary) = 0) \/ exists ge_signed_half_multiply_zero_rightfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_zero_rightfirst) = 2 * ge_signed_half_multiply_zero_rightfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_zero_rightfirstimaginary) = 0) /\ (ge_balance_negative_multiply_zero_rightfirstimaginary) = S ge_signed_half_multiply_zero_rightfirstimaginarydecode))) /\ ((ge_first_ip_multiply_zero_right) + ge_balance_negative_multiply_zero_rightfirstimaginary = (ge_first_in_multiply_zero_right) + ge_balance_positive_multiply_zero_rightfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_zero_rightsecond ge_representation_imaginary_code_multiply_zero_rightsecond. (((0) = ((ge_representation_real_code_multiply_zero_rightsecond) + (ge_representation_imaginary_code_multiply_zero_rightsecond)) * S ((ge_representation_real_code_multiply_zero_rightsecond) + (ge_representation_imaginary_code_multiply_zero_rightsecond)) + ((ge_representation_imaginary_code_multiply_zero_rightsecond) + (ge_representation_imaginary_code_multiply_zero_rightsecond))) /\ ((exists ge_balance_positive_multiply_zero_rightsecondreal ge_balance_negative_multiply_zero_rightsecondreal. (((((ge_representation_real_code_multiply_zero_rightsecond) = 2 * (ge_balance_positive_multiply_zero_rightsecondreal) /\ (ge_balance_negative_multiply_zero_rightsecondreal) = 0) \/ exists ge_signed_half_multiply_zero_rightsecondrealdecode. (((ge_representation_real_code_multiply_zero_rightsecond) = 2 * ge_signed_half_multiply_zero_rightsecondrealdecode + 1 /\ (ge_balance_positive_multiply_zero_rightsecondreal) = 0) /\ (ge_balance_negative_multiply_zero_rightsecondreal) = S ge_signed_half_multiply_zero_rightsecondrealdecode))) /\ ((ge_second_rp_multiply_zero_right) + ge_balance_negative_multiply_zero_rightsecondreal = (ge_second_rn_multiply_zero_right) + ge_balance_positive_multiply_zero_rightsecondreal))) /\ (exists ge_balance_positive_multiply_zero_rightsecondimaginary ge_balance_negative_multiply_zero_rightsecondimaginary. (((((ge_representation_imaginary_code_multiply_zero_rightsecond) = 2 * (ge_balance_positive_multiply_zero_rightsecondimaginary) /\ (ge_balance_negative_multiply_zero_rightsecondimaginary) = 0) \/ exists ge_signed_half_multiply_zero_rightsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_zero_rightsecond) = 2 * ge_signed_half_multiply_zero_rightsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_zero_rightsecondimaginary) = 0) /\ (ge_balance_negative_multiply_zero_rightsecondimaginary) = S ge_signed_half_multiply_zero_rightsecondimaginarydecode))) /\ ((ge_second_ip_multiply_zero_right) + ge_balance_negative_multiply_zero_rightsecondimaginary = (ge_second_in_multiply_zero_right) + ge_balance_positive_multiply_zero_rightsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_zero_rightoutput ge_representation_imaginary_code_multiply_zero_rightoutput. (((0) = ((ge_representation_real_code_multiply_zero_rightoutput) + (ge_representation_imaginary_code_multiply_zero_rightoutput)) * S ((ge_representation_real_code_multiply_zero_rightoutput) + (ge_representation_imaginary_code_multiply_zero_rightoutput)) + ((ge_representation_imaginary_code_multiply_zero_rightoutput) + (ge_representation_imaginary_code_multiply_zero_rightoutput))) /\ ((exists ge_balance_positive_multiply_zero_rightoutputreal ge_balance_negative_multiply_zero_rightoutputreal. (((((ge_representation_real_code_multiply_zero_rightoutput) = 2 * (ge_balance_positive_multiply_zero_rightoutputreal) /\ (ge_balance_negative_multiply_zero_rightoutputreal) = 0) \/ exists ge_signed_half_multiply_zero_rightoutputrealdecode. (((ge_representation_real_code_multiply_zero_rightoutput) = 2 * ge_signed_half_multiply_zero_rightoutputrealdecode + 1 /\ (ge_balance_positive_multiply_zero_rightoutputreal) = 0) /\ (ge_balance_negative_multiply_zero_rightoutputreal) = S ge_signed_half_multiply_zero_rightoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_zero_right) * (ge_second_rp_multiply_zero_right))) + (((ge_first_rn_multiply_zero_right) * (ge_second_rn_multiply_zero_right))))) + (((((ge_first_ip_multiply_zero_right) * (ge_second_in_multiply_zero_right))) + (((ge_first_in_multiply_zero_right) * (ge_second_ip_multiply_zero_right))))))) + ge_balance_negative_multiply_zero_rightoutputreal = (((((((ge_first_rp_multiply_zero_right) * (ge_second_rn_multiply_zero_right))) + (((ge_first_rn_multiply_zero_right) * (ge_second_rp_multiply_zero_right))))) + (((((ge_first_ip_multiply_zero_right) * (ge_second_ip_multiply_zero_right))) + (((ge_first_in_multiply_zero_right) * (ge_second_in_multiply_zero_right))))))) + ge_balance_positive_multiply_zero_rightoutputreal))) /\ (exists ge_balance_positive_multiply_zero_rightoutputimaginary ge_balance_negative_multiply_zero_rightoutputimaginary. (((((ge_representation_imaginary_code_multiply_zero_rightoutput) = 2 * (ge_balance_positive_multiply_zero_rightoutputimaginary) /\ (ge_balance_negative_multiply_zero_rightoutputimaginary) = 0) \/ exists ge_signed_half_multiply_zero_rightoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_zero_rightoutput) = 2 * ge_signed_half_multiply_zero_rightoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_zero_rightoutputimaginary) = 0) /\ (ge_balance_negative_multiply_zero_rightoutputimaginary) = S ge_signed_half_multiply_zero_rightoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_zero_right) * (ge_second_ip_multiply_zero_right))) + (((ge_first_rn_multiply_zero_right) * (ge_second_in_multiply_zero_right))))) + (((((ge_first_ip_multiply_zero_right) * (ge_second_rp_multiply_zero_right))) + (((ge_first_in_multiply_zero_right) * (ge_second_rn_multiply_zero_right))))))) + ge_balance_negative_multiply_zero_rightoutputimaginary = (((((((ge_first_rp_multiply_zero_right) * (ge_second_in_multiply_zero_right))) + (((ge_first_rn_multiply_zero_right) * (ge_second_ip_multiply_zero_right))))) + (((((ge_first_ip_multiply_zero_right) * (ge_second_rn_multiply_zero_right))) + (((ge_first_in_multiply_zero_right) * (ge_second_rp_multiply_zero_right))))))) + ge_balance_positive_multiply_zero_rightoutputimaginary)))))))))

Constructive proof overview

Generated structural guide

The actual canonical Gaussian multiply zero identity holds on the entire valid carrier.

The unchanged tactic script uses 4 declared prerequisites and contains 38 exact native proof lines.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

GF0001 gaussian_valid_has_representation gaussian_multiply_of_representations Alpha theorem; checked-use authorized gaussian_representation_integer_transport Alpha theorem; checked-use authorized GF000B gaussian_zero_representation

Direct dependents

GF002B gaussian_multiply_zero_left GF0045 gaussian_divides_zero GF0053 gaussian_divides_decidable GF005F gaussian_gcd_bezout_zero_right GF0060 gaussian_gcd_bezout_zero_case

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

38 script commands · 9 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
gaussian valid has representationgaussian zero representation

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro hv
02Establish hAL3–6

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

  1. L3
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep
  2. L4
    specialize gaussian_valid_has_representation (a)
  3. L5
    apply gaussian_valid_has_representation
  4. L6
    exact hv
03Separate the logical casesL7–10

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

  1. L7
    cases hA
  2. L8
    cases hA_witness
  3. L9
    cases hA_witness_witness
  4. L10
    cases hA_witness_witness_witness
04Use earlier factsL11–20

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

  1. L11
    specialize gaussian_multiply_of_representations (a)
  2. L12
    specialize gaussian_multiply_of_representations (0)
  3. L13
    specialize gaussian_multiply_of_representations (0)
  4. L14
    specialize gaussian_multiply_of_representations (x)
  5. L15
    specialize gaussian_multiply_of_representations (x1)
  6. L16
    specialize gaussian_multiply_of_representations (x2)
  7. L17
    specialize gaussian_multiply_of_representations (x3)
  8. L18
    specialize gaussian_multiply_of_representations (0)
  9. L19
    specialize gaussian_multiply_of_representations (0)
  10. L20
    specialize gaussian_multiply_of_representations (0)
05Use earlier factsL21–30

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

  1. L21
    specialize gaussian_multiply_of_representations (0)
  2. L22
    apply gaussian_multiply_of_representations
  3. L23
    exact hA_witness_witness_witness_witness
  4. L24
    exact gaussian_zero_representation
  5. L25
    specialize gaussian_representation_integer_transport (0)
  6. L26
    specialize gaussian_representation_integer_transport (0)
  7. L27
    specialize gaussian_representation_integer_transport (0)
  8. L28
    specialize gaussian_representation_integer_transport (0)
  9. L29
    specialize gaussian_representation_integer_transport (0)
  10. L30
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
06Use earlier factsL31–34

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

  1. L31
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  2. L32
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  3. L33
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  4. L34
    apply gaussian_representation_integer_transport
07Separate the logical casesL35–35

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

  1. L35
    split
08Calculate and transport equalitiesL36–37

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

  1. L36
    simp
  2. L37
    simp
09Use earlier factsL38–38

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

  1. L38
    exact gaussian_zero_representation

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro a
  2. 0002intro hv
  3. 0003have hA : exists rp rn ip inn. (exists ge_representation_real_code_chosen_hA ge_representation_imaginary_code_chosen_hA. (((a) = ((ge_representation_real_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA)) * S ((ge_representation_real_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA)) + ((ge_representation_imaginary_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA))) /\ ((exists ge_balance_positive_chosen_hAreal ge_balance_negative_chosen_hAreal. (((((ge_representation_real_code_chosen_hA) = 2 * (ge_balance_positive_chosen_hAreal) /\ (ge_balance_negative_chosen_hAreal) = 0) \/ exists ge_signed_half_chosen_hArealdecode. (((ge_representation_real_code_chosen_hA) = 2 * ge_signed_half_chosen_hArealdecode + 1 /\ (ge_balance_positive_chosen_hAreal) = 0) /\ (ge_balance_negative_chosen_hAreal) = S ge_signed_half_chosen_hArealdecode))) /\ ((rp) + ge_balance_negative_chosen_hAreal = (rn) + ge_balance_positive_chosen_hAreal))) /\ (exists ge_balance_positive_chosen_hAimaginary ge_balance_negative_chosen_hAimaginary. (((((ge_representation_imaginary_code_chosen_hA) = 2 * (ge_balance_positive_chosen_hAimaginary) /\ (ge_balance_negative_chosen_hAimaginary) = 0) \/ exists ge_signed_half_chosen_hAimaginarydecode. (((ge_representation_imaginary_code_chosen_hA) = 2 * ge_signed_half_chosen_hAimaginarydecode + 1 /\ (ge_balance_positive_chosen_hAimaginary) = 0) /\ (ge_balance_negative_chosen_hAimaginary) = S ge_signed_half_chosen_hAimaginarydecode))) /\ ((ip) + ge_balance_negative_chosen_hAimaginary = (inn) + ge_balance_positive_chosen_hAimaginary))))))
  4. 0004specialize gaussian_valid_has_representation (a)
  5. 0005apply gaussian_valid_has_representation
  6. 0006exact hv
  7. 0007cases hA
  8. 0008cases hA_witness
  9. 0009cases hA_witness_witness
  10. 0010cases hA_witness_witness_witness
  11. 0011specialize gaussian_multiply_of_representations (a)
  12. 0012specialize gaussian_multiply_of_representations (0)
  13. 0013specialize gaussian_multiply_of_representations (0)
  14. 0014specialize gaussian_multiply_of_representations (x)
  15. 0015specialize gaussian_multiply_of_representations (x1)
  16. 0016specialize gaussian_multiply_of_representations (x2)
  17. 0017specialize gaussian_multiply_of_representations (x3)
  18. 0018specialize gaussian_multiply_of_representations (0)
  19. 0019specialize gaussian_multiply_of_representations (0)
  20. 0020specialize gaussian_multiply_of_representations (0)
  21. 0021specialize gaussian_multiply_of_representations (0)
  22. 0022apply gaussian_multiply_of_representations
  23. 0023exact hA_witness_witness_witness_witness
  24. 0024exact gaussian_zero_representation
  25. 0025specialize gaussian_representation_integer_transport (0)
  26. 0026specialize gaussian_representation_integer_transport (0)
  27. 0027specialize gaussian_representation_integer_transport (0)
  28. 0028specialize gaussian_representation_integer_transport (0)
  29. 0029specialize gaussian_representation_integer_transport (0)
  30. 0030specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  31. 0031specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  32. 0032specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  33. 0033specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035split
  36. 0036simp
  37. 0037simp
  38. 0038exact gaussian_zero_representation