FS0012 · theorem body

four_square_signed_conjugate_quaternion

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

Euler's full eight-variable conjugate quaternion identity holds for the all-positive scalar and all three exact two-positive/two-negative vector 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) = (0) + m0) \/ ((0) = (a * e + b * f + c * g + d * h) + m0)) /\ ((((a * f + c * h) = (b * e + d * g) + m1) \/ ((b * e + d * g) = (a * f + c * h) + m1)) /\ ((((a * g + d * f) = (c * e + b * h) + m2) \/ ((c * e + b * h) = (a * g + d * f) + m2)) /\ (((a * h + b * g) = (d * e + c * f) + m3) \/ ((d * e + c * f) = (a * h + b * g) + 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) = (0) + m0) \/ ((0) = (a * e + b * f + c * g + d * h) + m0)) /\ ((((a * f + c * h) = (b * e + d * g) + m1) \/ ((b * e + d * g) = (a * f + c * h) + m1)) /\ ((((a * g + d * f) = (c * e + b * h) + m2) \/ ((c * e + b * h) = (a * g + d * f) + m2)) /\ (((a * h + b * g) = (d * e + c * f) + m3) \/ ((d * e + c * f) = (a * h + b * g) + 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

FS0011 four_square_conjugate_coordinate_square_transport FS002F four_square_euler_compensation_cancel FS0010 four_square_conjugate_global_compensation add_assoc · Stable closed

Direct theorem dependents

FS0013 four_square_conjugate_absolute_coordinates_total

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

53 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.

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 (3)
four square conjugate coordinate square transportfour square euler compensation cancelfour square conjugate 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
03Establish hbalancesL14–23

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

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

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

  1. L24
    specialize four_square_conjugate_coordinate_square_transport m1
  2. L25
    specialize four_square_conjugate_coordinate_square_transport m2
  3. L26
    specialize four_square_conjugate_coordinate_square_transport m3
  4. L27
    apply four_square_conjugate_coordinate_square_transport
  5. L28
    exact habsolute
05Separate the logical casesL29–31

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

  1. L29
    cases hbalances
  2. L30
    cases hbalances_right
  3. L31
    cases hbalances_right_right
06Calculate and transport equalitiesL32–32

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

  1. L32
    trans ((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3))))
07Use earlier factsL33–42

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

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

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

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

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

  1. L52
    symm
10Use earlier factsL53–53

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

  1. L53
    apply add_assoc

Library-wide reading audit

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