PA00BQ · theorem

bounded_euler_criterion_residue_iff

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

For bounded nonzero inputs, quadratic residuosity is equivalent to the half-power residue one.

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. ∀ n. ∀ h. ∀ A. p = S n → Prime(p) → ¬a = 0 → Lt(a,p) → n = h + h → Pow(a,h,A) → (QRes(p,a) → ModEq(p,A,1)) ∧ (ModEq(p,A,1) → 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

PD0002 Lt PD0004 Prime PD0008 ModEq PD0020 Pow PD0021 QRes

7 occurrences

In local proof propositions

PD0008 ModEq PD0021 QRes

6 occurrences

Exact expanded native-PA statement
forall p a n h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_ecb_prime esi_prime_right_ecb_prime. p = esi_prime_left_ecb_prime * esi_prime_right_ecb_prime -> esi_prime_left_ecb_prime = 1 \/ esi_prime_right_ecb_prime = 1)) -> ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> n = h + h -> (exists ff_b_ecb_power ff_c_ecb_power. ((forall ff_i_ecb_power_repeat. (exists ff_lt_ecb_power_repeat_bound. ff_lt_ecb_power_repeat_bound + S ff_i_ecb_power_repeat = h) -> (((exists ff_h_ecb_power_repeat_decoded. ff_h_ecb_power_repeat_decoded + S (a) = S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_repeat_decoded. ff_b_ecb_power = ff_q_ecb_power_repeat_decoded * S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power) + (a)))) /\ (exists ff_u_ecb_power_product ff_v_ecb_power_product. ((((exists ff_h_ecb_power_product_start. ff_h_ecb_power_product_start + S (1) = S ((S (0)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_start. ff_u_ecb_power_product = ff_q_ecb_power_product_start * S ((S (0)) * ff_v_ecb_power_product) + (1))) /\ ((((exists ff_h_ecb_power_product_terminal. ff_h_ecb_power_product_terminal + S (A) = S ((S (h)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_terminal. ff_u_ecb_power_product = ff_q_ecb_power_product_terminal * S ((S (h)) * ff_v_ecb_power_product) + (A))) /\ forall ff_i_ecb_power_product. (exists ff_lt_ecb_power_product_bound. ff_lt_ecb_power_product_bound + S ff_i_ecb_power_product = h) -> exists ff_p_ecb_power_product ff_r_ecb_power_product ff_s_ecb_power_product. ((((exists ff_h_ecb_power_product_factor. ff_h_ecb_power_product_factor + S (ff_p_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_product_factor. ff_b_ecb_power = ff_q_ecb_power_product_factor * S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power) + (ff_p_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_partial. ff_h_ecb_power_product_partial + S (ff_r_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_partial. ff_u_ecb_power_product = ff_q_ecb_power_product_partial * S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_r_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_successor. ff_h_ecb_power_product_successor + S (ff_s_ecb_power_product) = S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_successor. ff_u_ecb_power_product = ff_q_ecb_power_product_successor * S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_s_ecb_power_product))) /\ ff_s_ecb_power_product = ff_r_ecb_power_product * ff_p_ecb_power_product)))))))) -> ((((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) -> (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) /\ ((exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one) -> (exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres))))

Proof neighborhood

Direct theorem prerequisites

PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_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

63 script commands · 18 reading checkpoints · 3 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 (4)
bounded euler criterion dichotomyodd prime one not mod predecessormod eq symmmod eq trans
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro h
  5. L5
    intro A
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro ha0
  9. L9
    intro hap
  10. L10
    intro heven
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hpower
03Establish hdichotomyL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion dichotomy.

  1. L12
    have hdichotomy : QRes(p,a) ∧ ModEq(p,A,1) ∨ ¬QRes(p,a) ∧ ModEq(p,A,n)Definitions: QRes(p,a)ModEq(p,A,1)ModEq(p,A,n)Original native command in the exact edition
  2. L13
    specialize bounded_euler_criterion_dichotomy p
  3. L14
    specialize bounded_euler_criterion_dichotomy a
  4. L15
    specialize bounded_euler_criterion_dichotomy n
  5. L16
    specialize bounded_euler_criterion_dichotomy h
  6. L17
    specialize bounded_euler_criterion_dichotomy A
  7. L18
    apply bounded_euler_criterion_dichotomy
  8. L19
    exact hpn
  9. L20
    exact hp
  10. L21
    exact ha0
04Use earlier factsL22–24

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

  1. L22
    exact hap
  2. L23
    exact heven
  3. L24
    exact hpower
05Establish hdistinctL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime one not mod predecessor.

  1. L25
    have hdistinct : ¬ModEq(p,1,n)Definitions: ModEq(p,1,n)Original native command in the exact edition
  2. L26
    intro hcollision
  3. L27
    specialize odd_prime_one_not_mod_predecessor p
  4. L28
    specialize odd_prime_one_not_mod_predecessor n
  5. L29
    specialize odd_prime_one_not_mod_predecessor h
  6. L30
    apply odd_prime_one_not_mod_predecessor
  7. L31
    exact hpn
  8. L32
    exact hp
  9. L33
    exact heven
  10. L34
    exact hcollision
06Separate the logical casesL35–35

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

  1. L35
    split
07Fix variables and assumptionsL36–36

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

  1. L36
    intro hqres
08Separate the logical casesL37–38

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

  1. L37
    cases hdichotomy
  2. L38
    cases hdichotomy_left
09Use earlier factsL39–39

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

  1. L39
    exact hdichotomy_left_right
10Separate the logical casesL40–41

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

  1. L40
    cases hdichotomy_right
  2. L41
    exfalso
11Use earlier factsL42–43

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

  1. L42
    apply hdichotomy_right_left
  2. L43
    exact hqres
12Fix variables and assumptionsL44–44

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

  1. L44
    intro hone
13Separate the logical casesL45–46

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

  1. L45
    cases hdichotomy
  2. L46
    cases hdichotomy_left
14Use earlier factsL47–47

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

  1. L47
    exact hdichotomy_left_left
15Separate the logical casesL48–49

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

  1. L48
    cases hdichotomy_right
  2. L49
    exfalso
16Use earlier factsL50–50

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

  1. L50
    apply hdistinct
17Establish hone_backL51–60

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

  1. L51
    have hone_back : ModEq(p,1,A)Definitions: ModEq(p,1,A)Original native command in the exact edition
  2. L52
    specialize mod_eq_symm p
  3. L53
    specialize mod_eq_symm A
  4. L54
    specialize mod_eq_symm 1
  5. L55
    apply mod_eq_symm
  6. L56
    exact hone
  7. L57
    specialize mod_eq_trans p
  8. L58
    specialize mod_eq_trans 1
  9. L59
    specialize mod_eq_trans A
  10. L60
    specialize mod_eq_trans n
18Use earlier factsL61–63

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

  1. L61
    apply mod_eq_trans
  2. L62
    exact hone_back
  3. L63
    exact hdichotomy_right_right

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro ha0
  9. 0009intro hap
  10. 0010intro heven
  11. 0011intro hpower
  12. 0012have hdichotomy : QRes(p,a) ∧ ModEq(p,A,1) ∨ ¬QRes(p,a) ∧ ModEq(p,A,n)
    Exact native replay linehave hdichotomy : (((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) /\ (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) \/ ((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)) /\ (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor)))
  13. 0013specialize bounded_euler_criterion_dichotomy p
  14. 0014specialize bounded_euler_criterion_dichotomy a
  15. 0015specialize bounded_euler_criterion_dichotomy n
  16. 0016specialize bounded_euler_criterion_dichotomy h
  17. 0017specialize bounded_euler_criterion_dichotomy A
  18. 0018apply bounded_euler_criterion_dichotomy
  19. 0019exact hpn
  20. 0020exact hp
  21. 0021exact ha0
  22. 0022exact hap
  23. 0023exact heven
  24. 0024exact hpower
  25. 0025have hdistinct : ¬ModEq(p,1,n)
    Exact native replay linehave hdistinct : ~(exists wpp_mod_left_ecb_one_mod_predecessor wpp_mod_right_ecb_one_mod_predecessor. (1) + p * wpp_mod_left_ecb_one_mod_predecessor = (n) + p * wpp_mod_right_ecb_one_mod_predecessor)
  26. 0026intro hcollision
  27. 0027specialize odd_prime_one_not_mod_predecessor p
  28. 0028specialize odd_prime_one_not_mod_predecessor n
  29. 0029specialize odd_prime_one_not_mod_predecessor h
  30. 0030apply odd_prime_one_not_mod_predecessor
  31. 0031exact hpn
  32. 0032exact hp
  33. 0033exact heven
  34. 0034exact hcollision
  35. 0035split
  36. 0036intro hqres
  37. 0037cases hdichotomy
  38. 0038cases hdichotomy_left
  39. 0039exact hdichotomy_left_right
  40. 0040cases hdichotomy_right
  41. 0041exfalso
  42. 0042apply hdichotomy_right_left
  43. 0043exact hqres
  44. 0044intro hone
  45. 0045cases hdichotomy
  46. 0046cases hdichotomy_left
  47. 0047exact hdichotomy_left_left
  48. 0048cases hdichotomy_right
  49. 0049exfalso
  50. 0050apply hdistinct
  51. 0051have hone_back : ModEq(p,1,A)
    Exact native replay linehave hone_back : exists wpp_mod_left_ecb_one_back wpp_mod_right_ecb_one_back. (1) + p * wpp_mod_left_ecb_one_back = (A) + p * wpp_mod_right_ecb_one_back
  52. 0052specialize mod_eq_symm p
  53. 0053specialize mod_eq_symm A
  54. 0054specialize mod_eq_symm 1
  55. 0055apply mod_eq_symm
  56. 0056exact hone
  57. 0057specialize mod_eq_trans p
  58. 0058specialize mod_eq_trans 1
  59. 0059specialize mod_eq_trans A
  60. 0060specialize mod_eq_trans n
  61. 0061apply mod_eq_trans
  62. 0062exact hone_back
  63. 0063exact hdichotomy_right_right