GF0028

gaussian_multiply_one_right

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

The actual canonical Gaussian multiply one 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_one_domain ge_real_negative_multiply_one_domain ge_imaginary_positive_multiply_one_domain ge_imaginary_negative_multiply_one_domain. (exists ge_real_code_multiply_one_domaindecode ge_imaginary_code_multiply_one_domaindecode. (((a) = ((ge_real_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode)) * S ((ge_real_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode)) + ((ge_imaginary_code_multiply_one_domaindecode) + (ge_imaginary_code_multiply_one_domaindecode))) /\ (((((ge_real_code_multiply_one_domaindecode) = 2 * (ge_real_positive_multiply_one_domain) /\ (ge_real_negative_multiply_one_domain) = 0) \/ exists ge_signed_half_ge_multiply_one_domaindecode_real. (((ge_real_code_multiply_one_domaindecode) = 2 * ge_signed_half_ge_multiply_one_domaindecode_real + 1 /\ (ge_real_positive_multiply_one_domain) = 0) /\ (ge_real_negative_multiply_one_domain) = S ge_signed_half_ge_multiply_one_domaindecode_real))) /\ ((((ge_imaginary_code_multiply_one_domaindecode) = 2 * (ge_imaginary_positive_multiply_one_domain) /\ (ge_imaginary_negative_multiply_one_domain) = 0) \/ exists ge_signed_half_ge_multiply_one_domaindecode_imaginary. (((ge_imaginary_code_multiply_one_domaindecode) = 2 * ge_signed_half_ge_multiply_one_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_multiply_one_domain) = 0) /\ (ge_imaginary_negative_multiply_one_domain) = S ge_signed_half_ge_multiply_one_domaindecode_imaginary))))))) -> (exists ge_first_rp_multiply_one_right ge_first_rn_multiply_one_right ge_first_ip_multiply_one_right ge_first_in_multiply_one_right ge_second_rp_multiply_one_right ge_second_rn_multiply_one_right ge_second_ip_multiply_one_right ge_second_in_multiply_one_right. ((exists ge_representation_real_code_multiply_one_rightfirst ge_representation_imaginary_code_multiply_one_rightfirst. (((a) = ((ge_representation_real_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst)) * S ((ge_representation_real_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst)) + ((ge_representation_imaginary_code_multiply_one_rightfirst) + (ge_representation_imaginary_code_multiply_one_rightfirst))) /\ ((exists ge_balance_positive_multiply_one_rightfirstreal ge_balance_negative_multiply_one_rightfirstreal. (((((ge_representation_real_code_multiply_one_rightfirst) = 2 * (ge_balance_positive_multiply_one_rightfirstreal) /\ (ge_balance_negative_multiply_one_rightfirstreal) = 0) \/ exists ge_signed_half_multiply_one_rightfirstrealdecode. (((ge_representation_real_code_multiply_one_rightfirst) = 2 * ge_signed_half_multiply_one_rightfirstrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightfirstreal) = 0) /\ (ge_balance_negative_multiply_one_rightfirstreal) = S ge_signed_half_multiply_one_rightfirstrealdecode))) /\ ((ge_first_rp_multiply_one_right) + ge_balance_negative_multiply_one_rightfirstreal = (ge_first_rn_multiply_one_right) + ge_balance_positive_multiply_one_rightfirstreal))) /\ (exists ge_balance_positive_multiply_one_rightfirstimaginary ge_balance_negative_multiply_one_rightfirstimaginary. (((((ge_representation_imaginary_code_multiply_one_rightfirst) = 2 * (ge_balance_positive_multiply_one_rightfirstimaginary) /\ (ge_balance_negative_multiply_one_rightfirstimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightfirst) = 2 * ge_signed_half_multiply_one_rightfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightfirstimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightfirstimaginary) = S ge_signed_half_multiply_one_rightfirstimaginarydecode))) /\ ((ge_first_ip_multiply_one_right) + ge_balance_negative_multiply_one_rightfirstimaginary = (ge_first_in_multiply_one_right) + ge_balance_positive_multiply_one_rightfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_one_rightsecond ge_representation_imaginary_code_multiply_one_rightsecond. (((6) = ((ge_representation_real_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond)) * S ((ge_representation_real_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond)) + ((ge_representation_imaginary_code_multiply_one_rightsecond) + (ge_representation_imaginary_code_multiply_one_rightsecond))) /\ ((exists ge_balance_positive_multiply_one_rightsecondreal ge_balance_negative_multiply_one_rightsecondreal. (((((ge_representation_real_code_multiply_one_rightsecond) = 2 * (ge_balance_positive_multiply_one_rightsecondreal) /\ (ge_balance_negative_multiply_one_rightsecondreal) = 0) \/ exists ge_signed_half_multiply_one_rightsecondrealdecode. (((ge_representation_real_code_multiply_one_rightsecond) = 2 * ge_signed_half_multiply_one_rightsecondrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightsecondreal) = 0) /\ (ge_balance_negative_multiply_one_rightsecondreal) = S ge_signed_half_multiply_one_rightsecondrealdecode))) /\ ((ge_second_rp_multiply_one_right) + ge_balance_negative_multiply_one_rightsecondreal = (ge_second_rn_multiply_one_right) + ge_balance_positive_multiply_one_rightsecondreal))) /\ (exists ge_balance_positive_multiply_one_rightsecondimaginary ge_balance_negative_multiply_one_rightsecondimaginary. (((((ge_representation_imaginary_code_multiply_one_rightsecond) = 2 * (ge_balance_positive_multiply_one_rightsecondimaginary) /\ (ge_balance_negative_multiply_one_rightsecondimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightsecond) = 2 * ge_signed_half_multiply_one_rightsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightsecondimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightsecondimaginary) = S ge_signed_half_multiply_one_rightsecondimaginarydecode))) /\ ((ge_second_ip_multiply_one_right) + ge_balance_negative_multiply_one_rightsecondimaginary = (ge_second_in_multiply_one_right) + ge_balance_positive_multiply_one_rightsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_one_rightoutput ge_representation_imaginary_code_multiply_one_rightoutput. (((a) = ((ge_representation_real_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput)) * S ((ge_representation_real_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput)) + ((ge_representation_imaginary_code_multiply_one_rightoutput) + (ge_representation_imaginary_code_multiply_one_rightoutput))) /\ ((exists ge_balance_positive_multiply_one_rightoutputreal ge_balance_negative_multiply_one_rightoutputreal. (((((ge_representation_real_code_multiply_one_rightoutput) = 2 * (ge_balance_positive_multiply_one_rightoutputreal) /\ (ge_balance_negative_multiply_one_rightoutputreal) = 0) \/ exists ge_signed_half_multiply_one_rightoutputrealdecode. (((ge_representation_real_code_multiply_one_rightoutput) = 2 * ge_signed_half_multiply_one_rightoutputrealdecode + 1 /\ (ge_balance_positive_multiply_one_rightoutputreal) = 0) /\ (ge_balance_negative_multiply_one_rightoutputreal) = S ge_signed_half_multiply_one_rightoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_one_right) * (ge_second_rp_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_rn_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_in_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_ip_multiply_one_right))))))) + ge_balance_negative_multiply_one_rightoutputreal = (((((((ge_first_rp_multiply_one_right) * (ge_second_rn_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_rp_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_ip_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_in_multiply_one_right))))))) + ge_balance_positive_multiply_one_rightoutputreal))) /\ (exists ge_balance_positive_multiply_one_rightoutputimaginary ge_balance_negative_multiply_one_rightoutputimaginary. (((((ge_representation_imaginary_code_multiply_one_rightoutput) = 2 * (ge_balance_positive_multiply_one_rightoutputimaginary) /\ (ge_balance_negative_multiply_one_rightoutputimaginary) = 0) \/ exists ge_signed_half_multiply_one_rightoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_one_rightoutput) = 2 * ge_signed_half_multiply_one_rightoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_one_rightoutputimaginary) = 0) /\ (ge_balance_negative_multiply_one_rightoutputimaginary) = S ge_signed_half_multiply_one_rightoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_one_right) * (ge_second_ip_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_in_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_rp_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_rn_multiply_one_right))))))) + ge_balance_negative_multiply_one_rightoutputimaginary = (((((((ge_first_rp_multiply_one_right) * (ge_second_in_multiply_one_right))) + (((ge_first_rn_multiply_one_right) * (ge_second_ip_multiply_one_right))))) + (((((ge_first_ip_multiply_one_right) * (ge_second_rn_multiply_one_right))) + (((ge_first_in_multiply_one_right) * (ge_second_rp_multiply_one_right))))))) + ge_balance_positive_multiply_one_rightoutputimaginary)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 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 GF000E gaussian_one_representation zero_add Stable theorem; checked-use authorized

