PA0087 · theorem

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.

Statement with defined notation

∀ p. ∀ a. ∀ r. ModEq(p,a,r) → (QRes(p,a) → QRes(p,r)) ∧ (QRes(p,r) → QRes(p,a))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq PD0021 QRes

5 occurrences

In local proof propositions

PD0008 ModEq

1 occurrences

Exact expanded native-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))))

Proof neighborhood

Direct theorem prerequisites

PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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 defined 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 : ModEq(p,r,a)
    Exact native replay linehave 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