PA005R

quadratic_residue_bounded_equiv

Stable checked-use theorem · independently closed

Every square witness has an equivalent canonical bounded root.

Exact expanded PA statement

forall p a. ~(p = 0) -> (((exists qr_x_unbounded. exists qr_u_unbounded qr_v_unbounded. qr_x_unbounded * qr_x_unbounded + p * qr_u_unbounded = a + p * qr_v_unbounded) -> (exists qr_x_bounded. (exists qr_h_bounded. qr_h_bounded + S qr_x_bounded = p) /\ exists qr_u_bounded qr_v_bounded. qr_x_bounded * qr_x_bounded + p * qr_u_bounded = a + p * qr_v_bounded)) /\ ((exists qr_x_bounded. (exists qr_h_bounded. qr_h_bounded + S qr_x_bounded = p) /\ exists qr_u_bounded qr_v_bounded. qr_x_bounded * qr_x_bounded + p * qr_u_bounded = a + p * qr_v_bounded) -> (exists qr_x_unbounded. exists qr_u_unbounded qr_v_unbounded. qr_x_unbounded * qr_x_unbounded + p * qr_u_unbounded = a + p * qr_v_unbounded)))

Structural proof guide

Generated structural guide

Every square witness has an equivalent canonical bounded root.

Use the direct prerequisites division_remainder_exists, square_residue_witness, remainder_decomposition_to_mod_eq, mod_eq_symm, mod_eq_trans, mul_comm, zero_add as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (6), certified simplification (1).

Referenced ingredients

PA001D division_remainder_exists PA005Q square_residue_witness PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA000H mul_comm PA0001 zero_add

Proof neighborhood

Direct dependencies

PA001D division_remainder_exists PA005Q square_residue_witness PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA000H mul_comm PA0001 zero_add

Direct dependents

PA005S quadratic_residue_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. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004split
  5. 0005intro hunbounded
  6. 0006cases hunbounded
  7. 0007have hdivision : exists q r. x = p * q + r /\ exists h. h + S r = p
  8. 0008specialize division_remainder_exists p
  9. 0009specialize division_remainder_exists x
  10. 0010apply division_remainder_exists
  11. 0011exact hp
  12. 0012cases hdivision
  13. 0013cases hdivision_witness
  14. 0014cases hdivision_witness_witness
  15. 0015have hsquare : exists w. x * x = p * w + x2 * x2
  16. 0016specialize square_residue_witness p
  17. 0017specialize square_residue_witness x
  18. 0018specialize square_residue_witness x1
  19. 0019specialize square_residue_witness x2
  20. 0020specialize square_residue_witness 0
  21. 0021specialize square_residue_witness (x2 * x2)
  22. 0022apply square_residue_witness
  23. 0023exact hdivision_witness_witness_left
  24. 0024simp
  25. 0025specialize zero_add (x2 * x2)
  26. 0026symm
  27. 0027exact zero_add
  28. 0028cases hsquare
  29. 0029have hdecomp : x * x = x3 * p + x2 * x2
  30. 0030trans p * x3 + x2 * x2
  31. 0031exact hsquare_witness
  32. 0032congr
  33. 0033apply mul_comm
  34. 0034refl
  35. 0035have hxr : exists u v. x * x + p * u = x2 * x2 + p * v
  36. 0036specialize remainder_decomposition_to_mod_eq p
  37. 0037specialize remainder_decomposition_to_mod_eq (x * x)
  38. 0038specialize remainder_decomposition_to_mod_eq x3
  39. 0039specialize remainder_decomposition_to_mod_eq (x2 * x2)
  40. 0040apply remainder_decomposition_to_mod_eq
  41. 0041exact hdecomp
  42. 0042have hrx : exists u v. x2 * x2 + p * u = x * x + p * v
  43. 0043specialize mod_eq_symm p
  44. 0044specialize mod_eq_symm (x * x)
  45. 0045specialize mod_eq_symm (x2 * x2)
  46. 0046apply mod_eq_symm
  47. 0047exact hxr
  48. 0048have hra : exists u v. x2 * x2 + p * u = a + p * v
  49. 0049specialize mod_eq_trans p
  50. 0050specialize mod_eq_trans (x2 * x2)
  51. 0051specialize mod_eq_trans (x * x)
  52. 0052specialize mod_eq_trans a
  53. 0053apply mod_eq_trans
  54. 0054exact hrx
  55. 0055exact hunbounded_witness
  56. 0056exists x2
  57. 0057split
  58. 0058exact hdivision_witness_witness_right
  59. 0059exact hra
  60. 0060intro hbounded
  61. 0061cases hbounded
  62. 0062cases hbounded_witness
  63. 0063exists x
  64. 0064exact hbounded_witness_right