FS002Y

four_square_euler_quaternion

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 28 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

FS002I four_square_euler_quaternion_conditional FS002X four_square_euler_global_compensation

Direct 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

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

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.

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