FS0024 · theorem body

four_square_descent_odd_centered_strict_step

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

For every proper nonunit odd prime multiplier, any represented signed centered quotient automatically gives a nonzero strictly smaller represented multiplier.

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. ∀ h. ∀ r. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ j. Prime(p) → ¬k = 0 → ¬k = 1 → Lt(k,p) → k = 2 · h + 1 → 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(j + j,k) ∧ ((∃ x. d = k · x + j) ∨ Dvd(k,d + j)) → k · r = e · e + f · f + g · g + j · j → (∃ x. ∃ y. ∃ z. ∃ n. p · r = x · x + y · y + z · z + n · n) → ∃ x. ¬x = 0 ∧ (Lt(x,k) ∧ (∃ y. ∃ z. ∃ n. ∃ m. p · x = y · y + z · z + n · n + m · m))

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 PD0002 Lt PD0003 Dvd PD0004 Prime

In local proof propositions

PD0002 Lt
Exact expanded first-order statement
forall p k h r a b c d e f g j. ((~(p = 1) /\ forall frm_prime_left_fsd_p frm_prime_right_fsd_p. p = frm_prime_left_fsd_p * frm_prime_right_fsd_p -> frm_prime_left_fsd_p = 1 \/ frm_prime_right_fsd_p = 1)) -> ~(k = 0) -> ~(k = 1) -> (exists gap. gap + S k = p) -> k = 2 * h + 1 -> p * k = a * a + b * b + c * c + d * d -> (((exists fsd_center_bound_odd_step_a. fsd_center_bound_odd_step_a + (e + e) = k) /\ ((exists fsd_center_lower_odd_step_a. a = k * fsd_center_lower_odd_step_a + e) \/ (exists fsd_center_upper_odd_step_a. a + e = k * fsd_center_upper_odd_step_a)))) -> (((exists fsd_center_bound_odd_step_b. fsd_center_bound_odd_step_b + (f + f) = k) /\ ((exists fsd_center_lower_odd_step_b. b = k * fsd_center_lower_odd_step_b + f) \/ (exists fsd_center_upper_odd_step_b. b + f = k * fsd_center_upper_odd_step_b)))) -> (((exists fsd_center_bound_odd_step_c. fsd_center_bound_odd_step_c + (g + g) = k) /\ ((exists fsd_center_lower_odd_step_c. c = k * fsd_center_lower_odd_step_c + g) \/ (exists fsd_center_upper_odd_step_c. c + g = k * fsd_center_upper_odd_step_c)))) -> (((exists fsd_center_bound_odd_step_d. fsd_center_bound_odd_step_d + (j + j) = k) /\ ((exists fsd_center_lower_odd_step_d. d = k * fsd_center_lower_odd_step_d + j) \/ (exists fsd_center_upper_odd_step_d. d + j = k * fsd_center_upper_odd_step_d)))) -> k * r = e * e + f * f + g * g + j * j -> (exists fsl_a_odd_step_representation fsl_b_odd_step_representation fsl_c_odd_step_representation fsl_d_odd_step_representation. (p * r) = fsl_a_odd_step_representation * fsl_a_odd_step_representation + fsl_b_odd_step_representation * fsl_b_odd_step_representation + fsl_c_odd_step_representation * fsl_c_odd_step_representation + fsl_d_odd_step_representation * fsl_d_odd_step_representation) -> exists s. (~(s = 0) /\ ((exists gap. gap + S s = k) /\ (exists fsl_a_odd_step_smaller fsl_b_odd_step_smaller fsl_c_odd_step_smaller fsl_d_odd_step_smaller. (p * s) = fsl_a_odd_step_smaller * fsl_a_odd_step_smaller + fsl_b_odd_step_smaller * fsl_b_odd_step_smaller + fsl_c_odd_step_smaller * fsl_c_odd_step_smaller + fsl_d_odd_step_smaller * fsl_d_odd_step_smaller)))

Proof neighborhood

Direct theorem prerequisites

FS0023 four_square_descent_bounded_centered_quotient_nonzero FS001Y four_square_descent_odd_centered_norm_strict FS001O four_square_descent_norm_bound_forces_smaller_multiplier

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

