FS0049 · theorem body

four_square_ordered_half_square_injective

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

On the inclusive odd-prime half range, congruent squares of ordered coordinates have equal coordinates.

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. ∀ h. ∀ x. ∀ y. ∀ d. p = 2 · h + 1 → Prime(p) → Le(x,h) → Le(y,h) → y = x + d → ModEq(p,x · x,y · y) → x = y

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 PD0008 ModEq

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd
Exact expanded first-order statement
forall p h x y d. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_fsri_prime frm_prime_right_fsri_prime. p = frm_prime_left_fsri_prime * frm_prime_right_fsri_prime -> frm_prime_left_fsri_prime = 1 \/ frm_prime_right_fsri_prime = 1)) -> (exists fsri_gap_ordered_x. fsri_gap_ordered_x + (x) = (h)) -> (exists fsri_gap_ordered_y. fsri_gap_ordered_y + (y) = (h)) -> y = x + d -> (exists fsri_left_ordered_equal fsri_right_ordered_equal. (x * x) + (p) * fsri_left_ordered_equal = (y * y) + (p) * fsri_right_ordered_equal) -> x = y

Proof neighborhood

Direct theorem prerequisites

FS0048 four_square_ordered_square_congruence_factors euclid_prime_dvd_product · Stable closed odd_half_strictly_below_modulus · Alpha closed lt_of_le_of_lt · Stable closed FS0046 four_square_bounded_multiple_is_zero FS0045 four_square_half_sum_below_odd add_eq_zero_left · Stable closed add_eq_zero_right · Stable closed add_comm · Stable closed

Direct theorem dependents

FS004A four_square_prime_half_square_residues_injective

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

88 script commands · 17 reading checkpoints · 10 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 ordered square congruence factorsfour square bounded multiple is zerofour square half sum below odd
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro d
  6. L6
    intro hodd
  7. L7
    intro hprime
  8. L8
    intro hx
  9. L9
    intro hy
  10. L10
    intro horder
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsquares
03Establish hproductL12–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square ordered square congruence factors.

  1. L12
    have hproduct : Dvd(p,d · (y + x))Definitions: Dvd(p,d · (y + x))Original native command in the exact edition
  2. L13
    specialize four_square_ordered_square_congruence_factors p
  3. L14
    specialize four_square_ordered_square_congruence_factors x
  4. L15
    specialize four_square_ordered_square_congruence_factors y
  5. L16
    specialize four_square_ordered_square_congruence_factors d
  6. L17
    apply four_square_ordered_square_congruence_factors
  7. L18
    exact horder
  8. L19
    exact hsquares
04Establish hsplitL20–26

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

  1. L20
    have hsplit : Dvd(p,d) ∨ Dvd(p,y + x)Definitions: Dvd(p,d)Dvd(p,y + x)Original native command in the exact edition
  2. L21
    specialize euclid_prime_dvd_product p
  3. L22
    specialize euclid_prime_dvd_product d
  4. L23
    specialize euclid_prime_dvd_product (y + x)
  5. L24
    apply euclid_prime_dvd_product
  6. L25
    exact hprime
  7. L26
    exact hproduct
05Separate the logical casesL27–27

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

  1. L27
    cases hsplit
06Establish hdleyL28–28

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

  1. L28
07Construct an explicit witnessL29–29

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

  1. L29
    exists x
08Calculate and transport equalitiesL30–30

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

  1. L30
    symm
09Use earlier factsL31–31

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

  1. L31
    exact horder
10Establish hylpL32–41

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

  1. L32
  2. L33
    specialize lt_of_le_of_lt y
  3. L34
    specialize lt_of_le_of_lt h
  4. L35
    specialize lt_of_le_of_lt p
  5. L36
    apply lt_of_le_of_lt
  6. L37
    exact hy
  7. L38
    specialize odd_half_strictly_below_modulus p
  8. L39
    specialize odd_half_strictly_below_modulus h
  9. L40
    apply odd_half_strictly_below_modulus
  10. L41
    exact hodd
