PA005M

quadratic_residue_bounded_decidable_nonzero

Stable checked-use theorem · independently closed

A nonzero modulus admits a finite constructive residue search.

Exact expanded PA statement

forall p a. ~(p = 0) -> (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)

Structural proof guide

Generated structural guide

A nonzero modulus admits a finite constructive residue search.

Use the direct prerequisites nonzero_is_succ, quadratic_residue_search_up_to as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (2).

Referenced ingredients

PA001V nonzero_is_succ PA005L quadratic_residue_search_up_to

Proof neighborhood

Direct dependencies

PA001V nonzero_is_succ PA005L quadratic_residue_search_up_to

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. 0004have hs : exists B. p = S B
  5. 0005specialize nonzero_is_succ p
  6. 0006apply nonzero_is_succ
  7. 0007exact hp
  8. 0008cases hs
  9. 0009have hsearch : (exists r. (exists h. h + r = x) /\ exists u v. r * r + p * u = a + p * v) \/ (forall r. (exists h. h + r = x) -> ~(exists u v. r * r + p * u = a + p * v))
  10. 0010specialize quadratic_residue_search_up_to x
  11. 0011specialize quadratic_residue_search_up_to p
  12. 0012specialize quadratic_residue_search_up_to a
  13. 0013apply quadratic_residue_search_up_to
  14. 0014exact hp
  15. 0015cases hsearch
  16. 0016left
  17. 0017cases hsearch_left
  18. 0018cases hsearch_left_witness
  19. 0019exists x1
  20. 0020split
  21. 0021cases hsearch_left_witness_left
  22. 0022exists x2
  23. 0023trans S (x2 + x1)
  24. 0024apply PA4
  25. 0025trans S x
  26. 0026congr
  27. 0027exact hsearch_left_witness_left_witness
  28. 0028symm
  29. 0029exact hs_witness
  30. 0030exact hsearch_left_witness_right
  31. 0031right
  32. 0032intro hbounded
  33. 0033cases hbounded
  34. 0034cases hbounded_witness
  35. 0035specialize hsearch_right x1
  36. 0036apply hsearch_right
  37. 0037cases hbounded_witness_left
  38. 0038exists x2
  39. 0039apply PA2
  40. 0040trans x2 + S x1
  41. 0041symm
  42. 0042apply PA4
  43. 0043trans p
  44. 0044exact hbounded_witness_left_witness
  45. 0045exact hs_witness
  46. 0046exact hbounded_witness_right