PA005L

quadratic_residue_search_up_to

Stable checked-use theorem · independently closed

Inclusive bounded search constructively decides square congruence.

Exact expanded PA statement

forall B p a. ~(p = 0) -> ((exists qr_x_search_yes. (exists qr_bound_search_yes. qr_bound_search_yes + qr_x_search_yes = B) /\ (exists qr_u_search_yes qr_v_search_yes. qr_x_search_yes * qr_x_search_yes + p * qr_u_search_yes = a + p * qr_v_search_yes)) \/ (forall qr_x_search_no. (exists qr_bound_search_no. qr_bound_search_no + qr_x_search_no = B) -> ~(exists qr_u_search_no qr_v_search_no. qr_x_search_no * qr_x_search_no + p * qr_u_search_no = a + p * qr_v_search_no)))

Structural proof guide

Generated structural guide

Inclusive bounded search constructively decides square congruence.

Use the direct prerequisites mod_eq_decidable_nonzero, add_eq_zero_right, le_eq_or_lt, add_succ_left, zero_add as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (9), intermediate claims (5), equality transport (4), certified simplification (2).

Referenced ingredients

PA005K mod_eq_decidable_nonzero PA0004 add_eq_zero_right PA000W le_eq_or_lt PA000E add_succ_left PA0001 zero_add

Proof neighborhood

Direct dependencies

PA005K mod_eq_decidable_nonzero PA0004 add_eq_zero_right PA000W le_eq_or_lt PA000E add_succ_left PA0001 zero_add

Direct dependents

PA005M quadratic_residue_bounded_decidable_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001induction B
  2. 0002intro p
  3. 0003intro a
  4. 0004intro hp
  5. 0005have hdec : (exists u v. 0 * 0 + p * u = a + p * v) \/ ~(exists u v. 0 * 0 + p * u = a + p * v)
  6. 0006specialize mod_eq_decidable_nonzero p
  7. 0007specialize mod_eq_decidable_nonzero (0 * 0)
  8. 0008specialize mod_eq_decidable_nonzero a
  9. 0009apply mod_eq_decidable_nonzero
  10. 0010exact hp
  11. 0011cases hdec
  12. 0012left
  13. 0013exists 0
  14. 0014split
  15. 0015exists 0
  16. 0016simp
  17. 0017exact hdec_left
  18. 0018right
  19. 0019intro x
  20. 0020intro hx
  21. 0021intro hs
  22. 0022cases hx
  23. 0023have hx0 : x = 0
  24. 0024specialize add_eq_zero_right x1
  25. 0025specialize add_eq_zero_right x
  26. 0026apply add_eq_zero_right
  27. 0027exact hx_witness
  28. 0028apply hdec_right
  29. 0029rewrite hx0 at hs
  30. 0030rewrite hx0 at hs
  31. 0031exact hs
  32. 0032intro p
  33. 0033intro a
  34. 0034intro hp
  35. 0035have hprev : (exists x. (exists h. h + x = B) /\ exists u v. x * x + p * u = a + p * v) \/ (forall x. (exists h. h + x = B) -> ~(exists u v. x * x + p * u = a + p * v))
  36. 0036specialize IH p
  37. 0037specialize IH a
  38. 0038apply IH
  39. 0039exact hp
  40. 0040cases hprev
  41. 0041left
  42. 0042cases hprev_left
  43. 0043cases hprev_left_witness
  44. 0044exists x
  45. 0045split
  46. 0046cases hprev_left_witness_left
  47. 0047exists S x1
  48. 0048trans S (x1 + x)
  49. 0049apply add_succ_left
  50. 0050congr
  51. 0051exact hprev_left_witness_left_witness
  52. 0052exact hprev_left_witness_right
  53. 0053have hdec : (exists u v. (S B) * (S B) + p * u = a + p * v) \/ ~(exists u v. (S B) * (S B) + p * u = a + p * v)
  54. 0054specialize mod_eq_decidable_nonzero p
  55. 0055specialize mod_eq_decidable_nonzero ((S B) * (S B))
  56. 0056specialize mod_eq_decidable_nonzero a
  57. 0057apply mod_eq_decidable_nonzero
  58. 0058exact hp
  59. 0059cases hdec
  60. 0060left
  61. 0061exists S B
  62. 0062split
  63. 0063exists 0
  64. 0064simp
  65. 0065congr
  66. 0066specialize zero_add B
  67. 0067exact zero_add
  68. 0068exact hdec_left
  69. 0069right
  70. 0070intro x
  71. 0071intro hx
  72. 0072intro hs
  73. 0073specialize le_eq_or_lt x
  74. 0074specialize le_eq_or_lt (S B)
  75. 0075have hcases : x = S B \/ exists k. k + S x = S B
  76. 0076apply le_eq_or_lt
  77. 0077exact hx
  78. 0078cases hcases
  79. 0079apply hdec_right
  80. 0080rewrite hcases_left at hs
  81. 0081rewrite hcases_left at hs
  82. 0082exact hs
  83. 0083apply hprev_right
  84. 0084cases hcases_right
  85. 0085exists x1
  86. 0086apply PA2
  87. 0087trans x1 + S x
  88. 0088symm
  89. 0089apply PA4
  90. 0090exact hcases_right_witness
  91. 0091exact hs