FS0013

four_square_conjugate_absolute_coordinates_total

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

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

Constructive proof overview

Generated structural guide

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

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

FS000H four_square_absolute_difference_total FS0012 four_square_signed_conjugate_quaternion

Direct 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

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

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.

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