GI0017

gaussian_signed_product_shuffle

Four actual signed factors admit the exact middle-factor interchange, assembled from checked associative and commutative components.

Alpha v34 checked-use · first admitted v28 · 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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. (a · c + b · d) · (e · g + f · h) + (a · d + b · c) · (e · h + f · g) = (a · e + b · f) · (c · g + d · h) + (a · f + b · e) · (c · h + d · g) ∧ (a · c + b · d) · (e · h + f · g) + (a · d + b · c) · (e · g + f · h) = (a · e + b · f) · (c · h + d · g) + (a · f + b · e) · (c · g + d · h)

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

Definition DAG

none

Actual proof prerequisites

signed_pair_mul_components_associate · checked external prerequisitegaussian_signed_product_interchange_positivegaussian_signed_product_interchange_negative
Original expanded first-order statement 
forall a b c d e f g h. (((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g))))))))) = (((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g)))))))))) /\ ((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h))))))))) = (((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h)))))))))))

Complete tactic proof in conservative notation

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

67 script commands · 24 reading checkpoints · 4 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
gaussian signed product interchange positivegaussian signed product interchange negative
01Fix variables and assumptionsL1–8

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 d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
02Establish hleftL9–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed pair mul components associate.

  1. L9
    have hleft · expand full local formula (761 characters)have hleft : (((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g))))))))) = (((((a) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))) + (((b) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h)))))))))))))) /\ ((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h))))))))) = (((((a) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))) + (((b) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g)))))))))))))))
  2. L10
    specialize signed_pair_mul_components_associate a
  3. L11
    specialize signed_pair_mul_components_associate b
  4. L12
    specialize signed_pair_mul_components_associate c
  5. L13
    specialize signed_pair_mul_components_associate d
  6. L14
    specialize signed_pair_mul_components_associate ((((e) * (g))) + (((f) * (h))))
  7. L15
    specialize signed_pair_mul_components_associate ((((e) * (h))) + (((f) * (g))))
  8. L16
    apply signed_pair_mul_components_associate
03Separate the logical casesL17–17

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

  1. L17
    cases hleft
04Establish hrightL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed pair mul components associate.

  1. L18
    have hright · expand full local formula (762 characters)have hright : (((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((a) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))) + (((b) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h)))))))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((a) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))) + (((b) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g)))))))))))))))
  2. L19
    specialize signed_pair_mul_components_associate a
  3. L20
    specialize signed_pair_mul_components_associate b
  4. L21
    specialize signed_pair_mul_components_associate e
  5. L22
    specialize signed_pair_mul_components_associate f
  6. L23
    specialize signed_pair_mul_components_associate ((((c) * (g))) + (((d) * (h))))
  7. L24
    specialize signed_pair_mul_components_associate ((((c) * (h))) + (((d) * (g))))
  8. L25
    apply signed_pair_mul_components_associate
05Separate the logical casesL26–26

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

  1. L26
    cases hright
06Establish hmiddle_positiveL27–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian signed product interchange positive.

  1. L27
    have hmiddle_positive : ((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g)))))))) = ((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))
  2. L28
    specialize gaussian_signed_product_interchange_positive c
  3. L29
    specialize gaussian_signed_product_interchange_positive d
  4. L30
    specialize gaussian_signed_product_interchange_positive e
  5. L31
    specialize gaussian_signed_product_interchange_positive f
  6. L32
    specialize gaussian_signed_product_interchange_positive g
  7. L33
    specialize gaussian_signed_product_interchange_positive h
  8. L34
    apply gaussian_signed_product_interchange_positive
07Establish hmiddle_negativeL35–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian signed product interchange negative.

  1. L35
    have hmiddle_negative : ((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h)))))))) = ((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))
  2. L36
    specialize gaussian_signed_product_interchange_negative c
  3. L37
    specialize gaussian_signed_product_interchange_negative d
  4. L38
    specialize gaussian_signed_product_interchange_negative e
  5. L39
    specialize gaussian_signed_product_interchange_negative f
  6. L40
    specialize gaussian_signed_product_interchange_negative g
  7. L41
    specialize gaussian_signed_product_interchange_negative h
  8. L42
    apply gaussian_signed_product_interchange_negative
08Separate the logical casesL43–43

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

  1. L43
    split
09Calculate and transport equalitiesL44–44

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

  1. L44
    trans ((((a) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))) + (((b) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))))
10Use earlier factsL45–45

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

  1. L45
    exact hleft_left
11Calculate and transport equalitiesL46–49

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

  1. L46
    trans ((((a) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))) + (((b) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))))
  2. L47
    congr
  3. L48
    congr
  4. L49
    refl
12Use earlier factsL50–50

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

  1. L50
    exact hmiddle_positive
13Calculate and transport equalitiesL51–52

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

  1. L51
    congr
  2. L52
    refl
14Use earlier factsL53–53

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

  1. L53
    exact hmiddle_negative