Direct dependents

GF0029 gaussian_multiply_one_left GF003D gaussian_one_unit GF0044 gaussian_divides_reflexive GF005A gaussian_mutual_divisibility_associate GF005F gaussian_gcd_bezout_zero_right GF0060 gaussian_gcd_bezout_zero_case GF0068 gaussian_nonzero_product_divisor_unit_cofactor GF0092 gaussian_unit_empty_factorization

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 one 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 (6)
  3. L13
    specialize gaussian_multiply_of_representations (a)
  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 (1)
  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_one_representation
  5. L25
    specialize gaussian_representation_integer_transport (a)
  6. L26
    specialize gaussian_representation_integer_transport (x)
  7. L27
    specialize gaussian_representation_integer_transport (x1)
  8. L28
    specialize gaussian_representation_integer_transport (x2)
  9. L29
    specialize gaussian_representation_integer_transport (x3)
  10. L30
    specialize gaussian_representation_integer_transport (((((((x) * (1))) + (((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) * (1))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  2. L32
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (1))) + (((x3) * (0)))))))
  3. L33
    specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (1)))))))
  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 [zero_add]
  2. L37
    simp [zero_add]
09Use earlier factsL38–38

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

  1. L38
    exact hA_witness_witness_witness_witness

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 (6)
  13. 0013specialize gaussian_multiply_of_representations (a)
  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 (1)
  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_one_representation
  25. 0025specialize gaussian_representation_integer_transport (a)
  26. 0026specialize gaussian_representation_integer_transport (x)
  27. 0027specialize gaussian_representation_integer_transport (x1)
  28. 0028specialize gaussian_representation_integer_transport (x2)
  29. 0029specialize gaussian_representation_integer_transport (x3)
  30. 0030specialize gaussian_representation_integer_transport (((((((x) * (1))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  31. 0031specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (1))))) + (((((x2) * (0))) + (((x3) * (0)))))))
  32. 0032specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (1))) + (((x3) * (0)))))))
  33. 0033specialize gaussian_representation_integer_transport (((((((x) * (0))) + (((x1) * (0))))) + (((((x2) * (0))) + (((x3) * (1)))))))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035split
  36. 0036simp [zero_add]
  37. 0037simp [zero_add]
  38. 0038exact hA_witness_witness_witness_witness