77 script commands · 13 reading checkpoints · 2 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 (3)
four square descent bounded centered quotient nonzerofour square descent odd centered norm strictfour square descent norm bound forces smaller multiplier
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 h
  4. L4
    intro r
  5. L5
    intro a
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro d
  9. L9
    intro e
  10. L10
    intro f
02Fix variables and assumptionsL11–20

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

  1. L11
    intro g
  2. L12
    intro j
  3. L13
    intro hprime
  4. L14
    intro hk
  5. L15
    intro hnonunit
  6. L16
    intro hproper
  7. L17
    intro hodd
  8. L18
    intro hnorm
  9. L19
    intro ha
  10. L20
    intro hb
03Fix variables and assumptionsL21–24

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

  1. L21
    intro hc
  2. L22
    intro hd
  3. L23
    intro hcenter_norm
  4. L24
    intro hrepresented
04Establish hnonzeroL25–34

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

  1. L25
    have hnonzero : ~(r = 0)
  2. L26
    intro hrzero
  3. L27
    specialize four_square_descent_bounded_centered_quotient_nonzero p
  4. L28
    specialize four_square_descent_bounded_centered_quotient_nonzero k
  5. L29
    specialize four_square_descent_bounded_centered_quotient_nonzero r
  6. L30
    specialize four_square_descent_bounded_centered_quotient_nonzero a
  7. L31
    specialize four_square_descent_bounded_centered_quotient_nonzero b
  8. L32
    specialize four_square_descent_bounded_centered_quotient_nonzero c
  9. L33
    specialize four_square_descent_bounded_centered_quotient_nonzero d
  10. L34
    specialize four_square_descent_bounded_centered_quotient_nonzero e
05Use earlier factsL35–44

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

  1. L35
    specialize four_square_descent_bounded_centered_quotient_nonzero f
  2. L36
    specialize four_square_descent_bounded_centered_quotient_nonzero g
  3. L37
    specialize four_square_descent_bounded_centered_quotient_nonzero j
  4. L38
    apply four_square_descent_bounded_centered_quotient_nonzero
  5. L39
    exact hprime
  6. L40
    exact hk
  7. L41
    exact hnonunit
  8. L42
    exact hproper
  9. L43
    exact hnorm
  10. L44
    exact ha
06Use earlier factsL45–49

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

  1. L45
    exact hb
  2. L46
    exact hc
  3. L47
    exact hd
  4. L48
    exact hcenter_norm
  5. L49
    exact hrzero
07Establish hnormboundL50–59

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

  1. L50
    have hnormbound : Lt(e · e + f · f + g · g + j · j,k · k)Definitions: Lt(e · e + f · f + g · g + j · j,k · k)Original native command in the exact edition
  2. L51
    specialize four_square_descent_odd_centered_norm_strict k
  3. L52
    specialize four_square_descent_odd_centered_norm_strict h
  4. L53
    specialize four_square_descent_odd_centered_norm_strict a
  5. L54
    specialize four_square_descent_odd_centered_norm_strict b
  6. L55
    specialize four_square_descent_odd_centered_norm_strict c
  7. L56
    specialize four_square_descent_odd_centered_norm_strict d
  8. L57
    specialize four_square_descent_odd_centered_norm_strict e
  9. L58
    specialize four_square_descent_odd_centered_norm_strict f
  10. L59
    specialize four_square_descent_odd_centered_norm_strict g
08Use earlier factsL60–66

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

  1. L60
    specialize four_square_descent_odd_centered_norm_strict j
  2. L61
    apply four_square_descent_odd_centered_norm_strict
  3. L62
    exact hodd
  4. L63
    exact ha
  5. L64
    exact hb
  6. L65
    exact hc
  7. L66
    exact hd
09Construct an explicit witnessL67–67

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

  1. L67
    exists r
10Separate the logical casesL68–68

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

  1. L68
    split
11Use earlier factsL69–69

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

  1. L69
    exact hnonzero
12Separate the logical casesL70–70

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

  1. L70
    split
