PA005S

quadratic_residue_decidable_nonzero

Stable checked-use theorem · independently closed

Quadratic residuosity is constructively decidable at nonzero modulus.

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_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

Quadratic residuosity is constructively decidable at nonzero modulus.

Use the direct prerequisites quadratic_residue_bounded_decidable_nonzero, quadratic_residue_bounded_equiv as previously established PA formulas.

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

Referenced ingredients

PA005M quadratic_residue_bounded_decidable_nonzero PA005R quadratic_residue_bounded_equiv

Proof neighborhood

Direct dependencies

PA005M quadratic_residue_bounded_decidable_nonzero PA005R quadratic_residue_bounded_equiv

Direct dependents

PA00BN bounded_euler_criterion_dichotomy

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 hequiv : (((exists x. exists u v. x * x + p * u = a + p * v) -> (exists r. (exists h. h + S r = p) /\ exists u v. r * r + p * u = a + p * v)) /\ ((exists r. (exists h. h + S r = p) /\ exists u v. r * r + p * u = a + p * v) -> (exists x. exists u v. x * x + p * u = a + p * v)))
  5. 0005specialize quadratic_residue_bounded_equiv p
  6. 0006specialize quadratic_residue_bounded_equiv a
  7. 0007apply quadratic_residue_bounded_equiv
  8. 0008exact hp
  9. 0009cases hequiv
  10. 0010have hdec : (exists r. (exists h. h + S r = p) /\ exists u v. r * r + p * u = a + p * v) \/ ~(exists r. (exists h. h + S r = p) /\ exists u v. r * r + p * u = a + p * v)
  11. 0011specialize quadratic_residue_bounded_decidable_nonzero p
  12. 0012specialize quadratic_residue_bounded_decidable_nonzero a
  13. 0013apply quadratic_residue_bounded_decidable_nonzero
  14. 0014exact hp
  15. 0015cases hdec
  16. 0016left
  17. 0017apply hequiv_right
  18. 0018exact hdec_left
  19. 0019right
  20. 0020intro hunbounded
  21. 0021apply hdec_right
  22. 0022apply hequiv_left
  23. 0023exact hunbounded