11Establish hdlpL42–48

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

  1. L42
  2. L43
    specialize lt_of_le_of_lt d
  3. L44
    specialize lt_of_le_of_lt y
  4. L45
    specialize lt_of_le_of_lt p
  5. L46
    apply lt_of_le_of_lt
  6. L47
    exact hdley
  7. L48
    exact hylp
12Establish hzeroL49–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square bounded multiple is zero.

  1. L49
    have hzero : d = 0
  2. L50
    specialize four_square_bounded_multiple_is_zero p
  3. L51
    specialize four_square_bounded_multiple_is_zero d
  4. L52
    apply four_square_bounded_multiple_is_zero
  5. L53
    exact hdlp
  6. L54
    exact hsplit_left
  7. L55
    rewrite hzero at horder
  8. L56
    symm
  9. L57
    trans x + 0
  10. L58
    exact horder
13Use earlier factsL59–59

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

  1. L59
    apply PA3
14Establish hsum_boundL60–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square half sum below odd.

  1. L60
    have hsum_bound : Lt(y + x,p)Definitions: Lt(y + x,p)Original native command in the exact edition
  2. L61
    specialize four_square_half_sum_below_odd p
  3. L62
    specialize four_square_half_sum_below_odd h
  4. L63
    specialize four_square_half_sum_below_odd y
  5. L64
    specialize four_square_half_sum_below_odd x
  6. L65
    apply four_square_half_sum_below_odd
  7. L66
    exact hodd
  8. L67
    exact hy
  9. L68
    exact hx
15Establish hsum_zeroL69–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square bounded multiple is zero.

  1. L69
    have hsum_zero : y + x = 0
  2. L70
    specialize four_square_bounded_multiple_is_zero p
  3. L71
    specialize four_square_bounded_multiple_is_zero (y + x)
  4. L72
    apply four_square_bounded_multiple_is_zero
  5. L73
    exact hsum_bound
  6. L74
    exact hsplit_right
16Establish hyzeroL75–79

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

  1. L75
    have hyzero : y = 0
  2. L76
    specialize add_eq_zero_left y
  3. L77
    specialize add_eq_zero_left x
  4. L78
    apply add_eq_zero_left
  5. L79
    exact hsum_zero