15Calculate and transport equalitiesL54–54

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

  1. L54
    symm
16Use earlier factsL55–55

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

  1. L55
    exact hright_left
17Calculate and transport equalitiesL56–56

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

  1. L56
    trans ((((a) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))) + (((b) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))))
18Use earlier factsL57–57

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

  1. L57
    exact hleft_right
19Calculate and transport equalitiesL58–61

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

  1. L58
    trans ((((a) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))) + (((b) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))))
  2. L59
    congr
  3. L60
    congr
  4. L61
    refl
20Use earlier factsL62–62

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

  1. L62
    exact hmiddle_negative
21Calculate and transport equalitiesL63–64

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

  1. L63
    congr
  2. L64
    refl
22Use earlier factsL65–65

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

  1. L65
    exact hmiddle_positive
23Calculate and transport equalitiesL66–66

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

  1. L66
    symm
24Use earlier factsL67–67

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

  1. L67
    exact hright_right

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009have hleft : (((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g))))))))) = (((((a) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))) + (((b) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h)))))))))))))) /\ ((((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h))))))))) = (((((a) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))) + (((b) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g)))))))))))))))
  10. 0010specialize signed_pair_mul_components_associate a
  11. 0011specialize signed_pair_mul_components_associate b
  12. 0012specialize signed_pair_mul_components_associate c
  13. 0013specialize signed_pair_mul_components_associate d
  14. 0014specialize signed_pair_mul_components_associate ((((e) * (g))) + (((f) * (h))))
  15. 0015specialize signed_pair_mul_components_associate ((((e) * (h))) + (((f) * (g))))
  16. 0016apply signed_pair_mul_components_associate
  17. 0017cases hleft
  18. 0018have hright : (((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((a) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))) + (((b) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h)))))))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((a) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))) + (((b) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g)))))))))))))))
  19. 0019specialize signed_pair_mul_components_associate a
  20. 0020specialize signed_pair_mul_components_associate b
  21. 0021specialize signed_pair_mul_components_associate e
  22. 0022specialize signed_pair_mul_components_associate f
  23. 0023specialize signed_pair_mul_components_associate ((((c) * (g))) + (((d) * (h))))
  24. 0024specialize signed_pair_mul_components_associate ((((c) * (h))) + (((d) * (g))))
  25. 0025apply signed_pair_mul_components_associate
  26. 0026cases hright
  27. 0027have hmiddle_positive : ((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g)))))))) = ((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))
  28. 0028specialize gaussian_signed_product_interchange_positive c
  29. 0029specialize gaussian_signed_product_interchange_positive d
  30. 0030specialize gaussian_signed_product_interchange_positive e
  31. 0031specialize gaussian_signed_product_interchange_positive f
  32. 0032specialize gaussian_signed_product_interchange_positive g
  33. 0033specialize gaussian_signed_product_interchange_positive h
  34. 0034apply gaussian_signed_product_interchange_positive
  35. 0035have hmiddle_negative : ((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h)))))))) = ((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))
  36. 0036specialize gaussian_signed_product_interchange_negative c
  37. 0037specialize gaussian_signed_product_interchange_negative d
  38. 0038specialize gaussian_signed_product_interchange_negative e
  39. 0039specialize gaussian_signed_product_interchange_negative f
  40. 0040specialize gaussian_signed_product_interchange_negative g
  41. 0041specialize gaussian_signed_product_interchange_negative h
  42. 0042apply gaussian_signed_product_interchange_negative
  43. 0043split
  44. 0044trans ((((a) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))) + (((b) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))))
  45. 0045exact hleft_left
  46. 0046trans ((((a) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))) + (((b) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))))
  47. 0047congr
  48. 0048congr
  49. 0049refl
  50. 0050exact hmiddle_positive
  51. 0051congr
  52. 0052refl
  53. 0053exact hmiddle_negative
  54. 0054symm
  55. 0055exact hright_left
  56. 0056trans ((((a) * (((((c) * (((((e) * (h))) + (((f) * (g))))))) + (((d) * (((((e) * (g))) + (((f) * (h))))))))))) + (((b) * (((((c) * (((((e) * (g))) + (((f) * (h))))))) + (((d) * (((((e) * (h))) + (((f) * (g))))))))))))
  57. 0057exact hleft_right
  58. 0058trans ((((a) * (((((e) * (((((c) * (h))) + (((d) * (g))))))) + (((f) * (((((c) * (g))) + (((d) * (h))))))))))) + (((b) * (((((e) * (((((c) * (g))) + (((d) * (h))))))) + (((f) * (((((c) * (h))) + (((d) * (g))))))))))))
  59. 0059congr
  60. 0060congr
  61. 0061refl
  62. 0062exact hmiddle_negative
  63. 0063congr
  64. 0064refl
  65. 0065exact hmiddle_positive
  66. 0066symm
  67. 0067exact hright_right