FS005C

four_square_signed_centered_norm_congruent

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

All sixteen independent sign patterns yield the same constructive modular congruence between original and centered four-square norms.

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 k a b c d e f g h. (((exists fsd_center_bound_fssq_a. fsd_center_bound_fssq_a + (e + e) = k) /\ ((exists fsd_center_lower_fssq_a. a = k * fsd_center_lower_fssq_a + e) \/ (exists fsd_center_upper_fssq_a. a + e = k * fsd_center_upper_fssq_a)))) -> (((exists fsd_center_bound_fssq_b. fsd_center_bound_fssq_b + (f + f) = k) /\ ((exists fsd_center_lower_fssq_b. b = k * fsd_center_lower_fssq_b + f) \/ (exists fsd_center_upper_fssq_b. b + f = k * fsd_center_upper_fssq_b)))) -> (((exists fsd_center_bound_fssq_c. fsd_center_bound_fssq_c + (g + g) = k) /\ ((exists fsd_center_lower_fssq_c. c = k * fsd_center_lower_fssq_c + g) \/ (exists fsd_center_upper_fssq_c. c + g = k * fsd_center_upper_fssq_c)))) -> (((exists fsd_center_bound_fssq_d. fsd_center_bound_fssq_d + (h + h) = k) /\ ((exists fsd_center_lower_fssq_d. d = k * fsd_center_lower_fssq_d + h) \/ (exists fsd_center_upper_fssq_d. d + h = k * fsd_center_upper_fssq_d)))) -> (exists ftcn_left_fssq_norm ftcn_right_fssq_norm. (a * a + b * b + c * c + d * d) + (k) * ftcn_left_fssq_norm = (e * e + f * f + g * g + h * h) + (k) * ftcn_right_fssq_norm)

Constructive proof overview

Generated structural guide

All sixteen independent sign patterns yield the same constructive modular congruence between original and centered four-square norms.

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

FS005B four_square_signed_centered_square_congruent mod_eq_add Stable theorem; checked-use authorized

Direct dependents

FS005D four_square_signed_centered_norm_quotient_exists

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

63 script commands · 9 reading checkpoints · 6 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 (1)
four square signed centered square congruent
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hb
  2. L12
    intro hc
  3. L13
    intro hd
03Establish hfirstL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered square congruent.

  1. L14
    have hfirst : exists ftcn_left_fssq_first ftcn_right_fssq_first. (a * a) + (k) * ftcn_left_fssq_first = (e * e) + (k) * ftcn_right_fssq_first
  2. L15
    specialize four_square_signed_centered_square_congruent k
  3. L16
    specialize four_square_signed_centered_square_congruent a
  4. L17
    specialize four_square_signed_centered_square_congruent e
  5. L18
    apply four_square_signed_centered_square_congruent
  6. L19
    exact ha
04Establish hsecondL20–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered square congruent.

  1. L20
    have hsecond : exists ftcn_left_fssq_second ftcn_right_fssq_second. (b * b) + (k) * ftcn_left_fssq_second = (f * f) + (k) * ftcn_right_fssq_second
  2. L21
    specialize four_square_signed_centered_square_congruent k
  3. L22
    specialize four_square_signed_centered_square_congruent b
  4. L23
    specialize four_square_signed_centered_square_congruent f
  5. L24
    apply four_square_signed_centered_square_congruent
  6. L25
    exact hb
05Establish hthirdL26–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered square congruent.

  1. L26
    have hthird : exists ftcn_left_fssq_third ftcn_right_fssq_third. (c * c) + (k) * ftcn_left_fssq_third = (g * g) + (k) * ftcn_right_fssq_third
  2. L27
    specialize four_square_signed_centered_square_congruent k
  3. L28
    specialize four_square_signed_centered_square_congruent c
  4. L29
    specialize four_square_signed_centered_square_congruent g
  5. L30
    apply four_square_signed_centered_square_congruent
  6. L31
    exact hc
06Establish hfourthL32–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed centered square congruent.

  1. L32
    have hfourth : exists ftcn_left_fssq_fourth ftcn_right_fssq_fourth. (d * d) + (k) * ftcn_left_fssq_fourth = (h * h) + (k) * ftcn_right_fssq_fourth
  2. L33
    specialize four_square_signed_centered_square_congruent k
  3. L34
    specialize four_square_signed_centered_square_congruent d
  4. L35
    specialize four_square_signed_centered_square_congruent h
  5. L36
    apply four_square_signed_centered_square_congruent
  6. L37
    exact hd
07Establish hpairL38–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L38
    have hpair : exists ftcn_left_fssq_pair ftcn_right_fssq_pair. (a * a + b * b) + (k) * ftcn_left_fssq_pair = (e * e + f * f) + (k) * ftcn_right_fssq_pair
  2. L39
    specialize mod_eq_add k
  3. L40
    specialize mod_eq_add (a * a)
  4. L41
    specialize mod_eq_add (e * e)
  5. L42
    specialize mod_eq_add (b * b)
  6. L43
    specialize mod_eq_add (f * f)
  7. L44
    apply mod_eq_add
  8. L45
    exact hfirst
  9. L46
    exact hsecond
