FS001X · theorem body

four_square_descent_odd_half_norm_strict

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

Statement with defined notation

∀ h. ∀ a. ∀ b. ∀ c. ∀ d. Le(a,h) → Le(b,h) → Le(c,h) → Le(d,h) → Lt(a · a + b · b + c · c + d · d,(2 · h + 1) · (2 · h + 1))

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

In local proof propositions

PD0001 Le
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

mul_le_mul · Alpha closed FS001V four_square_descent_add_le_add add_assoc · Stable closed FS001W four_square_descent_double_square_four_sum lt_of_le_of_lt · Stable closed square_lt_successor_square · Alpha closed

Direct theorem dependents

FS000M four_square_odd_prime_half_seed_norm_strict FS001Y four_square_descent_odd_centered_norm_strict

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

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.

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 (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 : Le(a · a,h · h)Definitions: Le(a · a,h · h)Original native command in the exact edition
  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 : Le(b · b,h · h)Definitions: Le(b · b,h · h)Original native command in the exact edition
  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 : Le(c · c,h · h)Definitions: Le(c · c,h · h)Original native command in the exact edition
  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 : Le(d · d,h · h)Definitions: Le(d · d,h · h)Original native command in the exact edition
  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 : Le(a · a + b · b,h · h + h · h)Definitions: Le(a · a + b · b,h · h + h · h)Original native command in the exact edition
  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 : Le(c · c + d · d,h · h + h · h)Definitions: Le(c · c + d · d,h · h + h · h)Original native command in the exact edition
  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 : Le(a · a + b · b + (c · c + d · d),h · h + h · h + (h · h + h · h))Definitions: Le(a · a + b · b + (c · c + d · d),h · h + h · h + (h · h + h · h))Original native command in the exact edition
  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 : Le(a · a + b · b + c · c + d · d,2 · h · (2 · h))Definitions: Le(a · a + b · b + c · c + d · d,2 · h · (2 · h))Original native command in the exact edition
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 defined 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 : Le(a · a,h · h)
    Exact native replay linehave hsa : exists gap. gap + a * a = h * h
  11. 0011apply mul_le_mul
  12. 0012exact ha
  13. 0013exact ha
  14. 0014have hsb : Le(b · b,h · h)
    Exact native replay linehave hsb : exists gap. gap + b * b = h * h
  15. 0015apply mul_le_mul
  16. 0016exact hb
  17. 0017exact hb
  18. 0018have hsc : Le(c · c,h · h)
    Exact native replay linehave hsc : exists gap. gap + c * c = h * h
  19. 0019apply mul_le_mul
  20. 0020exact hc
  21. 0021exact hc
  22. 0022have hsd : Le(d · d,h · h)
    Exact native replay linehave hsd : exists gap. gap + d * d = h * h
  23. 0023apply mul_le_mul
  24. 0024exact hd
  25. 0025exact hd
  26. 0026have hab : Le(a · a + b · b,h · h + h · h)
    Exact native replay linehave 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 : Le(c · c + d · d,h · h + h · h)
    Exact native replay linehave 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 : Le(a · a + b · b + (c · c + d · d),h · h + h · h + (h · h + h · h))
    Exact native replay linehave 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 : Le(a · a + b · b + c · c + d · d,2 · h · (2 · h))
    Exact native replay linehave 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