FS003I · theorem body

four_square_lagrange_bounded_from_primes

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

Bounded constructive prime-factor descent proves every nonzero natural is a sum of four squares once every prime has such a representation.

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

∀ B. ∀ n. Le(n,B) → ¬n = 0 → (∀ x. Prime(x) → ∃ y. ∃ z. ∃ m. ∃ k. x = y · y + z · z + m · m + k · k) → ∃ x. ∃ y. ∃ z. ∃ m. n = x · x + y · y + z · z + 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 PD0004 Prime

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime
Exact expanded first-order statement
forall B n. (exists fsl_bound. fsl_bound + n = B) -> ~(n = 0) -> (forall fsl_prime_universal. ((~(fsl_prime_universal = 1) /\ forall frm_prime_left_fsl_all_universal frm_prime_right_fsl_all_universal. fsl_prime_universal = frm_prime_left_fsl_all_universal * frm_prime_right_fsl_all_universal -> frm_prime_left_fsl_all_universal = 1 \/ frm_prime_right_fsl_all_universal = 1)) -> (exists fsl_a_all_universal fsl_b_all_universal fsl_c_all_universal fsl_d_all_universal. (fsl_prime_universal) = fsl_a_all_universal * fsl_a_all_universal + fsl_b_all_universal * fsl_b_all_universal + fsl_c_all_universal * fsl_c_all_universal + fsl_d_all_universal * fsl_d_all_universal)) -> (exists fsl_a_value fsl_b_value fsl_c_value fsl_d_value. (n) = fsl_a_value * fsl_a_value + fsl_b_value * fsl_b_value + fsl_c_value * fsl_c_value + fsl_d_value * fsl_d_value)

Proof neighborhood

Direct theorem prerequisites

le_zero · Stable closed eq_decidable · Stable closed prime_divisor_exists · Stable closed mul_comm · Stable closed proper_factor_lt · Stable closed le_trans · Stable closed le_of_succ_le_succ · Stable closed FS0030 four_square_euler_representations_closed_under_multiplication

Direct theorem dependents

FS003J four_square_lagrange_from_all_primes

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

82 script commands · 22 reading checkpoints · 9 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 euler representations closed under multiplication
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro n
  3. L4
    intro hbound
  4. L5
    intro hnonzero
  5. L6
    intro hprimes
03Separate the logical casesL7–7

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

  1. L7
    exfalso
04Use earlier factsL8–11

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

  1. L8
    apply hnonzero
  2. L9
    specialize le_zero n
  3. L10
    apply le_zero
  4. L11
    exact hbound
05Fix variables and assumptionsL12–15

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

  1. L12
    intro n
  2. L13
    intro hbound
  3. L14
    intro hnonzero
  4. L15
    intro hprimes
06Use earlier factsL16–17

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

  1. L16
    specialize eq_decidable n
  2. L17
    specialize eq_decidable 1
07Separate the logical casesL18–18

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

  1. L18
    cases eq_decidable
08Construct an explicit witnessL19–22

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

  1. L19
    exists 1
  2. L20
    exists 0
  3. L21
    exists 0
  4. L22
    exists 0
09Calculate and transport equalitiesL23–24

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

  1. L23
    rewrite eq_decidable_left
  2. L24
    norm_num
10Establish hfactorL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor exists.

  1. L25
    have hfactor : ∃ p. Prime(p) ∧ Dvd(p,n)Definitions: Prime(p)Dvd(p,n)Original native command in the exact edition
  2. L26
    specialize prime_divisor_exists n
  3. L27
    apply prime_divisor_exists
  4. L28
    exact hnonzero
  5. L29
    exact eq_decidable_right
11Separate the logical casesL30–32

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

  1. L30
    cases hfactor
  2. L31
    cases hfactor_witness
  3. L32
    cases hfactor_witness_right
12Establish hprefix_nonzeroL33–39

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

  1. L33
    have hprefix_nonzero : ~(x1 = 0)
  2. L34
    intro hzero
  3. L35
    apply hnonzero
  4. L36
    trans x * x1
  5. L37
    exact hfactor_witness_right_witness
  6. L38
    rewrite hzero
  7. L39
    apply PA5
