FS002E · theorem body

four_square_euler_balance_aggregate

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

Four exact signed-coordinate square balances aggregate into the sum of their natural squares plus their full cross correction.

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

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

Proof neighborhood

Direct theorem prerequisites

FS002D four_square_euler_four_add_shuffle

Direct theorem dependents

FS002F four_square_euler_compensation_cancel

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

21 script commands · 4 reading checkpoints · 0 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 four add shuffle
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro n3
  2. L12
    intro m3
  3. L13
    intro h0
  4. L14
    intro h1
  5. L15
    intro h2
  6. L16
    intro h3
03Calculate and transport equalitiesL17–20

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

  1. L17
    rewrite h0
  2. L18
    rewrite h1
  3. L19
    rewrite h2
  4. L20
    rewrite h3
04Use earlier factsL21–21

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

  1. L21
    apply four_square_euler_four_add_shuffle

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro p0
  2. 0002intro n0
  3. 0003intro m0
  4. 0004intro p1
  5. 0005intro n1
  6. 0006intro m1
  7. 0007intro p2
  8. 0008intro n2
  9. 0009intro m2
  10. 0010intro p3
  11. 0011intro n3
  12. 0012intro m3
  13. 0013intro h0
  14. 0014intro h1
  15. 0015intro h2
  16. 0016intro h3
  17. 0017rewrite h0
  18. 0018rewrite h1
  19. 0019rewrite h2
  20. 0020rewrite h3
  21. 0021apply four_square_euler_four_add_shuffle