GI0018

gaussian_signed_product_cross_interchange

The actual cross products (ac)(bd) and (ad)(bc) agree in both signed 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 · e + b · f) · (c · g + d · h) + (a · f + b · e) · (c · h + d · g) = (a · g + b · h) · (c · e + d · f) + (a · h + b · g) · (c · f + d · e) ∧ (a · e + b · f) · (c · h + d · g) + (a · f + b · e) · (c · g + d · h) = (a · g + b · h) · (c · f + d · e) + (a · h + b · g) · (c · e + d · f)

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

Definition DAG

none

Actual proof prerequisites

gaussian_signed_product_shufflegaussian_signed_product_commutative
Original expanded first-order statement 
forall a b c d e f g h. (((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (e))) + (((d) * (f))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (f))) + (((d) * (e)))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (f))) + (((d) * (e))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (e))) + (((d) * (f)))))))))))

Complete tactic proof in conservative notation

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

62 script commands · 23 reading checkpoints · 3 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 shufflegaussian signed product commutative
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–18

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

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

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

  1. L19
    cases hleft
04Establish hrightL20–29

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

  1. L20
    have hright · expand full local formula (642 characters)have hright : (((((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (e))) + (((d) * (f))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (f))) + (((d) * (e))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (e))) + (((h) * (f))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (f))) + (((h) * (e)))))))))) /\ ((((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (f))) + (((d) * (e))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (e))) + (((d) * (f))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (f))) + (((h) * (e))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (e))) + (((h) * (f)))))))))))
  2. L21
    specialize gaussian_signed_product_shuffle a
  3. L22
    specialize gaussian_signed_product_shuffle b
  4. L23
    specialize gaussian_signed_product_shuffle g
  5. L24
    specialize gaussian_signed_product_shuffle h
  6. L25
    specialize gaussian_signed_product_shuffle c
  7. L26
    specialize gaussian_signed_product_shuffle d
  8. L27
    specialize gaussian_signed_product_shuffle e
  9. L28
    specialize gaussian_signed_product_shuffle f
  10. L29
    apply gaussian_signed_product_shuffle
05Separate the logical casesL30–30

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

  1. L30
    cases hright
06Establish hcommuteL31–36

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

  1. L31
    have hcommute : (((((((e) * (g))) + (((f) * (h))))) = (((((g) * (e))) + (((h) * (f)))))) /\ ((((((e) * (h))) + (((f) * (g))))) = (((((g) * (f))) + (((h) * (e)))))))
  2. L32
    specialize gaussian_signed_product_commutative e
  3. L33
    specialize gaussian_signed_product_commutative f
  4. L34
    specialize gaussian_signed_product_commutative g
  5. L35
    specialize gaussian_signed_product_commutative h
  6. L36
    apply gaussian_signed_product_commutative
07Separate the logical casesL37–38

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

  1. L37
    cases hcommute
  2. L38
    split
08Calculate and transport equalitiesL39–39

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

  1. L39
    trans ((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g))))))))
09Use earlier factsL40–40

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

  1. L40
    exact hleft_left
10Calculate and transport equalitiesL41–44

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

  1. L41
    trans ((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (e))) + (((h) * (f))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (f))) + (((h) * (e))))))))
  2. L42
    congr
  3. L43
    congr
  4. L44
    refl
11Use earlier factsL45–45

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

  1. L45
    exact hcommute_left
12Calculate and transport equalitiesL46–47

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

  1. L46
    congr
  2. L47
    refl
13Use earlier factsL48–48

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

  1. L48
    exact hcommute_right
14Calculate and transport equalitiesL49–49

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

  1. L49
    symm
15Use earlier factsL50–50

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

  1. L50
    exact hright_left
16Calculate and transport equalitiesL51–51

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

  1. L51
    trans ((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h))))))))
17Use earlier factsL52–52

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

  1. L52
    exact hleft_right
18Calculate and transport equalitiesL53–56

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

  1. L53
    trans ((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (f))) + (((h) * (e))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (e))) + (((h) * (f))))))))
  2. L54
    congr
  3. L55
    congr
  4. L56
    refl
19Use earlier factsL57–57

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

  1. L57
    exact hcommute_right
20Calculate and transport equalitiesL58–59

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

  1. L58
    congr
  2. L59
    refl
