FS001X

four_square_descent_odd_half_norm_strict

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

Four coordinates in the odd half interval have norm strictly below the square of the full odd modulus.

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 h a b c d. (exists gap. gap + a = h) -> (exists gap. gap + b = h) -> (exists gap. gap + c = h) -> (exists gap. gap + d = h) -> exists gap. gap + S (a * a + b * b + c * c + d * d) = (2 * h + 1) * (2 * h + 1)

Constructive proof overview

Generated structural guide

Four coordinates in the odd half interval have norm strictly below the square of the full odd modulus.

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

mul_le_mul Alpha theorem; checked-use authorized FS001V four_square_descent_add_le_add add_assoc Stable theorem; checked-use authorized FS001W four_square_descent_double_square_four_sum lt_of_le_of_lt Stable theorem; checked-use authorized square_lt_successor_square Alpha theorem; checked-use authorized

Direct dependents

FS000M four_square_odd_prime_half_seed_norm_strict FS001Y four_square_descent_odd_centered_norm_strict

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

58 script commands · 18 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.

Named ingredients (2)
four square descent add le addfour square descent double square four sum
01Fix variables and assumptionsL1–9

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

  1. L1
    intro h
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro ha
  7. L7
    intro hb
  8. L8
    intro hc
  9. L9
    intro hd
02Establish hsaL10–13

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

  1. L10
    have hsa : exists gap. gap + a * a = h * h
  2. L11
    apply mul_le_mul
  3. L12
    exact ha
  4. L13
    exact ha
03Establish hsbL14–17

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

  1. L14
    have hsb : exists gap. gap + b * b = h * h
  2. L15
    apply mul_le_mul
  3. L16
    exact hb
  4. L17
    exact hb
04Establish hscL18–21

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

  1. L18
    have hsc : exists gap. gap + c * c = h * h
  2. L19
    apply mul_le_mul
  3. L20
    exact hc
  4. L21
    exact hc
05Establish hsdL22–25

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

  1. L22
    have hsd : exists gap. gap + d * d = h * h
  2. L23
    apply mul_le_mul
  3. L24
    exact hd
  4. L25
    exact hd
06Establish habL26–29

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

  1. L26
    have hab : exists gap. gap + (a * a + b * b) = h * h + h * h
  2. L27
    apply four_square_descent_add_le_add
  3. L28
    exact hsa
  4. L29
    exact hsb
07Establish hcdL30–33

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

  1. L30
    have hcd : exists gap. gap + (c * c + d * d) = h * h + h * h
  2. L31
    apply four_square_descent_add_le_add
  3. L32
    exact hsc
  4. L33
    exact hsd
08Establish hpairedL34–37

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

  1. L34
    have hpaired : exists gap. gap + ((a * a + b * b) + (c * c + d * d)) = (h * h + h * h) + (h * h + h * h)
  2. L35
    apply four_square_descent_add_le_add
  3. L36
    exact hab
  4. L37
    exact hcd
09Establish hnormL38–38

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

  1. L38
    have hnorm : exists gap. gap + (a * a + b * b + c * c + d * d) = (2 * h) * (2 * h)
10Separate the logical casesL39–39

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

  1. L39
    cases hpaired
11Construct an explicit witnessL40–40

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

  1. L40
    exists x
12Calculate and transport equalitiesL41–43

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

  1. L41
    trans x + ((a * a + b * b) + (c * c + d * d))
  2. L42
    congr
  3. L43
    refl
13Use earlier factsL44–44

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

  1. L44
    apply add_assoc
14Calculate and transport equalitiesL45–45

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

  1. L45
    trans (h * h + h * h) + (h * h + h * h)
15Use earlier factsL46–46

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

  1. L46
    exact hpaired_witness
16Calculate and transport equalitiesL47–47

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

  1. L47
    symm
17Use earlier factsL48–48

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

  1. L48
    apply four_square_descent_double_square_four_sum
18Establish honeL49–58

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

  1. L49
    have hone : 2 * h + 1 = S (2 * h)
  2. L50
    simp
  3. L51
    rewrite hone
  4. L52
    rewrite hone
  5. L53
    specialize lt_of_le_of_lt (a * a + b * b + c * c + d * d)
  6. L54
    specialize lt_of_le_of_lt ((2 * h) * (2 * h))
  7. L55
    specialize lt_of_le_of_lt (S (2 * h) * S (2 * h))
  8. L56
    apply lt_of_le_of_lt
  9. L57
    exact hnorm
  10. L58
    apply square_lt_successor_square

Library-wide reading audit

Original exact command ledger · 58 lines
  1. 0001intro h
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro ha
  7. 0007intro hb
  8. 0008intro hc
  9. 0009intro hd
  10. 0010have hsa : exists gap. gap + a * a = h * h
  11. 0011apply mul_le_mul
  12. 0012exact ha
  13. 0013exact ha
  14. 0014have hsb : exists gap. gap + b * b = h * h
  15. 0015apply mul_le_mul
  16. 0016exact hb
  17. 0017exact hb
  18. 0018have hsc : exists gap. gap + c * c = h * h
  19. 0019apply mul_le_mul
  20. 0020exact hc
  21. 0021exact hc
  22. 0022have hsd : exists gap. gap + d * d = h * h
  23. 0023apply mul_le_mul
  24. 0024exact hd
  25. 0025exact hd
  26. 0026have hab : exists gap. gap + (a * a + b * b) = h * h + h * h
  27. 0027apply four_square_descent_add_le_add
  28. 0028exact hsa
  29. 0029exact hsb
  30. 0030have hcd : exists gap. gap + (c * c + d * d) = h * h + h * h
  31. 0031apply four_square_descent_add_le_add
  32. 0032exact hsc
  33. 0033exact hsd
  34. 0034have hpaired : exists gap. gap + ((a * a + b * b) + (c * c + d * d)) = (h * h + h * h) + (h * h + h * h)
  35. 0035apply four_square_descent_add_le_add
  36. 0036exact hab
  37. 0037exact hcd
  38. 0038have hnorm : exists gap. gap + (a * a + b * b + c * c + d * d) = (2 * h) * (2 * h)
  39. 0039cases hpaired
  40. 0040exists x
  41. 0041trans x + ((a * a + b * b) + (c * c + d * d))
  42. 0042congr
  43. 0043refl
  44. 0044apply add_assoc
  45. 0045trans (h * h + h * h) + (h * h + h * h)
  46. 0046exact hpaired_witness
  47. 0047symm
  48. 0048apply four_square_descent_double_square_four_sum
  49. 0049have hone : 2 * h + 1 = S (2 * h)
  50. 0050simp
  51. 0051rewrite hone
  52. 0052rewrite hone
  53. 0053specialize lt_of_le_of_lt (a * a + b * b + c * c + d * d)
  54. 0054specialize lt_of_le_of_lt ((2 * h) * (2 * h))
  55. 0055specialize lt_of_le_of_lt (S (2 * h) * S (2 * h))
  56. 0056apply lt_of_le_of_lt
  57. 0057exact hnorm
  58. 0058apply square_lt_successor_square