FS001D · theorem body

four_square_descent_quaternion_quotient

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

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.

Statement with defined notation

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)

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

Proof neighborhood

Direct theorem prerequisites

FS002Y four_square_euler_quaternion FS001C four_square_descent_scaled_norm_quotient

Direct theorem dependents

FS001E four_square_descent_strict_step_from_centered_quaternion

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

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.

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