13Establish hrepresented_primeL40–43

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

  1. L40
    have hrepresented_prime : (exists fsl_a_induction_prime fsl_b_induction_prime fsl_c_induction_prime fsl_d_induction_prime. (x) = fsl_a_induction_prime * fsl_a_induction_prime + fsl_b_induction_prime * fsl_b_induction_prime + fsl_c_induction_prime * fsl_c_induction_prime + fsl_d_induction_prime * fsl_d_induction_prime)
  2. L41
    specialize hprimes x
  3. L42
    apply hprimes
  4. L43
    exact hfactor_witness_left
14Establish horderedL44–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L44
    have hordered : n = x1 * x
  2. L45
    trans x * x1
  3. L46
    exact hfactor_witness_right_witness
  4. L47
    apply mul_comm
15Establish hnotoneL48–48

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

  1. L48
    have hnotone : ~(x = 1)
16Separate the logical casesL49–49

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

  1. L49
    cases hfactor_witness_left
17Use earlier factsL50–50

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

  1. L50
    exact hfactor_witness_left_left
18Establish hstrictL51–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply proper factor lt.

  1. L51
    have hstrict : Lt(x1,n)Definitions: Lt(x1,n)Original native command in the exact edition
  2. L52
    specialize proper_factor_lt n
  3. L53
    specialize proper_factor_lt x1
  4. L54
    specialize proper_factor_lt x
  5. L55
    apply proper_factor_lt
  6. L56
    exact hnonzero
  7. L57
    exact hordered
  8. L58
    exact hnotone
19Establish hsuccessor_boundL59–65

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

  1. L59
    have hsuccessor_bound : Lt(x1,S B)Definitions: Lt(x1,S B)Original native command in the exact edition
  2. L60
    specialize le_trans (S x1)
  3. L61
    specialize le_trans n
  4. L62
    specialize le_trans (S B)
  5. L63
    apply le_trans
  6. L64
    exact hstrict
  7. L65
    exact hbound
20Establish hprefix_boundL66–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L66
    have hprefix_bound : Le(x1,B)Definitions: Le(x1,B)Original native command in the exact edition
  2. L67
    specialize le_of_succ_le_succ x1
  3. L68
    specialize le_of_succ_le_succ B
  4. L69
    apply le_of_succ_le_succ
  5. L70
    exact hsuccessor_bound
21Establish hprefix_representationL71–80

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

  1. L71
    have hprefix_representation : (exists fsl_a_induction_prefix fsl_b_induction_prefix fsl_c_induction_prefix fsl_d_induction_prefix. (x1) = fsl_a_induction_prefix * fsl_a_induction_prefix + fsl_b_induction_prefix * fsl_b_induction_prefix + fsl_c_induction_prefix * fsl_c_induction_prefix + fsl_d_induction_prefix * fsl_d_induction_prefix)
  2. L72
    specialize IH x1
  3. L73
    apply IH
  4. L74
    exact hprefix_bound
  5. L75
    exact hprefix_nonzero
  6. L76
    exact hprimes
  7. L77
    rewrite hordered
  8. L78
    specialize four_square_euler_representations_closed_under_multiplication x1
  9. L79
    specialize four_square_euler_representations_closed_under_multiplication x
  10. L80
    apply four_square_euler_representations_closed_under_multiplication