21Use earlier factsL60–60

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

  1. L60
    exact hcommute_left
22Calculate and transport equalitiesL61–61

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

  1. L61
    symm
23Use earlier factsL62–62

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

  1. L62
    exact hright_right

Library-wide reading audit

Original defined command ledger · 62 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) * (e))) + (((b) * (f))))) * (((((c) * (g))) + (((d) * (h))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (h))) + (((d) * (g))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g)))))))))) /\ ((((((((((a) * (e))) + (((b) * (f))))) * (((((c) * (h))) + (((d) * (g))))))) + (((((((a) * (f))) + (((b) * (e))))) * (((((c) * (g))) + (((d) * (h))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h)))))))))))
  10. 0010specialize gaussian_signed_product_shuffle a
  11. 0011specialize gaussian_signed_product_shuffle b
  12. 0012specialize gaussian_signed_product_shuffle e
  13. 0013specialize gaussian_signed_product_shuffle f
  14. 0014specialize gaussian_signed_product_shuffle c
  15. 0015specialize gaussian_signed_product_shuffle d
  16. 0016specialize gaussian_signed_product_shuffle g
  17. 0017specialize gaussian_signed_product_shuffle h
  18. 0018apply gaussian_signed_product_shuffle
  19. 0019cases hleft
  20. 0020have hright : (((((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (e))) + (((d) * (f))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (f))) + (((d) * (e))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (e))) + (((h) * (f))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (f))) + (((h) * (e)))))))))) /\ ((((((((((a) * (g))) + (((b) * (h))))) * (((((c) * (f))) + (((d) * (e))))))) + (((((((a) * (h))) + (((b) * (g))))) * (((((c) * (e))) + (((d) * (f))))))))) = (((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (f))) + (((h) * (e))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (e))) + (((h) * (f)))))))))))
  21. 0021specialize gaussian_signed_product_shuffle a
  22. 0022specialize gaussian_signed_product_shuffle b
  23. 0023specialize gaussian_signed_product_shuffle g
  24. 0024specialize gaussian_signed_product_shuffle h
  25. 0025specialize gaussian_signed_product_shuffle c
  26. 0026specialize gaussian_signed_product_shuffle d
  27. 0027specialize gaussian_signed_product_shuffle e
  28. 0028specialize gaussian_signed_product_shuffle f
  29. 0029apply gaussian_signed_product_shuffle
  30. 0030cases hright
  31. 0031have hcommute : (((((((e) * (g))) + (((f) * (h))))) = (((((g) * (e))) + (((h) * (f)))))) /\ ((((((e) * (h))) + (((f) * (g))))) = (((((g) * (f))) + (((h) * (e)))))))
  32. 0032specialize gaussian_signed_product_commutative e
  33. 0033specialize gaussian_signed_product_commutative f
  34. 0034specialize gaussian_signed_product_commutative g
  35. 0035specialize gaussian_signed_product_commutative h
  36. 0036apply gaussian_signed_product_commutative
  37. 0037cases hcommute
  38. 0038split
  39. 0039trans ((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (g))) + (((f) * (h))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (h))) + (((f) * (g))))))))
  40. 0040exact hleft_left
  41. 0041trans ((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (e))) + (((h) * (f))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (f))) + (((h) * (e))))))))
  42. 0042congr
  43. 0043congr
  44. 0044refl
  45. 0045exact hcommute_left
  46. 0046congr
  47. 0047refl
  48. 0048exact hcommute_right
  49. 0049symm
  50. 0050exact hright_left
  51. 0051trans ((((((((a) * (c))) + (((b) * (d))))) * (((((e) * (h))) + (((f) * (g))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((e) * (g))) + (((f) * (h))))))))
  52. 0052exact hleft_right
  53. 0053trans ((((((((a) * (c))) + (((b) * (d))))) * (((((g) * (f))) + (((h) * (e))))))) + (((((((a) * (d))) + (((b) * (c))))) * (((((g) * (e))) + (((h) * (f))))))))
  54. 0054congr
  55. 0055congr
  56. 0056refl
  57. 0057exact hcommute_right
  58. 0058congr
  59. 0059refl
  60. 0060exact hcommute_left
  61. 0061symm
  62. 0062exact hright_right