FS0049

four_square_ordered_half_square_injective

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

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

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

FS0048 four_square_ordered_square_congruence_factors euclid_prime_dvd_product Stable theorem; checked-use authorized odd_half_strictly_below_modulus Alpha theorem; checked-use authorized lt_of_le_of_lt Stable theorem; checked-use authorized FS0046 four_square_bounded_multiple_is_zero FS0045 four_square_half_sum_below_odd add_eq_zero_left Stable theorem; checked-use authorized add_eq_zero_right Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

FS004A four_square_prime_half_square_residues_injective

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

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.

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 : exists fsri_factor_ordered_product. (d * (y + x)) = (p) * fsri_factor_ordered_product
  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 : (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)
  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
    have hdley : exists fsri_gap_ordered_gap_le_y. fsri_gap_ordered_gap_le_y + (d) = (y)
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
    have hylp : exists fsri_gap_ordered_y_lt_prime. fsri_gap_ordered_y_lt_prime + S (y) = (p)
  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
    have hdlp : exists fsri_gap_ordered_gap_lt_prime. fsri_gap_ordered_gap_lt_prime + S (d) = (p)
  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 : exists fsri_gap_ordered_sum_lt_prime. fsri_gap_ordered_sum_lt_prime + S (y + x) = (p)
  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 exact 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 : 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 : (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 : 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 : 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 : 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 : 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