FS002F · theorem body

four_square_euler_compensation_cancel

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

Ordinary constructive additive cancellation turns all four signed cross corrections into an exact 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 norm p0 n0 m0 p1 n1 m1 p2 n2 m2 p3 n3 m3. (((p0) * (p0) + (n0) * (n0)) = (((m0) * (m0)) + ((p0) * (n0) + (n0) * (p0)))) -> (((p1) * (p1) + (n1) * (n1)) = (((m1) * (m1)) + ((p1) * (n1) + (n1) * (p1)))) -> (((p2) * (p2) + (n2) * (n2)) = (((m2) * (m2)) + ((p2) * (n2) + (n2) * (p2)))) -> (((p3) * (p3) + (n3) * (n3)) = (((m3) * (m3)) + ((p3) * (n3) + (n3) * (p3)))) -> ((norm) + (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3))))) = (((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3)))))) -> norm = (((((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 norm p0 n0 m0 p1 n1 m1 p2 n2 m2 p3 n3 m3. (((p0) * (p0) + (n0) * (n0)) = (((m0) * (m0)) + ((p0) * (n0) + (n0) * (p0)))) -> (((p1) * (p1) + (n1) * (n1)) = (((m1) * (m1)) + ((p1) * (n1) + (n1) * (p1)))) -> (((p2) * (p2) + (n2) * (n2)) = (((m2) * (m2)) + ((p2) * (n2) + (n2) * (p2)))) -> (((p3) * (p3) + (n3) * (n3)) = (((m3) * (m3)) + ((p3) * (n3) + (n3) * (p3)))) -> ((norm) + (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3))))) = (((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3)))))) -> norm = (((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3)))))

Proof neighborhood

Direct theorem prerequisites

FS002E four_square_euler_balance_aggregate add_right_cancel · Stable closed

Direct theorem dependents

FS0012 four_square_signed_conjugate_quaternion FS002I four_square_euler_quaternion_conditional

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

43 script commands · 7 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 (1)
four square euler balance aggregate
01Fix variables and assumptionsL1–10

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

  1. L1
    intro norm
  2. L2
    intro p0
  3. L3
    intro n0
  4. L4
    intro m0
  5. L5
    intro p1
  6. L6
    intro n1
  7. L7
    intro m1
  8. L8
    intro p2
  9. L9
    intro n2
  10. L10
    intro m2
02Fix variables and assumptionsL11–18

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

  1. L11
    intro p3
  2. L12
    intro n3
  3. L13
    intro m3
  4. L14
    intro h0
  5. L15
    intro h1
  6. L16
    intro h2
  7. L17
    intro h3
  8. L18
    intro hcompensation
03Establish hgroupL19–28

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

  1. L19
    have hgroup : (((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3))))) = ((((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3))))) + (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3))))))
  2. L20
    specialize four_square_euler_balance_aggregate p0
  3. L21
    specialize four_square_euler_balance_aggregate n0
  4. L22
    specialize four_square_euler_balance_aggregate m0
  5. L23
    specialize four_square_euler_balance_aggregate p1
  6. L24
    specialize four_square_euler_balance_aggregate n1
  7. L25
    specialize four_square_euler_balance_aggregate m1
  8. L26
    specialize four_square_euler_balance_aggregate p2
  9. L27
    specialize four_square_euler_balance_aggregate n2
  10. L28
    specialize four_square_euler_balance_aggregate m2
04Use earlier factsL29–38

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

  1. L29
    specialize four_square_euler_balance_aggregate p3
  2. L30
    specialize four_square_euler_balance_aggregate n3
  3. L31
    specialize four_square_euler_balance_aggregate m3
  4. L32
    apply four_square_euler_balance_aggregate
  5. L33
    exact h0
  6. L34
    exact h1
  7. L35
    exact h2
  8. L36
    exact h3
  9. L37
    specialize add_right_cancel norm
  10. L38
    specialize add_right_cancel (((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3)))))
05Use earlier factsL39–40

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

  1. L39
    specialize add_right_cancel (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3)))))
  2. L40
    apply add_right_cancel
06Calculate and transport equalitiesL41–41

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

  1. L41
    trans ((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3))))
07Use earlier factsL42–43

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

  1. L42
    exact hcompensation
  2. L43
    exact hgroup

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro norm
  2. 0002intro p0
  3. 0003intro n0
  4. 0004intro m0
  5. 0005intro p1
  6. 0006intro n1
  7. 0007intro m1
  8. 0008intro p2
  9. 0009intro n2
  10. 0010intro m2
  11. 0011intro p3
  12. 0012intro n3
  13. 0013intro m3
  14. 0014intro h0
  15. 0015intro h1
  16. 0016intro h2
  17. 0017intro h3
  18. 0018intro hcompensation
  19. 0019have hgroup : (((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3))))) = ((((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3))))) + (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3))))))
  20. 0020specialize four_square_euler_balance_aggregate p0
  21. 0021specialize four_square_euler_balance_aggregate n0
  22. 0022specialize four_square_euler_balance_aggregate m0
  23. 0023specialize four_square_euler_balance_aggregate p1
  24. 0024specialize four_square_euler_balance_aggregate n1
  25. 0025specialize four_square_euler_balance_aggregate m1
  26. 0026specialize four_square_euler_balance_aggregate p2
  27. 0027specialize four_square_euler_balance_aggregate n2
  28. 0028specialize four_square_euler_balance_aggregate m2
  29. 0029specialize four_square_euler_balance_aggregate p3
  30. 0030specialize four_square_euler_balance_aggregate n3
  31. 0031specialize four_square_euler_balance_aggregate m3
  32. 0032apply four_square_euler_balance_aggregate
  33. 0033exact h0
  34. 0034exact h1
  35. 0035exact h2
  36. 0036exact h3
  37. 0037specialize add_right_cancel norm
  38. 0038specialize add_right_cancel (((((m0) * (m0)) + ((m1) * (m1))) + (((m2) * (m2)) + ((m3) * (m3)))))
  39. 0039specialize add_right_cancel (((((p0) * (n0) + (n0) * (p0)) + ((p1) * (n1) + (n1) * (p1))) + (((p2) * (n2) + (n2) * (p2)) + ((p3) * (n3) + (n3) * (p3)))))
  40. 0040apply add_right_cancel
  41. 0041trans ((((p0) * (p0) + (n0) * (n0)) + ((p1) * (p1) + (n1) * (n1))) + (((p2) * (p2) + (n2) * (n2)) + ((p3) * (p3) + (n3) * (n3))))
  42. 0042exact hcompensation
  43. 0043exact hgroup