08Establish htripleL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L47
    have htriple : exists ftcn_left_fssq_triple ftcn_right_fssq_triple. (a * a + b * b + c * c) + (k) * ftcn_left_fssq_triple = (e * e + f * f + g * g) + (k) * ftcn_right_fssq_triple
  2. L48
    specialize mod_eq_add k
  3. L49
    specialize mod_eq_add (a * a + b * b)
  4. L50
    specialize mod_eq_add (e * e + f * f)
  5. L51
    specialize mod_eq_add (c * c)
  6. L52
    specialize mod_eq_add (g * g)
  7. L53
    apply mod_eq_add
  8. L54
    exact hpair
  9. L55
    exact hthird
  10. L56
    specialize mod_eq_add k
09Use earlier factsL57–63

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

  1. L57
    specialize mod_eq_add (a * a + b * b + c * c)
  2. L58
    specialize mod_eq_add (e * e + f * f + g * g)
  3. L59
    specialize mod_eq_add (d * d)
  4. L60
    specialize mod_eq_add (h * h)
  5. L61
    apply mod_eq_add
  6. L62
    exact htriple
  7. L63
    exact hfourth

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro h
  10. 0010intro ha
  11. 0011intro hb
  12. 0012intro hc
  13. 0013intro hd
  14. 0014have hfirst : exists ftcn_left_fssq_first ftcn_right_fssq_first. (a * a) + (k) * ftcn_left_fssq_first = (e * e) + (k) * ftcn_right_fssq_first
  15. 0015specialize four_square_signed_centered_square_congruent k
  16. 0016specialize four_square_signed_centered_square_congruent a
  17. 0017specialize four_square_signed_centered_square_congruent e
  18. 0018apply four_square_signed_centered_square_congruent
  19. 0019exact ha
  20. 0020have hsecond : exists ftcn_left_fssq_second ftcn_right_fssq_second. (b * b) + (k) * ftcn_left_fssq_second = (f * f) + (k) * ftcn_right_fssq_second
  21. 0021specialize four_square_signed_centered_square_congruent k
  22. 0022specialize four_square_signed_centered_square_congruent b
  23. 0023specialize four_square_signed_centered_square_congruent f
  24. 0024apply four_square_signed_centered_square_congruent
  25. 0025exact hb
  26. 0026have hthird : exists ftcn_left_fssq_third ftcn_right_fssq_third. (c * c) + (k) * ftcn_left_fssq_third = (g * g) + (k) * ftcn_right_fssq_third
  27. 0027specialize four_square_signed_centered_square_congruent k
  28. 0028specialize four_square_signed_centered_square_congruent c
  29. 0029specialize four_square_signed_centered_square_congruent g
  30. 0030apply four_square_signed_centered_square_congruent
  31. 0031exact hc
  32. 0032have hfourth : exists ftcn_left_fssq_fourth ftcn_right_fssq_fourth. (d * d) + (k) * ftcn_left_fssq_fourth = (h * h) + (k) * ftcn_right_fssq_fourth
  33. 0033specialize four_square_signed_centered_square_congruent k
  34. 0034specialize four_square_signed_centered_square_congruent d
  35. 0035specialize four_square_signed_centered_square_congruent h
  36. 0036apply four_square_signed_centered_square_congruent
  37. 0037exact hd
  38. 0038have hpair : exists ftcn_left_fssq_pair ftcn_right_fssq_pair. (a * a + b * b) + (k) * ftcn_left_fssq_pair = (e * e + f * f) + (k) * ftcn_right_fssq_pair
  39. 0039specialize mod_eq_add k
  40. 0040specialize mod_eq_add (a * a)
  41. 0041specialize mod_eq_add (e * e)
  42. 0042specialize mod_eq_add (b * b)
  43. 0043specialize mod_eq_add (f * f)
  44. 0044apply mod_eq_add
  45. 0045exact hfirst
  46. 0046exact hsecond
  47. 0047have htriple : exists ftcn_left_fssq_triple ftcn_right_fssq_triple. (a * a + b * b + c * c) + (k) * ftcn_left_fssq_triple = (e * e + f * f + g * g) + (k) * ftcn_right_fssq_triple
  48. 0048specialize mod_eq_add k
  49. 0049specialize mod_eq_add (a * a + b * b)
  50. 0050specialize mod_eq_add (e * e + f * f)
  51. 0051specialize mod_eq_add (c * c)
  52. 0052specialize mod_eq_add (g * g)
  53. 0053apply mod_eq_add
  54. 0054exact hpair
  55. 0055exact hthird
  56. 0056specialize mod_eq_add k
  57. 0057specialize mod_eq_add (a * a + b * b + c * c)
  58. 0058specialize mod_eq_add (e * e + f * f + g * g)
  59. 0059specialize mod_eq_add (d * d)
  60. 0060specialize mod_eq_add (h * h)
  61. 0061apply mod_eq_add
  62. 0062exact htriple
  63. 0063exact hfourth