FS002I

four_square_euler_quaternion_conditional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The exact eight-variable quaternion Euler identity follows constructively from its one remaining subtraction-free global compensation equality.

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)) + (((((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) * (a * e) + (b * f + c * g + d * h) * (b * f + c * g + d * h)) + ((a * f + b * e + c * h) * (a * f + b * e + c * h) + (d * g) * (d * g))) + (((a * g + c * e + d * f) * (a * g + c * e + d * f) + (b * h) * (b * h)) + ((a * h + b * g + d * e) * (a * h + b * g + d * e) + (c * f) * (c * f)))))) -> ((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

The exact eight-variable quaternion Euler identity follows constructively from its one remaining subtraction-free global compensation equality.

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

FS000F quaternion_coordinate_square_transport FS002F four_square_euler_compensation_cancel add_assoc Stable theorem; checked-use authorized

Direct dependents

FS002Y four_square_euler_quaternion

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

54 script commands · 10 reading checkpoints · 1 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)
quaternion coordinate square transportfour square euler compensation cancel
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–14

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

  1. L11
    intro m2
  2. L12
    intro m3
  3. L13
    intro habsolute
  4. L14
    intro hcompensation
03Establish hbalancesL15–24

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have hbalances · expand full local formula (655 characters)have hbalances : (((a * e) * (a * e) + (b * f + c * g + d * h) * (b * f + c * g + d * h) = m0 * m0 + ((a * e) * (b * f + c * g + d * h) + (b * f + c * g + d * h) * (a * e))) /\ (((a * f + b * e + c * h) * (a * f + b * e + c * h) + (d * g) * (d * g) = m1 * m1 + ((a * f + b * e + c * h) * (d * g) + (d * g) * (a * f + b * e + c * h))) /\ (((a * g + c * e + d * f) * (a * g + c * e + d * f) + (b * h) * (b * h) = m2 * m2 + ((a * g + c * e + d * f) * (b * h) + (b * h) * (a * g + c * e + d * f))) /\ ((a * h + b * g + d * e) * (a * h + b * g + d * e) + (c * f) * (c * f) = m3 * m3 + ((a * h + b * g + d * e) * (c * f) + (c * f) * (a * h + b * g + d * e))))))
  2. L16
    specialize quaternion_coordinate_square_transport a
  3. L17
    specialize quaternion_coordinate_square_transport b
  4. L18
    specialize quaternion_coordinate_square_transport c
  5. L19
    specialize quaternion_coordinate_square_transport d
  6. L20
    specialize quaternion_coordinate_square_transport e
  7. L21
    specialize quaternion_coordinate_square_transport f
  8. L22
    specialize quaternion_coordinate_square_transport g
  9. L23
    specialize quaternion_coordinate_square_transport h
  10. L24
    specialize quaternion_coordinate_square_transport m0
04Use earlier factsL25–29

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

  1. L25
    specialize quaternion_coordinate_square_transport m1
  2. L26
    specialize quaternion_coordinate_square_transport m2
  3. L27
    specialize quaternion_coordinate_square_transport m3
  4. L28
    apply quaternion_coordinate_square_transport
  5. L29
    exact habsolute
05Separate the logical casesL30–32

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

  1. L30
    cases hbalances
  2. L31
    cases hbalances_right
  3. L32
    cases hbalances_right_right
06Calculate and transport equalitiesL33–33

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

  1. L33
    trans ((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3))))
07Use earlier factsL34–43

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

  1. L34
    specialize four_square_euler_compensation_cancel ((a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h))
  2. L35
    specialize four_square_euler_compensation_cancel (a * e)
  3. L36
    specialize four_square_euler_compensation_cancel (b * f + c * g + d * h)
  4. L37
    specialize four_square_euler_compensation_cancel m0
  5. L38
    specialize four_square_euler_compensation_cancel (a * f + b * e + c * h)
  6. L39
    specialize four_square_euler_compensation_cancel (d * g)
  7. L40
    specialize four_square_euler_compensation_cancel m1
  8. L41
    specialize four_square_euler_compensation_cancel (a * g + c * e + d * f)
  9. L42
    specialize four_square_euler_compensation_cancel (b * h)
  10. L43
    specialize four_square_euler_compensation_cancel m2
