FS002H

four_square_euler_diagonal_expansion

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The complete eight-variable quaternion norm product expands into exactly its sixteen squared coordinate products.

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. (a * a + b * b + c * c + d * d) * (e * e + f * f + g * g + h * h) = ((a * e) * (a * e) + (a * f) * (a * f) + (a * g) * (a * g) + (a * h) * (a * h)) + ((b * e) * (b * e) + (b * f) * (b * f) + (b * g) * (b * g) + (b * h) * (b * h)) + ((c * e) * (c * e) + (c * f) * (c * f) + (c * g) * (c * g) + (c * h) * (c * h)) + ((d * e) * (d * e) + (d * f) * (d * f) + (d * g) * (d * g) + (d * h) * (d * h))

Constructive proof overview

Generated structural guide

The complete eight-variable quaternion norm product expands into exactly its sixteen squared coordinate products.

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

FS0003 four_square_norm_distributes FS002G four_square_euler_diagonal_block

Direct dependents

FS0010 four_square_conjugate_global_compensation FS002X four_square_euler_global_compensation

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

24 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.

Named ingredients (2)
four square norm distributesfour square euler diagonal block
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
02Use earlier factsL9–16

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

  1. L9
    specialize four_square_norm_distributes a
  2. L10
    specialize four_square_norm_distributes b
  3. L11
    specialize four_square_norm_distributes c
  4. L12
    specialize four_square_norm_distributes d
  5. L13
    specialize four_square_norm_distributes e
  6. L14
    specialize four_square_norm_distributes f
  7. L15
    specialize four_square_norm_distributes g
  8. L16
    specialize four_square_norm_distributes h
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 four_square_norm_distributes
  2. L18
    congr
  3. L19
    congr
  4. L20
    congr
04Use earlier factsL21–24

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

  1. L21
    apply four_square_euler_diagonal_block
  2. L22
    apply four_square_euler_diagonal_block
  3. L23
    apply four_square_euler_diagonal_block
  4. L24
    apply four_square_euler_diagonal_block

Library-wide reading audit

Original exact command ledger · 24 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. 0009specialize four_square_norm_distributes a
  10. 0010specialize four_square_norm_distributes b
  11. 0011specialize four_square_norm_distributes c
  12. 0012specialize four_square_norm_distributes d
  13. 0013specialize four_square_norm_distributes e
  14. 0014specialize four_square_norm_distributes f
  15. 0015specialize four_square_norm_distributes g
  16. 0016specialize four_square_norm_distributes h
  17. 0017rewrite four_square_norm_distributes
  18. 0018congr
  19. 0019congr
  20. 0020congr
  21. 0021apply four_square_euler_diagonal_block
  22. 0022apply four_square_euler_diagonal_block
  23. 0023apply four_square_euler_diagonal_block
  24. 0024apply four_square_euler_diagonal_block