FS002V · theorem body

four_square_euler_cross_decomposition

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

The complete four-coordinate signed correction splits into its twelve exact symmetric mixed-product blocks.

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.

Statement with defined notation

forall a b c d e f g h. (((((a * e) * (b * f + c * g + d * h) + (b * f + c * g + d * h) * (a * e)) + ((a * f + b * e + c * h) * (d * g) + (d * g) * (a * f + b * e + c * h))) + (((a * g + c * e + d * f) * (b * h) + (b * h) * (a * g + c * e + d * f)) + ((a * h + b * g + d * e) * (c * f) + (c * f) * (a * h + b * g + d * e))))) = ((((((((((a * e) * (b * f)) + ((b * f) * (a * e)))) + ((((a * e) * (c * g)) + ((c * g) * (a * e))))) + ((((a * e) * (d * h)) + ((d * h) * (a * e)))))) + (((((((a * f) * (d * g)) + ((d * g) * (a * f)))) + ((((b * e) * (d * g)) + ((d * g) * (b * e))))) + ((((c * h) * (d * g)) + ((d * g) * (c * h))))))) + ((((((((a * g) * (b * h)) + ((b * h) * (a * g)))) + ((((b * h) * (c * e)) + ((c * e) * (b * h))))) + ((((b * h) * (d * f)) + ((d * f) * (b * h)))))) + (((((((a * h) * (c * f)) + ((c * f) * (a * h)))) + ((((b * g) * (c * f)) + ((c * f) * (b * g))))) + ((((c * f) * (d * e)) + ((d * e) * (c * f)))))))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

none
Exact expanded first-order statement
forall a b c d e f g h. (((((a * e) * (b * f + c * g + d * h) + (b * f + c * g + d * h) * (a * e)) + ((a * f + b * e + c * h) * (d * g) + (d * g) * (a * f + b * e + c * h))) + (((a * g + c * e + d * f) * (b * h) + (b * h) * (a * g + c * e + d * f)) + ((a * h + b * g + d * e) * (c * f) + (c * f) * (a * h + b * g + d * e))))) = ((((((((((a * e) * (b * f)) + ((b * f) * (a * e)))) + ((((a * e) * (c * g)) + ((c * g) * (a * e))))) + ((((a * e) * (d * h)) + ((d * h) * (a * e)))))) + (((((((a * f) * (d * g)) + ((d * g) * (a * f)))) + ((((b * e) * (d * g)) + ((d * g) * (b * e))))) + ((((c * h) * (d * g)) + ((d * g) * (c * h))))))) + ((((((((a * g) * (b * h)) + ((b * h) * (a * g)))) + ((((b * h) * (c * e)) + ((c * e) * (b * h))))) + ((((b * h) * (d * f)) + ((d * f) * (b * h)))))) + (((((((a * h) * (c * f)) + ((c * f) * (a * h)))) + ((((b * g) * (c * f)) + ((c * f) * (b * g))))) + ((((c * f) * (d * e)) + ((d * e) * (c * f)))))))))

Proof neighborhood

Direct theorem prerequisites

FS002P four_square_euler_cross_triple_expansion add_comm · Stable closed

Direct theorem dependents

FS002X four_square_euler_global_compensation

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

45 script commands · 22 reading checkpoints · 0 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 (1)
four square euler cross triple expansion
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
02Calculate and transport equalitiesL9–11

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

  1. L9
    congr
  2. L10
    congr
  3. L11
    trans ((((((a * e) * (b * f)) + ((b * f) * (a * e)))) + ((((a * e) * (c * g)) + ((c * g) * (a * e))))) + ((((a * e) * (d * h)) + ((d * h) * (a * e)))))
03Use earlier factsL12–12

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

  1. L12
    apply four_square_euler_cross_triple_expansion
04Calculate and transport equalitiesL13–18

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

  1. L13
    congr
  2. L14
    congr
  3. L15
    refl
  4. L16
    refl
  5. L17
    refl
  6. L18
    trans (d * g) * ((((a * f) + (b * e)) + (c * h))) + ((((a * f) + (b * e)) + (c * h))) * (d * g)
05Use earlier factsL19–19

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

  1. L19
    apply add_comm
06Calculate and transport equalitiesL20–20

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

  1. L20
    trans ((((((d * g) * (a * f)) + ((a * f) * (d * g)))) + ((((d * g) * (b * e)) + ((b * e) * (d * g))))) + ((((d * g) * (c * h)) + ((c * h) * (d * g)))))
07Use earlier factsL21–21

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

  1. L21
    apply four_square_euler_cross_triple_expansion
08Calculate and transport equalitiesL22–23

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

  1. L22
    congr
  2. L23
    congr
09Use earlier factsL24–26

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

  1. L24
    apply add_comm
  2. L25
    apply add_comm
  3. L26
    apply add_comm
10Calculate and transport equalitiesL27–28

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

  1. L27
    congr
  2. L28
    trans (b * h) * ((((a * g) + (c * e)) + (d * f))) + ((((a * g) + (c * e)) + (d * f))) * (b * h)
11Use earlier factsL29–29

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

  1. L29
    apply add_comm
12Calculate and transport equalitiesL30–30

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

  1. L30
    trans ((((((b * h) * (a * g)) + ((a * g) * (b * h)))) + ((((b * h) * (c * e)) + ((c * e) * (b * h))))) + ((((b * h) * (d * f)) + ((d * f) * (b * h)))))
13Use earlier factsL31–31

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

  1. L31
    apply four_square_euler_cross_triple_expansion
14Calculate and transport equalitiesL32–33

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

  1. L32
    congr
  2. L33
    congr
15Use earlier factsL34–34

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

  1. L34
    apply add_comm
16Calculate and transport equalitiesL35–37

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

  1. L35
    refl
  2. L36
    refl
  3. L37
    trans (c * f) * ((((a * h) + (b * g)) + (d * e))) + ((((a * h) + (b * g)) + (d * e))) * (c * f)
17Use earlier factsL38–38

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

  1. L38
    apply add_comm
18Calculate and transport equalitiesL39–39

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

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

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

  1. L40
    apply four_square_euler_cross_triple_expansion
20Calculate and transport equalitiesL41–42

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

  1. L41
    congr
  2. L42
    congr
21Use earlier factsL43–44

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

  1. L43
    apply add_comm
  2. L44
    apply add_comm
22Calculate and transport equalitiesL45–45

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

  1. L45
    refl

Library-wide reading audit

Original defined command ledger · 45 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. 0009congr
  10. 0010congr
  11. 0011trans ((((((a * e) * (b * f)) + ((b * f) * (a * e)))) + ((((a * e) * (c * g)) + ((c * g) * (a * e))))) + ((((a * e) * (d * h)) + ((d * h) * (a * e)))))
  12. 0012apply four_square_euler_cross_triple_expansion
  13. 0013congr
  14. 0014congr
  15. 0015refl
  16. 0016refl
  17. 0017refl
  18. 0018trans (d * g) * ((((a * f) + (b * e)) + (c * h))) + ((((a * f) + (b * e)) + (c * h))) * (d * g)
  19. 0019apply add_comm
  20. 0020trans ((((((d * g) * (a * f)) + ((a * f) * (d * g)))) + ((((d * g) * (b * e)) + ((b * e) * (d * g))))) + ((((d * g) * (c * h)) + ((c * h) * (d * g)))))
  21. 0021apply four_square_euler_cross_triple_expansion
  22. 0022congr
  23. 0023congr
  24. 0024apply add_comm
  25. 0025apply add_comm
  26. 0026apply add_comm
  27. 0027congr
  28. 0028trans (b * h) * ((((a * g) + (c * e)) + (d * f))) + ((((a * g) + (c * e)) + (d * f))) * (b * h)
  29. 0029apply add_comm
  30. 0030trans ((((((b * h) * (a * g)) + ((a * g) * (b * h)))) + ((((b * h) * (c * e)) + ((c * e) * (b * h))))) + ((((b * h) * (d * f)) + ((d * f) * (b * h)))))
  31. 0031apply four_square_euler_cross_triple_expansion
  32. 0032congr
  33. 0033congr
  34. 0034apply add_comm
  35. 0035refl
  36. 0036refl
  37. 0037trans (c * f) * ((((a * h) + (b * g)) + (d * e))) + ((((a * h) + (b * g)) + (d * e))) * (c * f)
  38. 0038apply add_comm
  39. 0039trans ((((((c * f) * (a * h)) + ((a * h) * (c * f)))) + ((((c * f) * (b * g)) + ((b * g) * (c * f))))) + ((((c * f) * (d * e)) + ((d * e) * (c * f)))))
  40. 0040apply four_square_euler_cross_triple_expansion
  41. 0041congr
  42. 0042congr
  43. 0043apply add_comm
  44. 0044apply add_comm
  45. 0045refl