13Use earlier factsL71–77

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

  1. L71
    specialize four_square_descent_norm_bound_forces_smaller_multiplier k
  2. L72
    specialize four_square_descent_norm_bound_forces_smaller_multiplier r
  3. L73
    specialize four_square_descent_norm_bound_forces_smaller_multiplier (e * e + f * f + g * g + j * j)
  4. L74
    apply four_square_descent_norm_bound_forces_smaller_multiplier
  5. L75
    exact hcenter_norm
  6. L76
    exact hnormbound
  7. L77
    exact hrepresented

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro h
  4. 0004intro r
  5. 0005intro a
  6. 0006intro b
  7. 0007intro c
  8. 0008intro d
  9. 0009intro e
  10. 0010intro f
  11. 0011intro g
  12. 0012intro j
  13. 0013intro hprime
  14. 0014intro hk
  15. 0015intro hnonunit
  16. 0016intro hproper
  17. 0017intro hodd
  18. 0018intro hnorm
  19. 0019intro ha
  20. 0020intro hb
  21. 0021intro hc
  22. 0022intro hd
  23. 0023intro hcenter_norm
  24. 0024intro hrepresented
  25. 0025have hnonzero : ~(r = 0)
  26. 0026intro hrzero
  27. 0027specialize four_square_descent_bounded_centered_quotient_nonzero p
  28. 0028specialize four_square_descent_bounded_centered_quotient_nonzero k
  29. 0029specialize four_square_descent_bounded_centered_quotient_nonzero r
  30. 0030specialize four_square_descent_bounded_centered_quotient_nonzero a
  31. 0031specialize four_square_descent_bounded_centered_quotient_nonzero b
  32. 0032specialize four_square_descent_bounded_centered_quotient_nonzero c
  33. 0033specialize four_square_descent_bounded_centered_quotient_nonzero d
  34. 0034specialize four_square_descent_bounded_centered_quotient_nonzero e
  35. 0035specialize four_square_descent_bounded_centered_quotient_nonzero f
  36. 0036specialize four_square_descent_bounded_centered_quotient_nonzero g
  37. 0037specialize four_square_descent_bounded_centered_quotient_nonzero j
  38. 0038apply four_square_descent_bounded_centered_quotient_nonzero
  39. 0039exact hprime
  40. 0040exact hk
  41. 0041exact hnonunit
  42. 0042exact hproper
  43. 0043exact hnorm
  44. 0044exact ha
  45. 0045exact hb
  46. 0046exact hc
  47. 0047exact hd
  48. 0048exact hcenter_norm
  49. 0049exact hrzero
  50. 0050have hnormbound : Lt(e · e + f · f + g · g + j · j,k · k)
    Exact native replay linehave hnormbound : exists gap. gap + S (e * e + f * f + g * g + j * j) = k * k
  51. 0051specialize four_square_descent_odd_centered_norm_strict k
  52. 0052specialize four_square_descent_odd_centered_norm_strict h
  53. 0053specialize four_square_descent_odd_centered_norm_strict a
  54. 0054specialize four_square_descent_odd_centered_norm_strict b
  55. 0055specialize four_square_descent_odd_centered_norm_strict c
  56. 0056specialize four_square_descent_odd_centered_norm_strict d
  57. 0057specialize four_square_descent_odd_centered_norm_strict e
  58. 0058specialize four_square_descent_odd_centered_norm_strict f
  59. 0059specialize four_square_descent_odd_centered_norm_strict g
  60. 0060specialize four_square_descent_odd_centered_norm_strict j
  61. 0061apply four_square_descent_odd_centered_norm_strict
  62. 0062exact hodd
  63. 0063exact ha
  64. 0064exact hb
  65. 0065exact hc
  66. 0066exact hd
  67. 0067exists r
  68. 0068split
  69. 0069exact hnonzero
  70. 0070split
  71. 0071specialize four_square_descent_norm_bound_forces_smaller_multiplier k
  72. 0072specialize four_square_descent_norm_bound_forces_smaller_multiplier r
  73. 0073specialize four_square_descent_norm_bound_forces_smaller_multiplier (e * e + f * f + g * g + j * j)
  74. 0074apply four_square_descent_norm_bound_forces_smaller_multiplier
  75. 0075exact hcenter_norm
  76. 0076exact hnormbound
  77. 0077exact hrepresented