FS005D · theorem body

four_square_signed_centered_norm_quotient_exists

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

For every one of the sixteen centered sign patterns, a represented prime multiple yields an actual natural quotient of the centered four-square norm.

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

∀ p. ∀ k. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. p · k = a · a + b · b + c · c + d · d → 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)) → ∃ x. k · x = 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

In local proof propositions

PD0003 Dvd PD0008 ModEq
Exact expanded first-order statement
forall p k a b c d e f g h. p * k = (a * a + b * b + c * c + d * d) -> (((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 r. k * r = (e * e + f * f + g * g + h * h)

Proof neighborhood

Direct theorem prerequisites

FS005C four_square_signed_centered_norm_congruent multiple_implies_balanced_zero_congruence · Alpha closed mod_eq_symm · Stable closed mod_eq_trans · Stable closed balanced_zero_congruence_implies_multiple · Alpha closed mul_comm · Stable closed

Direct theorem dependents

FS000T four_square_branch_odd_represented_strict_step

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

62 script commands · 15 reading checkpoints · 5 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 norm congruent
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hnorm
  2. L12
    intro ha
  3. L13
    intro hb
  4. L14
    intro hc
  5. L15
    intro hd
03Establish hcongruentL16–25

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

  1. L16
    have hcongruent : ModEq(k,a · a + b · b + c · c + d · d,e · e + f · f + g · g + h · h)Definitions: ModEq(k,a · a + b · b + c · c + d · d,e · e + f · f + g · g + h · h)Original native command in the exact edition
  2. L17
    specialize four_square_signed_centered_norm_congruent k
  3. L18
    specialize four_square_signed_centered_norm_congruent a
  4. L19
    specialize four_square_signed_centered_norm_congruent b
  5. L20
    specialize four_square_signed_centered_norm_congruent c
  6. L21
    specialize four_square_signed_centered_norm_congruent d
  7. L22
    specialize four_square_signed_centered_norm_congruent e
  8. L23
    specialize four_square_signed_centered_norm_congruent f
  9. L24
    specialize four_square_signed_centered_norm_congruent g
  10. L25
    specialize four_square_signed_centered_norm_congruent h
04Use earlier factsL26–30

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

  1. L26
    apply four_square_signed_centered_norm_congruent
  2. L27
    exact ha
  3. L28
    exact hb
  4. L29
    exact hc
  5. L30
    exact hd
05Establish hleft_zeroL31–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple implies balanced zero congruence.

  1. L31
    have hleft_zero : ModEq(k,a · a + b · b + c · c + d · d,0)Definitions: ModEq(k,a · a + b · b + c · c + d · d,0)Original native command in the exact edition
  2. L32
    specialize multiple_implies_balanced_zero_congruence k
  3. L33
    specialize multiple_implies_balanced_zero_congruence (a * a + b * b + c * c + d * d)
  4. L34
    apply multiple_implies_balanced_zero_congruence
06Construct an explicit witnessL35–35

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists p
07Calculate and transport equalitiesL36–37

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

  1. L36
    trans p * k
  2. L37
    symm
08Use earlier factsL38–39

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

  1. L38
    exact hnorm
  2. L39
    apply mul_comm
09Establish hreverseL40–45

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

  1. L40
    have hreverse : ModEq(k,e · e + f · f + g · g + h · h,a · a + b · b + c · c + d · d)Definitions: ModEq(k,e · e + f · f + g · g + h · h,a · a + b · b + c · c + d · d)Original native command in the exact edition
  2. L41
    specialize mod_eq_symm k
  3. L42
    specialize mod_eq_symm (a * a + b * b + c * c + d * d)
  4. L43
    specialize mod_eq_symm (e * e + f * f + g * g + h * h)
  5. L44
    apply mod_eq_symm
  6. L45
    exact hcongruent
10Establish hzeroL46–53

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

  1. L46
    have hzero : ModEq(k,e · e + f · f + g · g + h · h,0)Definitions: ModEq(k,e · e + f · f + g · g + h · h,0)Original native command in the exact edition
  2. L47
    specialize mod_eq_trans k
  3. L48
    specialize mod_eq_trans (e * e + f * f + g * g + h * h)
  4. L49
    specialize mod_eq_trans (a * a + b * b + c * c + d * d)
  5. L50
    specialize mod_eq_trans 0
  6. L51
    apply mod_eq_trans
  7. L52
    exact hreverse
  8. L53
    exact hleft_zero
11Establish hmultipleL54–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply balanced zero congruence implies multiple.

  1. L54
    have hmultiple : Dvd(k,e · e + f · f + g · g + h · h)Definitions: Dvd(k,e · e + f · f + g · g + h · h)Original native command in the exact edition
  2. L55
    specialize balanced_zero_congruence_implies_multiple k
  3. L56
    specialize balanced_zero_congruence_implies_multiple (e * e + f * f + g * g + h * h)
  4. L57
    apply balanced_zero_congruence_implies_multiple
  5. L58
    exact hzero
12Separate the logical casesL59–59

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L59
    cases hmultiple
13Construct an explicit witnessL60–60

Supply the displayed value, then prove that it has the required property.

  1. L60
    exists x
14Calculate and transport equalitiesL61–61

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

  1. L61
    symm
15Use earlier factsL62–62

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

  1. L62
    exact hmultiple_witness

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro e
  8. 0008intro f
  9. 0009intro g
  10. 0010intro h
  11. 0011intro hnorm
  12. 0012intro ha
  13. 0013intro hb
  14. 0014intro hc
  15. 0015intro hd
  16. 0016have hcongruent : ModEq(k,a · a + b · b + c · c + d · d,e · e + f · f + g · g + h · h)
    Exact native replay linehave hcongruent : exists ftcn_left_fssq_quotient_congruence ftcn_right_fssq_quotient_congruence. (a * a + b * b + c * c + d * d) + (k) * ftcn_left_fssq_quotient_congruence = (e * e + f * f + g * g + h * h) + (k) * ftcn_right_fssq_quotient_congruence
  17. 0017specialize four_square_signed_centered_norm_congruent k
  18. 0018specialize four_square_signed_centered_norm_congruent a
  19. 0019specialize four_square_signed_centered_norm_congruent b
  20. 0020specialize four_square_signed_centered_norm_congruent c
  21. 0021specialize four_square_signed_centered_norm_congruent d
  22. 0022specialize four_square_signed_centered_norm_congruent e
  23. 0023specialize four_square_signed_centered_norm_congruent f
  24. 0024specialize four_square_signed_centered_norm_congruent g
  25. 0025specialize four_square_signed_centered_norm_congruent h
  26. 0026apply four_square_signed_centered_norm_congruent
  27. 0027exact ha
  28. 0028exact hb
  29. 0029exact hc
  30. 0030exact hd
  31. 0031have hleft_zero : ModEq(k,a · a + b · b + c · c + d · d,0)
    Exact native replay linehave hleft_zero : exists ftcn_left_fssq_quotient_left_zero ftcn_right_fssq_quotient_left_zero. (a * a + b * b + c * c + d * d) + (k) * ftcn_left_fssq_quotient_left_zero = (0) + (k) * ftcn_right_fssq_quotient_left_zero
  32. 0032specialize multiple_implies_balanced_zero_congruence k
  33. 0033specialize multiple_implies_balanced_zero_congruence (a * a + b * b + c * c + d * d)
  34. 0034apply multiple_implies_balanced_zero_congruence
  35. 0035exists p
  36. 0036trans p * k
  37. 0037symm
  38. 0038exact hnorm
  39. 0039apply mul_comm
  40. 0040have hreverse : ModEq(k,e · e + f · f + g · g + h · h,a · a + b · b + c · c + d · d)
    Exact native replay linehave hreverse : exists ftcn_left_fssq_quotient_reverse ftcn_right_fssq_quotient_reverse. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssq_quotient_reverse = (a * a + b * b + c * c + d * d) + (k) * ftcn_right_fssq_quotient_reverse
  41. 0041specialize mod_eq_symm k
  42. 0042specialize mod_eq_symm (a * a + b * b + c * c + d * d)
  43. 0043specialize mod_eq_symm (e * e + f * f + g * g + h * h)
  44. 0044apply mod_eq_symm
  45. 0045exact hcongruent
  46. 0046have hzero : ModEq(k,e · e + f · f + g · g + h · h,0)
    Exact native replay linehave hzero : exists ftcn_left_fssq_quotient_zero ftcn_right_fssq_quotient_zero. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssq_quotient_zero = (0) + (k) * ftcn_right_fssq_quotient_zero
  47. 0047specialize mod_eq_trans k
  48. 0048specialize mod_eq_trans (e * e + f * f + g * g + h * h)
  49. 0049specialize mod_eq_trans (a * a + b * b + c * c + d * d)
  50. 0050specialize mod_eq_trans 0
  51. 0051apply mod_eq_trans
  52. 0052exact hreverse
  53. 0053exact hleft_zero
  54. 0054have hmultiple : Dvd(k,e · e + f · f + g · g + h · h)
    Exact native replay linehave hmultiple : exists ftcn_factor_fssq_quotient_multiple. (e * e + f * f + g * g + h * h) = (k) * ftcn_factor_fssq_quotient_multiple
  55. 0055specialize balanced_zero_congruence_implies_multiple k
  56. 0056specialize balanced_zero_congruence_implies_multiple (e * e + f * f + g * g + h * h)
  57. 0057apply balanced_zero_congruence_implies_multiple
  58. 0058exact hzero
  59. 0059cases hmultiple
  60. 0060exists x
  61. 0061symm
  62. 0062exact hmultiple_witness