FS0013 · theorem body

four_square_conjugate_absolute_coordinates_total

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

Every pair of natural four-square tuples has four explicit conjugate absolute coordinates satisfying the complete norm identity.

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

FS000H four_square_absolute_difference_total FS0012 four_square_signed_conjugate_quaternion

Direct theorem dependents

FS004Q four_square_signed_orientation_mask_00 FS004T four_square_signed_orientation_mask_03 FS004V four_square_signed_orientation_mask_05 FS004W four_square_signed_orientation_mask_06 FS004Z four_square_signed_orientation_mask_09 FS0050 four_square_signed_orientation_mask_10 FS0052 four_square_signed_orientation_mask_12 FS0055 four_square_signed_orientation_mask_15

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

48 script commands · 19 reading checkpoints · 4 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 absolute difference totalfour square signed conjugate quaternion
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
02Establish h0L9–12

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

  1. L9
    have h0 : exists magnitude. (((a * e + b * f + c * g + d * h) = (0) + magnitude) \/ ((0) = (a * e + b * f + c * g + d * h) + magnitude))
  2. L10
    specialize four_square_absolute_difference_total (a * e + b * f + c * g + d * h)
  3. L11
    specialize four_square_absolute_difference_total (0)
  4. L12
    exact four_square_absolute_difference_total
03Establish h1L13–16

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

  1. L13
    have h1 : exists magnitude. (((a * f + c * h) = (b * e + d * g) + magnitude) \/ ((b * e + d * g) = (a * f + c * h) + magnitude))
  2. L14
    specialize four_square_absolute_difference_total (a * f + c * h)
  3. L15
    specialize four_square_absolute_difference_total (b * e + d * g)
  4. L16
    exact four_square_absolute_difference_total
04Establish h2L17–20

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

  1. L17
    have h2 : exists magnitude. (((a * g + d * f) = (c * e + b * h) + magnitude) \/ ((c * e + b * h) = (a * g + d * f) + magnitude))
  2. L18
    specialize four_square_absolute_difference_total (a * g + d * f)
  3. L19
    specialize four_square_absolute_difference_total (c * e + b * h)
  4. L20
    exact four_square_absolute_difference_total
05Establish h3L21–24

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

  1. L21
    have h3 : exists magnitude. (((a * h + b * g) = (d * e + c * f) + magnitude) \/ ((d * e + c * f) = (a * h + b * g) + magnitude))
  2. L22
    specialize four_square_absolute_difference_total (a * h + b * g)
  3. L23
    specialize four_square_absolute_difference_total (d * e + c * f)
  4. L24
    exact four_square_absolute_difference_total
06Separate the logical casesL25–28

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

  1. L25
    cases h0
  2. L26
    cases h1
  3. L27
    cases h2
  4. L28
    cases h3
07Construct an explicit witnessL29–32

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists x
  2. L30
    exists x1
  3. L31
    exists x2
  4. L32
    exists x3
08Separate the logical casesL33–34

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

  1. L33
    split
  2. L34
    split
09Use earlier factsL35–35

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

  1. L35
    exact h0_witness
10Separate the logical casesL36–36

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

  1. L36
    split
11Use earlier factsL37–37

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

  1. L37
    exact h1_witness
12Separate the logical casesL38–38

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

  1. L38
    split
13Use earlier factsL39–41

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

  1. L39
    exact h2_witness
  2. L40
    exact h3_witness
  3. L41
    apply four_square_signed_conjugate_quaternion
14Separate the logical casesL42–42

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

  1. L42
    split
15Use earlier factsL43–43

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

  1. L43
    exact h0_witness
16Separate the logical casesL44–44

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

  1. L44
    split
17Use earlier factsL45–45

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

  1. L45
    exact h1_witness
18Separate the logical casesL46–46

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

  1. L46
    split
19Use earlier factsL47–48

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

  1. L47
    exact h2_witness
  2. L48
    exact h3_witness

Library-wide reading audit

Original defined command ledger · 48 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. 0009have h0 : exists magnitude. (((a * e + b * f + c * g + d * h) = (0) + magnitude) \/ ((0) = (a * e + b * f + c * g + d * h) + magnitude))
  10. 0010specialize four_square_absolute_difference_total (a * e + b * f + c * g + d * h)
  11. 0011specialize four_square_absolute_difference_total (0)
  12. 0012exact four_square_absolute_difference_total
  13. 0013have h1 : exists magnitude. (((a * f + c * h) = (b * e + d * g) + magnitude) \/ ((b * e + d * g) = (a * f + c * h) + magnitude))
  14. 0014specialize four_square_absolute_difference_total (a * f + c * h)
  15. 0015specialize four_square_absolute_difference_total (b * e + d * g)
  16. 0016exact four_square_absolute_difference_total
  17. 0017have h2 : exists magnitude. (((a * g + d * f) = (c * e + b * h) + magnitude) \/ ((c * e + b * h) = (a * g + d * f) + magnitude))
  18. 0018specialize four_square_absolute_difference_total (a * g + d * f)
  19. 0019specialize four_square_absolute_difference_total (c * e + b * h)
  20. 0020exact four_square_absolute_difference_total
  21. 0021have h3 : exists magnitude. (((a * h + b * g) = (d * e + c * f) + magnitude) \/ ((d * e + c * f) = (a * h + b * g) + magnitude))
  22. 0022specialize four_square_absolute_difference_total (a * h + b * g)
  23. 0023specialize four_square_absolute_difference_total (d * e + c * f)
  24. 0024exact four_square_absolute_difference_total
  25. 0025cases h0
  26. 0026cases h1
  27. 0027cases h2
  28. 0028cases h3
  29. 0029exists x
  30. 0030exists x1
  31. 0031exists x2
  32. 0032exists x3
  33. 0033split
  34. 0034split
  35. 0035exact h0_witness
  36. 0036split
  37. 0037exact h1_witness
  38. 0038split
  39. 0039exact h2_witness
  40. 0040exact h3_witness
  41. 0041apply four_square_signed_conjugate_quaternion
  42. 0042split
  43. 0043exact h0_witness
  44. 0044split
  45. 0045exact h1_witness
  46. 0046split
  47. 0047exact h2_witness
  48. 0048exact h3_witness