08Use earlier factsL44–52

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

  1. L44
    specialize four_square_euler_compensation_cancel (a * h + b * g + d * e)
  2. L45
    specialize four_square_euler_compensation_cancel (c * f)
  3. L46
    specialize four_square_euler_compensation_cancel m3
  4. L47
    apply four_square_euler_compensation_cancel
  5. L48
    exact hbalances_left
  6. L49
    exact hbalances_right_left
  7. L50
    exact hbalances_right_right_left
  8. L51
    exact hbalances_right_right_right
  9. L52
    exact hcompensation
09Calculate and transport equalitiesL53–53

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

  1. L53
    symm
10Use earlier factsL54–54

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

  1. L54
    apply add_assoc

Library-wide reading audit

Original exact command ledger · 54 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. 0014intro hcompensation
  15. 0015have hbalances : (((a * e) * (a * e) + (b * f + c * g + d * h) * (b * f + c * g + d * h) = m0 * m0 + ((a * e) * (b * f + c * g + d * h) + (b * f + c * g + d * h) * (a * e))) /\ (((a * f + b * e + c * h) * (a * f + b * e + c * h) + (d * g) * (d * g) = m1 * m1 + ((a * f + b * e + c * h) * (d * g) + (d * g) * (a * f + b * e + c * h))) /\ (((a * g + c * e + d * f) * (a * g + c * e + d * f) + (b * h) * (b * h) = m2 * m2 + ((a * g + c * e + d * f) * (b * h) + (b * h) * (a * g + c * e + d * f))) /\ ((a * h + b * g + d * e) * (a * h + b * g + d * e) + (c * f) * (c * f) = m3 * m3 + ((a * h + b * g + d * e) * (c * f) + (c * f) * (a * h + b * g + d * e))))))
  16. 0016specialize quaternion_coordinate_square_transport a
  17. 0017specialize quaternion_coordinate_square_transport b
  18. 0018specialize quaternion_coordinate_square_transport c
  19. 0019specialize quaternion_coordinate_square_transport d
  20. 0020specialize quaternion_coordinate_square_transport e
  21. 0021specialize quaternion_coordinate_square_transport f
  22. 0022specialize quaternion_coordinate_square_transport g
  23. 0023specialize quaternion_coordinate_square_transport h
  24. 0024specialize quaternion_coordinate_square_transport m0
  25. 0025specialize quaternion_coordinate_square_transport m1
  26. 0026specialize quaternion_coordinate_square_transport m2
  27. 0027specialize quaternion_coordinate_square_transport m3
  28. 0028apply quaternion_coordinate_square_transport
  29. 0029exact habsolute
  30. 0030cases hbalances
  31. 0031cases hbalances_right
  32. 0032cases hbalances_right_right
  33. 0033trans ((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3))))
  34. 0034specialize four_square_euler_compensation_cancel ((a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h))
  35. 0035specialize four_square_euler_compensation_cancel (a * e)
  36. 0036specialize four_square_euler_compensation_cancel (b * f + c * g + d * h)
  37. 0037specialize four_square_euler_compensation_cancel m0
  38. 0038specialize four_square_euler_compensation_cancel (a * f + b * e + c * h)
  39. 0039specialize four_square_euler_compensation_cancel (d * g)
  40. 0040specialize four_square_euler_compensation_cancel m1
  41. 0041specialize four_square_euler_compensation_cancel (a * g + c * e + d * f)
  42. 0042specialize four_square_euler_compensation_cancel (b * h)
  43. 0043specialize four_square_euler_compensation_cancel m2
  44. 0044specialize four_square_euler_compensation_cancel (a * h + b * g + d * e)
  45. 0045specialize four_square_euler_compensation_cancel (c * f)
  46. 0046specialize four_square_euler_compensation_cancel m3
  47. 0047apply four_square_euler_compensation_cancel
  48. 0048exact hbalances_left
  49. 0049exact hbalances_right_left
  50. 0050exact hbalances_right_right_left
  51. 0051exact hbalances_right_right_right
  52. 0052exact hcompensation
  53. 0053symm
  54. 0054apply add_assoc