FS002V

four_square_euler_cross_decomposition

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 45 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

FS002P four_square_euler_cross_triple_expansion add_comm Stable theorem; checked-use authorized

Direct dependents

FS002X four_square_euler_global_compensation

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

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.

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 exact 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