PA0087

quadratic_residue_mod_equiv

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

Quadratic residuosity depends only on the balanced congruence class.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

31 script commands · 11 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
mod eq symmmod eq trans
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro r
  4. L4
    intro har
02Separate the logical casesL5–5

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L5
    split
03Fix variables and assumptionsL6–6

Work with arbitrary variables or the premises of the current implication.

  1. L6
    intro hqa
04Separate the logical casesL7–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hqa
05Construct an explicit witnessL8–8

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists x
06Use earlier factsL9–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    specialize mod_eq_trans p
  2. L10
    specialize mod_eq_trans (x * x)
  3. L11
    specialize mod_eq_trans a
  4. L12
    specialize mod_eq_trans r
  5. L13
    apply mod_eq_trans
  6. L14
    exact hqa_witness
  7. L15
    exact har
07Fix variables and assumptionsL16–16

Work with arbitrary variables or the premises of the current implication.

  1. L16
    intro hqr
08Separate the logical casesL17–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hqr
09Construct an explicit witnessL18–18

Supply the displayed value, then prove that it has the required property.

  1. L18
    exists x
10Establish hraL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L19
    have 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
  2. L20
    specialize mod_eq_symm p
  3. L21
    specialize mod_eq_symm a
  4. L22
    specialize mod_eq_symm r
  5. L23
    apply mod_eq_symm
  6. L24
    exact har
  7. L25
    specialize mod_eq_trans p
  8. L26
    specialize mod_eq_trans (x * x)
  9. L27
    specialize mod_eq_trans r
  10. L28
    specialize mod_eq_trans a
11Use earlier factsL29–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    apply mod_eq_trans
  2. L30
    exact hqr_witness
  3. L31
    exact hra

Library-wide reading audit

Original exact command ledger · 31 lines
  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