FS002Y · theorem body

four_square_euler_quaternion

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

Euler's complete eight-variable quaternion four-square identity holds unconditionally for all constructively chosen natural absolute coordinates.

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 m0 m1 m2 m3. ((((a * e) = (b * f + c * g + d * h) + m0) \/ ((b * f + c * g + d * h) = (a * e) + m0)) /\ ((((a * f + b * e + c * h) = (d * g) + m1) \/ ((d * g) = (a * f + b * e + c * h) + m1)) /\ ((((a * g + c * e + d * f) = (b * h) + m2) \/ ((b * h) = (a * g + c * e + d * f) + m2)) /\ (((a * h + b * g + d * e) = (c * f) + m3) \/ ((c * f) = (a * h + b * g + d * e) + m3))))) -> ((a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h)) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3

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 m0 m1 m2 m3. ((((a * e) = (b * f + c * g + d * h) + m0) \/ ((b * f + c * g + d * h) = (a * e) + m0)) /\ ((((a * f + b * e + c * h) = (d * g) + m1) \/ ((d * g) = (a * f + b * e + c * h) + m1)) /\ ((((a * g + c * e + d * f) = (b * h) + m2) \/ ((b * h) = (a * g + c * e + d * f) + m2)) /\ (((a * h + b * g + d * e) = (c * f) + m3) \/ ((c * f) = (a * h + b * g + d * e) + m3))))) -> ((a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h)) = m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3

Proof neighborhood

Direct theorem prerequisites

FS002I four_square_euler_quaternion_conditional FS002X four_square_euler_global_compensation

Direct theorem dependents

FS001D four_square_descent_quaternion_quotient FS002Z four_square_euler_four_square_product_total FS004R four_square_signed_orientation_mask_01 FS004S four_square_signed_orientation_mask_02 FS004U four_square_signed_orientation_mask_04 FS004X four_square_signed_orientation_mask_07 FS004Y four_square_signed_orientation_mask_08 FS0051 four_square_signed_orientation_mask_11 FS0053 four_square_signed_orientation_mask_13 FS0054 four_square_signed_orientation_mask_14

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

28 script commands · 4 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 (2)
four square euler quaternion conditionalfour square euler global compensation
01Fix variables and assumptionsL1–10

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
  9. L9
    intro m0
  10. L10
    intro m1
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro m2
  2. L12
    intro m3
  3. L13
    intro habsolute
03Use earlier factsL14–23

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

  1. L14
    specialize four_square_euler_quaternion_conditional a
  2. L15
    specialize four_square_euler_quaternion_conditional b
  3. L16
    specialize four_square_euler_quaternion_conditional c
  4. L17
    specialize four_square_euler_quaternion_conditional d
  5. L18
    specialize four_square_euler_quaternion_conditional e
  6. L19
    specialize four_square_euler_quaternion_conditional f
  7. L20
    specialize four_square_euler_quaternion_conditional g
  8. L21
    specialize four_square_euler_quaternion_conditional h
  9. L22
    specialize four_square_euler_quaternion_conditional m0
  10. L23
    specialize four_square_euler_quaternion_conditional m1
04Use earlier factsL24–28

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

  1. L24
    specialize four_square_euler_quaternion_conditional m2
  2. L25
    specialize four_square_euler_quaternion_conditional m3
  3. L26
    apply four_square_euler_quaternion_conditional
  4. L27
    exact habsolute
  5. L28
    apply four_square_euler_global_compensation

Library-wide reading audit

Original defined command ledger · 28 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. 0009intro m0
  10. 0010intro m1
  11. 0011intro m2
  12. 0012intro m3
  13. 0013intro habsolute
  14. 0014specialize four_square_euler_quaternion_conditional a
  15. 0015specialize four_square_euler_quaternion_conditional b
  16. 0016specialize four_square_euler_quaternion_conditional c
  17. 0017specialize four_square_euler_quaternion_conditional d
  18. 0018specialize four_square_euler_quaternion_conditional e
  19. 0019specialize four_square_euler_quaternion_conditional f
  20. 0020specialize four_square_euler_quaternion_conditional g
  21. 0021specialize four_square_euler_quaternion_conditional h
  22. 0022specialize four_square_euler_quaternion_conditional m0
  23. 0023specialize four_square_euler_quaternion_conditional m1
  24. 0024specialize four_square_euler_quaternion_conditional m2
  25. 0025specialize four_square_euler_quaternion_conditional m3
  26. 0026apply four_square_euler_quaternion_conditional
  27. 0027exact habsolute
  28. 0028apply four_square_euler_global_compensation