22Use earlier factsL81–82

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

  1. L81
    exact hprefix_representation
  2. L82
    exact hrepresented_prime

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hbound
  5. 0005intro hnonzero
  6. 0006intro hprimes
  7. 0007exfalso
  8. 0008apply hnonzero
  9. 0009specialize le_zero n
  10. 0010apply le_zero
  11. 0011exact hbound
  12. 0012intro n
  13. 0013intro hbound
  14. 0014intro hnonzero
  15. 0015intro hprimes
  16. 0016specialize eq_decidable n
  17. 0017specialize eq_decidable 1
  18. 0018cases eq_decidable
  19. 0019exists 1
  20. 0020exists 0
  21. 0021exists 0
  22. 0022exists 0
  23. 0023rewrite eq_decidable_left
  24. 0024norm_num
  25. 0025have hfactor : ∃ p. Prime(p) ∧ Dvd(p,n)
    Exact native replay linehave hfactor : exists p. (((~(p = 1) /\ forall frm_prime_left_fsl_induction_factor frm_prime_right_fsl_induction_factor. p = frm_prime_left_fsl_induction_factor * frm_prime_right_fsl_induction_factor -> frm_prime_left_fsl_induction_factor = 1 \/ frm_prime_right_fsl_induction_factor = 1)) /\ exists r. n = p * r)
  26. 0026specialize prime_divisor_exists n
  27. 0027apply prime_divisor_exists
  28. 0028exact hnonzero
  29. 0029exact eq_decidable_right
  30. 0030cases hfactor
  31. 0031cases hfactor_witness
  32. 0032cases hfactor_witness_right
  33. 0033have hprefix_nonzero : ~(x1 = 0)
  34. 0034intro hzero
  35. 0035apply hnonzero
  36. 0036trans x * x1
  37. 0037exact hfactor_witness_right_witness
  38. 0038rewrite hzero
  39. 0039apply PA5
  40. 0040have hrepresented_prime : (exists fsl_a_induction_prime fsl_b_induction_prime fsl_c_induction_prime fsl_d_induction_prime. (x) = fsl_a_induction_prime * fsl_a_induction_prime + fsl_b_induction_prime * fsl_b_induction_prime + fsl_c_induction_prime * fsl_c_induction_prime + fsl_d_induction_prime * fsl_d_induction_prime)
  41. 0041specialize hprimes x
  42. 0042apply hprimes
  43. 0043exact hfactor_witness_left
  44. 0044have hordered : n = x1 * x
  45. 0045trans x * x1
  46. 0046exact hfactor_witness_right_witness
  47. 0047apply mul_comm
  48. 0048have hnotone : ~(x = 1)
  49. 0049cases hfactor_witness_left
  50. 0050exact hfactor_witness_left_left
  51. 0051have hstrict : Lt(x1,n)
    Exact native replay linehave hstrict : exists k. k + S x1 = n
  52. 0052specialize proper_factor_lt n
  53. 0053specialize proper_factor_lt x1
  54. 0054specialize proper_factor_lt x
  55. 0055apply proper_factor_lt
  56. 0056exact hnonzero
  57. 0057exact hordered
  58. 0058exact hnotone
  59. 0059have hsuccessor_bound : Lt(x1,S B)
    Exact native replay linehave hsuccessor_bound : exists k. k + S x1 = S B
  60. 0060specialize le_trans (S x1)
  61. 0061specialize le_trans n
  62. 0062specialize le_trans (S B)
  63. 0063apply le_trans
  64. 0064exact hstrict
  65. 0065exact hbound
  66. 0066have hprefix_bound : Le(x1,B)
    Exact native replay linehave hprefix_bound : exists k. k + x1 = B
  67. 0067specialize le_of_succ_le_succ x1
  68. 0068specialize le_of_succ_le_succ B
  69. 0069apply le_of_succ_le_succ
  70. 0070exact hsuccessor_bound
  71. 0071have hprefix_representation : (exists fsl_a_induction_prefix fsl_b_induction_prefix fsl_c_induction_prefix fsl_d_induction_prefix. (x1) = fsl_a_induction_prefix * fsl_a_induction_prefix + fsl_b_induction_prefix * fsl_b_induction_prefix + fsl_c_induction_prefix * fsl_c_induction_prefix + fsl_d_induction_prefix * fsl_d_induction_prefix)
  72. 0072specialize IH x1
  73. 0073apply IH
  74. 0074exact hprefix_bound
  75. 0075exact hprefix_nonzero
  76. 0076exact hprimes
  77. 0077rewrite hordered
  78. 0078specialize four_square_euler_representations_closed_under_multiplication x1
  79. 0079specialize four_square_euler_representations_closed_under_multiplication x
  80. 0080apply four_square_euler_representations_closed_under_multiplication
  81. 0081exact hprefix_representation
  82. 0082exact hrepresented_prime