FS005C · theorem body

four_square_signed_centered_norm_congruent

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ k. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. Le(e + e,k) ∧ ((∃ x. a = k · x + e) ∨ Dvd(k,a + e)) → Le(f + f,k) ∧ ((∃ x. b = k · x + f) ∨ Dvd(k,b + f)) → Le(g + g,k) ∧ ((∃ x. c = k · x + g) ∨ Dvd(k,c + g)) → Le(h + h,k) ∧ ((∃ x. d = k · x + h) ∨ Dvd(k,d + h)) → ModEq(k,a · a + b · b + c · c + d · d,e · e + f · f + g · g + h · h)

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

PD0001 Le PD0003 Dvd PD0008 ModEq

In local proof propositions

PD0008 ModEq
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

FS005B four_square_signed_centered_square_congruent mod_eq_add · Stable closed

Direct theorem dependents

FS005D four_square_signed_centered_norm_quotient_exists

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

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.

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 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 : ModEq(k,a · a,e · e)Definitions: ModEq(k,a · a,e · e)Original native command in the exact edition
  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 : ModEq(k,b · b,f · f)Definitions: ModEq(k,b · b,f · f)Original native command in the exact edition
  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 : ModEq(k,c · c,g · g)Definitions: ModEq(k,c · c,g · g)Original native command in the exact edition
  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 : ModEq(k,d · d,h · h)Definitions: ModEq(k,d · d,h · h)Original native command in the exact edition
  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 : ModEq(k,a · a + b · b,e · e + f · f)Definitions: ModEq(k,a · a + b · b,e · e + f · f)Original native command in the exact edition
  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 : ModEq(k,a · a + b · b + c · c,e · e + f · f + g · g)Definitions: ModEq(k,a · a + b · b + c · c,e · e + f · f + g · g)Original native command in the exact edition
  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 defined 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 : ModEq(k,a · a,e · e)
    Exact native replay linehave 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 : ModEq(k,b · b,f · f)
    Exact native replay linehave 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 : ModEq(k,c · c,g · g)
    Exact native replay linehave 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 : ModEq(k,d · d,h · h)
    Exact native replay linehave 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 : ModEq(k,a · a + b · b,e · e + f · f)
    Exact native replay linehave 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 : ModEq(k,a · a + b · b + c · c,e · e + f · f + g · g)
    Exact native replay linehave 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