PA0087

quadratic_residue_mod_equiv

Alpha v16 checked-use theorem · independently closed; not Stable

Quadratic residuosity depends only on the balanced congruence class.

Exact expanded PA statement

forall p a r. (exists wpp_mod_left_eca_qres_transport_mod wpp_mod_right_eca_qres_transport_mod. (a) + p * wpp_mod_left_eca_qres_transport_mod = (r) + p * wpp_mod_right_eca_qres_transport_mod) -> ((((exists qr_x_eca_qres_transport_a. exists qr_u_eca_qres_transport_a qr_v_eca_qres_transport_a. qr_x_eca_qres_transport_a * qr_x_eca_qres_transport_a + p * qr_u_eca_qres_transport_a = a + p * qr_v_eca_qres_transport_a) -> (exists qr_x_eca_qres_transport_r. exists qr_u_eca_qres_transport_r qr_v_eca_qres_transport_r. qr_x_eca_qres_transport_r * qr_x_eca_qres_transport_r + p * qr_u_eca_qres_transport_r = r + p * qr_v_eca_qres_transport_r)) /\ ((exists qr_x_eca_qres_transport_r. exists qr_u_eca_qres_transport_r qr_v_eca_qres_transport_r. qr_x_eca_qres_transport_r * qr_x_eca_qres_transport_r + p * qr_u_eca_qres_transport_r = r + p * qr_v_eca_qres_transport_r) -> (exists qr_x_eca_qres_transport_a. exists qr_u_eca_qres_transport_a qr_v_eca_qres_transport_a. qr_x_eca_qres_transport_a * qr_x_eca_qres_transport_a + p * qr_u_eca_qres_transport_a = a + p * qr_v_eca_qres_transport_a))))

Structural proof guide

Generated structural guide

Quadratic residuosity depends only on the balanced congruence class.

Use the direct prerequisites mod_eq_symm, mod_eq_trans as previously established PA formulas.

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

Referenced ingredients

PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro r
  4. 0004intro har
  5. 0005split
  6. 0006intro hqa
  7. 0007cases hqa
  8. 0008exists x
  9. 0009specialize mod_eq_trans p
  10. 0010specialize mod_eq_trans (x * x)
  11. 0011specialize mod_eq_trans a
  12. 0012specialize mod_eq_trans r
  13. 0013apply mod_eq_trans
  14. 0014exact hqa_witness
  15. 0015exact har
  16. 0016intro hqr
  17. 0017cases hqr
  18. 0018exists x
  19. 0019have hra : exists wpp_mod_left_eca_qres_proof_reverse wpp_mod_right_eca_qres_proof_reverse. (r) + p * wpp_mod_left_eca_qres_proof_reverse = (a) + p * wpp_mod_right_eca_qres_proof_reverse
  20. 0020specialize mod_eq_symm p
  21. 0021specialize mod_eq_symm a
  22. 0022specialize mod_eq_symm r
  23. 0023apply mod_eq_symm
  24. 0024exact har
  25. 0025specialize mod_eq_trans p
  26. 0026specialize mod_eq_trans (x * x)
  27. 0027specialize mod_eq_trans r
  28. 0028specialize mod_eq_trans a
  29. 0029apply mod_eq_trans
  30. 0030exact hqr_witness
  31. 0031exact hra