FS001D

four_square_descent_quaternion_quotient

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

A centered quaternion product whose four absolute coordinates are all k-divisible yields the exact four-square quotient p·r.

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 p k r a b c d e f g h u v w x. ~(k = 0) -> p * k = (a * a + b * b + c * c + d * d) -> k * r = (e * e + f * f + g * g + h * h) -> ((((a * e) = (b * f + c * g + d * h) + (k * u)) \/ ((b * f + c * g + d * h) = (a * e) + (k * u))) /\ ((((a * f + b * e + c * h) = (d * g) + (k * v)) \/ ((d * g) = (a * f + b * e + c * h) + (k * v))) /\ ((((a * g + c * e + d * f) = (b * h) + (k * w)) \/ ((b * h) = (a * g + c * e + d * f) + (k * w))) /\ (((a * h + b * g + d * e) = (c * f) + (k * x)) \/ ((c * f) = (a * h + b * g + d * e) + (k * x)))))) -> p * r = (u * u + v * v + w * w + x * x)

Constructive proof overview

Generated structural guide

A centered quaternion product whose four absolute coordinates are all k-divisible yields the exact four-square quotient p·r.

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

FS002Y four_square_euler_quaternion FS001C four_square_descent_scaled_norm_quotient

Direct dependents

FS001E four_square_descent_strict_step_from_centered_quaternion

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

39 script commands · 6 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)
four square euler quaternionfour square descent scaled norm quotient
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro r
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro f
  10. L10
    intro g
02Fix variables and assumptionsL11–19

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

  1. L11
    intro h
  2. L12
    intro u
  3. L13
    intro v
  4. L14
    intro w
  5. L15
    intro x
  6. L16
    intro hnonzero
  7. L17
    intro hfirst
  8. L18
    intro hsecond
  9. L19
    intro hbalances
03Establish hnormL20–29

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

  1. L20
    have hnorm : (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h) = ((k * u) * (k * u) + (k * v) * (k * v) + (k * w) * (k * w) + (k * x) * (k * x))
  2. L21
    specialize four_square_euler_quaternion a
  3. L22
    specialize four_square_euler_quaternion b
  4. L23
    specialize four_square_euler_quaternion c
  5. L24
    specialize four_square_euler_quaternion d
  6. L25
    specialize four_square_euler_quaternion e
  7. L26
    specialize four_square_euler_quaternion f
  8. L27
    specialize four_square_euler_quaternion g
  9. L28
    specialize four_square_euler_quaternion h
  10. L29
    specialize four_square_euler_quaternion (k * u)
04Use earlier factsL30–34

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

  1. L30
    specialize four_square_euler_quaternion (k * v)
  2. L31
    specialize four_square_euler_quaternion (k * w)
  3. L32
    specialize four_square_euler_quaternion (k * x)
  4. L33
    apply four_square_euler_quaternion
  5. L34
    exact hbalances
05Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite <- hfirst at hnorm
  2. L36
    rewrite <- hsecond at hnorm
06Use earlier factsL37–39

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

  1. L37
    apply four_square_descent_scaled_norm_quotient
  2. L38
    exact hnonzero
  3. L39
    exact hnorm

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro r
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro h
  12. 0012intro u
  13. 0013intro v
  14. 0014intro w
  15. 0015intro x
  16. 0016intro hnonzero
  17. 0017intro hfirst
  18. 0018intro hsecond
  19. 0019intro hbalances
  20. 0020have hnorm : (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h) = ((k * u) * (k * u) + (k * v) * (k * v) + (k * w) * (k * w) + (k * x) * (k * x))
  21. 0021specialize four_square_euler_quaternion a
  22. 0022specialize four_square_euler_quaternion b
  23. 0023specialize four_square_euler_quaternion c
  24. 0024specialize four_square_euler_quaternion d
  25. 0025specialize four_square_euler_quaternion e
  26. 0026specialize four_square_euler_quaternion f
  27. 0027specialize four_square_euler_quaternion g
  28. 0028specialize four_square_euler_quaternion h
  29. 0029specialize four_square_euler_quaternion (k * u)
  30. 0030specialize four_square_euler_quaternion (k * v)
  31. 0031specialize four_square_euler_quaternion (k * w)
  32. 0032specialize four_square_euler_quaternion (k * x)
  33. 0033apply four_square_euler_quaternion
  34. 0034exact hbalances
  35. 0035rewrite <- hfirst at hnorm
  36. 0036rewrite <- hsecond at hnorm
  37. 0037apply four_square_descent_scaled_norm_quotient
  38. 0038exact hnonzero
  39. 0039exact hnorm