17Establish hxzeroL80–88

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

  1. L80
    have hxzero : x = 0
  2. L81
    specialize add_eq_zero_right y
  3. L82
    specialize add_eq_zero_right x
  4. L83
    apply add_eq_zero_right
  5. L84
    exact hsum_zero
  6. L85
    trans 0
  7. L86
    exact hxzero
  8. L87
    symm
  9. L88
    exact hyzero

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro x
  4. 0004intro y
  5. 0005intro d
  6. 0006intro hodd
  7. 0007intro hprime
  8. 0008intro hx
  9. 0009intro hy
  10. 0010intro horder
  11. 0011intro hsquares
  12. 0012have hproduct : Dvd(p,d · (y + x))
    Exact native replay linehave hproduct : exists fsri_factor_ordered_product. (d * (y + x)) = (p) * fsri_factor_ordered_product
  13. 0013specialize four_square_ordered_square_congruence_factors p
  14. 0014specialize four_square_ordered_square_congruence_factors x
  15. 0015specialize four_square_ordered_square_congruence_factors y
  16. 0016specialize four_square_ordered_square_congruence_factors d
  17. 0017apply four_square_ordered_square_congruence_factors
  18. 0018exact horder
  19. 0019exact hsquares
  20. 0020have hsplit : Dvd(p,d) ∨ Dvd(p,y + x)
    Exact native replay linehave hsplit : (exists fsri_factor_ordered_gap_divides. (d) = (p) * fsri_factor_ordered_gap_divides) \/ (exists fsri_factor_ordered_sum_divides. (y + x) = (p) * fsri_factor_ordered_sum_divides)
  21. 0021specialize euclid_prime_dvd_product p
  22. 0022specialize euclid_prime_dvd_product d
  23. 0023specialize euclid_prime_dvd_product (y + x)
  24. 0024apply euclid_prime_dvd_product
  25. 0025exact hprime
  26. 0026exact hproduct
  27. 0027cases hsplit
  28. 0028have hdley : Le(d,y)
    Exact native replay linehave hdley : exists fsri_gap_ordered_gap_le_y. fsri_gap_ordered_gap_le_y + (d) = (y)
  29. 0029exists x
  30. 0030symm
  31. 0031exact horder
  32. 0032have hylp : Lt(y,p)
    Exact native replay linehave hylp : exists fsri_gap_ordered_y_lt_prime. fsri_gap_ordered_y_lt_prime + S (y) = (p)
  33. 0033specialize lt_of_le_of_lt y
  34. 0034specialize lt_of_le_of_lt h
  35. 0035specialize lt_of_le_of_lt p
  36. 0036apply lt_of_le_of_lt
  37. 0037exact hy
  38. 0038specialize odd_half_strictly_below_modulus p
  39. 0039specialize odd_half_strictly_below_modulus h
  40. 0040apply odd_half_strictly_below_modulus
  41. 0041exact hodd
  42. 0042have hdlp : Lt(d,p)
    Exact native replay linehave hdlp : exists fsri_gap_ordered_gap_lt_prime. fsri_gap_ordered_gap_lt_prime + S (d) = (p)
  43. 0043specialize lt_of_le_of_lt d
  44. 0044specialize lt_of_le_of_lt y
  45. 0045specialize lt_of_le_of_lt p
  46. 0046apply lt_of_le_of_lt
  47. 0047exact hdley
  48. 0048exact hylp
  49. 0049have hzero : d = 0
  50. 0050specialize four_square_bounded_multiple_is_zero p
  51. 0051specialize four_square_bounded_multiple_is_zero d
  52. 0052apply four_square_bounded_multiple_is_zero
  53. 0053exact hdlp
  54. 0054exact hsplit_left
  55. 0055rewrite hzero at horder
  56. 0056symm
  57. 0057trans x + 0
  58. 0058exact horder
  59. 0059apply PA3
  60. 0060have hsum_bound : Lt(y + x,p)
    Exact native replay linehave hsum_bound : exists fsri_gap_ordered_sum_lt_prime. fsri_gap_ordered_sum_lt_prime + S (y + x) = (p)
  61. 0061specialize four_square_half_sum_below_odd p
  62. 0062specialize four_square_half_sum_below_odd h
  63. 0063specialize four_square_half_sum_below_odd y
  64. 0064specialize four_square_half_sum_below_odd x
  65. 0065apply four_square_half_sum_below_odd
  66. 0066exact hodd
  67. 0067exact hy
  68. 0068exact hx
  69. 0069have hsum_zero : y + x = 0
  70. 0070specialize four_square_bounded_multiple_is_zero p
  71. 0071specialize four_square_bounded_multiple_is_zero (y + x)
  72. 0072apply four_square_bounded_multiple_is_zero
  73. 0073exact hsum_bound
  74. 0074exact hsplit_right
  75. 0075have hyzero : y = 0
  76. 0076specialize add_eq_zero_left y
  77. 0077specialize add_eq_zero_left x
  78. 0078apply add_eq_zero_left
  79. 0079exact hsum_zero
  80. 0080have hxzero : x = 0
  81. 0081specialize add_eq_zero_right y
  82. 0082specialize add_eq_zero_right x
  83. 0083apply add_eq_zero_right
  84. 0084exact hsum_zero
  85. 0085trans 0
  86. 0086exact hxzero
  87. 0087symm
  88. 0088exact hyzero